Advertisement

Truth — A verification platform for concurrent systems

  • Martin Lange
  • Martin Leucker
  • Thomas Noll
  • Stephan Tobies
Part of the Advances in Computing Science book series (ACS)

Abstract

Formal Methods are becoming more and more popular for the specification and verification of industrial critical systems. Several case studies have shown that these techniques can help to find errors during the design process (see Clarke and Wing (1996) for an overview). They are also gaining commercial success, e.g., companies such as Intel, National Semiconductor or Texas Instruments are establishing new departments for formal methods (see for example the job adverts in Concurrency Mailing List).

Keywords

Model Check Transition System Specification Language Process Algebra Concurrent System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Borovansky, C. Kirchner, H. Kirchner, P.E. Moreau, and M. Vittek. Elan: A logical framework based on computational systems. In Proc. of the First Int. Workshop on Rewriting Logic, volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996.Google Scholar
  2. E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. Technical Report CMU-CS-96–178, Carnegie Mellon University (CMU), September 1996.Google Scholar
  3. Manuel Clavel, Steven Eker, Patrick Lincoln, and Jos Meseguer. Principles of Maude. In José Meseguer, editor, Proceedings of the First International Workshop on Rewriting Logic, volume 4 of Electronic Notes in Theoretical Computer Science, pages 65–89. Elsevier, 1996.Google Scholar
  4. R. Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27 (8): 725–748, 1990.MathSciNetCrossRefMATHGoogle Scholar
  5. R. Cleaveland, E. Madelaine, and S. Sims. A front-end generator for verification tools. Lecture Notes in Computer Science, 1019: 153–173, 1995.CrossRefGoogle Scholar
  6. R. Cleaveland and S. Sims. The NCSU concurrency workbench. Lecture Notes in Computer Science, 1102: 394–397, 1996.CrossRefGoogle Scholar
  7. Volker Diekert and Grzegorz Rozenberg, editors.The Book of Traces. World Scientific, Singapore, 1995.Google Scholar
  8. E. A. Emerson. Automated Temporal Reasoning about Reactive Systems, volume 1043 of Lecture Notes in Computer Science, pages 41–101 Springer-Verlag Inc., New York, NY, USA, 1996.Google Scholar
  9. E. A. Emerson. Model checking and the mu-calculus, volume 31 of DIMACS: Series in Discrete Mathematics and Theoretical Computer Science, chapter 6. American Mathematical Society, 1997.Google Scholar
  10. E.A. Emerson and C.L. Lei. Efficient model checking in fragments of the propositional ti-calculus. In Symposion on Logic in Computer Science pages 267–278, Washington, D.C., USA, June 1986. IEEE Computer Society Press.Google Scholar
  11. Jean-Charles Grégoire, Gerard J. Holzmann, and Doron A. Peled, editors.The Spin Verification System volume 32 of DIMACS series. American Mathematical Society, 1997. ISBN 0–8218–0680–7, 203p.Google Scholar
  12. Dexter Kozen. Results on the propositional mu-calculus.Theoretical Computer Science27:333–354, December 1983.Google Scholar
  13. J. Launchbury and S. Peyton Jones. Lazy functional state threads. In Programming Languages Design and Implementation,Orlando, 1994. ACM Press.Google Scholar
  14. Martin Leucker and Stephan Tobies. Truth—A Platform for Verification of Distributed Systems. Technical Report 98–05, RWTH Aachen, May 1998.Google Scholar
  15. K. L. McMillan. The SMV system, symbolic model checking - an approach. Technical Report CMU-CS-92–131, Carnegie Mellon University, 1992.Google Scholar
  16. J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1):73–155, April 1992.Google Scholar
  17. José Meseguer. Rewriting as a unified model of concurrency. In Proceedings Concur’90 Conference,Lecture Notes in Computer Science, Volume 458, pages 384–400, Amsterdam, August 1990. Springer. Also, Report SRI-CSL-90–02R, Computer Science Lab, SRI International.Google Scholar
  18. José Meseguer. Rewriting logic as a semantic framework for concurrency: a progress report. In Seventh International Conference on Concurrency Theory (CONCUR ‘86), volume 1119 of Lecture Notes in Computer Science, pages 331–372. Springer Verlag, August 1996.Google Scholar
  19. R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.MATHGoogle Scholar
  20. F. Moller. The Edinburgh Concurrency Workbench (Version 6.1). Department of Computer Science, University of Edinburgh, October 1992.Google Scholar
  21. John Peterson, Kevin Hammond, et al. Report on the programming language haskell, a non-strict purely-functional programming language, version 1. 3. Technical report, Yale University, May 1996.Google Scholar
  22. C. Stirling. Games for bisimulation and model checking, June 1997. Notes for Mathfit instructional meeting on games and computation, Edinburgh.Google Scholar
  23. Patrick Viry. Rewriting: An effective model of concurrency. In Proceedings of PARLE ‘84 - Parallel Architectures and Languages Europe volume 817 of Lecture Notes in Computer Science pages 648–660. Springer-Verlag, 1994.Google Scholar
  24. Patrick Viry. Rewriting modulo a rewrite system. Technical Report TR-95–20, Dipartimento di Informatica, December 01 1995.Google Scholar
  25. Patrick Viry. A rewriting implementation of pi-calculus. Technical Report TR-96–30, Dipartimento di Informatica, March 26 1996.Google Scholar

Copyright information

© Springer-Verlag Wien 1999

Authors and Affiliations

  • Martin Lange
  • Martin Leucker
  • Thomas Noll
  • Stephan Tobies

There are no affiliations available

Personalised recommendations