Skip to main content
SpringerLink
Log in

The Temporal Rover and the ATG Rover

  • Conference paper
SPIN Model Checking and Software Verification (SPIN 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1885))

Included in the following conference series:

Abstract

The Temporal Rover is a specification based verification tool for applications written in C, C++, Java, Verilog and VHDL. The tool combines formal specification, using Linear-Time Temporal Logic (LTL) and Metric Temporal Logic (MTL), with conventional simulation/execution based testing. The Temporal Rover is tailored for the verification of complex protocols and reactive systems where behavior is time dependent. The Temporal Rover generates executable code from LTL and MTL assertions written as comments in the source code. This executable source code is compiled and linked as part of the application under test. During application execution the generated code validates the executing program against the formal temporal specification requirements. Using MTL, real time and relative time constraints can be validated. A special code generator supports validation of such constraints in the field, on an embedded target.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Chang, E., Pnueli, A., Manna, Z.: Compositional Verification of Real-Time Systems. In: Proc. 9’th IEEE Symp. On Logic In Computer Science, pp. 458–465 (1994)

    Google Scholar 

  2. Hailpern, B.T., Owicki, S.: Modular Verification of Communication Protocols. IEEE Trans of comm. COM-31(1), 56–68 (1983) No. 1

    Article  Google Scholar 

  3. Manna, Z., Pnueli, A.: Verification of Concurrent Programs: Temporal Proof Principles. In: Proc. of the Workshop on Logics of Programs. LNCS, pp. 200–252. Springer, Heidelberg (1981)

    Google Scholar 

  4. Owicki, S., Lamport, L.: Proving Liveness Properties of Concurrent Programs. TOPLAS 4(3), 455–495 (1982)

    Article  MATH  Google Scholar 

  5. Prior, A.: Past, Present and Future. Oxford University Press, Oxford (1967)

    MATH  Google Scholar 

  6. Pnueli, A.: The Temporal Logic of Programs. In: Proc. 181977 IEEE Symp. on Foundations of Computer Science, pp. 46–57.

    Google Scholar 

  7. Sistla, A.P., Clarke, E.M.: The Complexity of Linear Propositional Temporal Logic. Journal of the ACM 32, 733–749 (1985)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Time-Rover, Inc., 11425 Charsan Ln., Cupertino, CA, 95014, USA

    Doron Drusinsky

Authors
  1. Doron Drusinsky
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Kestrel Technology, Palo Alto, California, USA

    Klaus Havelund

  2.  ,  

    John Penix

  3. SEVEN Networks, 94063, Redwood City, CA, USA

    Willem Visser

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Drusinsky, D. (2000). The Temporal Rover and the ATG Rover. In: Havelund, K., Penix, J., Visser, W. (eds) SPIN Model Checking and Software Verification. SPIN 2000. Lecture Notes in Computer Science, vol 1885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722468_19

Download citation

  • DOI: https://doi.org/10.1007/10722468_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41030-0

  • Online ISBN: 978-3-540-45297-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation