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).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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.
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.
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.
R. Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27 (8): 725–748, 1990.
R. Cleaveland, E. Madelaine, and S. Sims. A front-end generator for verification tools. Lecture Notes in Computer Science, 1019: 153–173, 1995.
R. Cleaveland and S. Sims. The NCSU concurrency workbench. Lecture Notes in Computer Science, 1102: 394–397, 1996.
The concurrency mailing list. http://www-i2.informatik.rwth-aachen.de/Forschung/Mcs/mailing_list.html
Volker Diekert and Grzegorz Rozenberg, editors.The Book of Traces. World Scientific, Singapore, 1995.
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.
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.
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.
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.
Dexter Kozen. Results on the propositional mu-calculus.Theoretical Computer Science27:333–354, December 1983.
J. Launchbury and S. Peyton Jones. Lazy functional state threads. In Programming Languages Design and Implementation,Orlando, 1994. ACM Press.
Martin Leucker and Stephan Tobies. Truth—A Platform for Verification of Distributed Systems. Technical Report 98–05, RWTH Aachen, May 1998.
K. L. McMillan. The SMV system, symbolic model checking - an approach. Technical Report CMU-CS-92–131, Carnegie Mellon University, 1992.
J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1):73–155, April 1992.
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.
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.
R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.
F. Moller. The Edinburgh Concurrency Workbench (Version 6.1). Department of Computer Science, University of Edinburgh, October 1992.
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.
C. Stirling. Games for bisimulation and model checking, June 1997. Notes for Mathfit instructional meeting on games and computation, Edinburgh.
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.
Patrick Viry. Rewriting modulo a rewrite system. Technical Report TR-95–20, Dipartimento di Informatica, December 01 1995.
Patrick Viry. A rewriting implementation of pi-calculus. Technical Report TR-96–30, Dipartimento di Informatica, March 26 1996.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Wien
About this paper
Cite this paper
Lange, M., Leucker, M., Noll, T., Tobies, S. (1999). Truth — A verification platform for concurrent systems. In: Berghammer, R., Lakhnech, Y. (eds) Tool Support for System Specification, Development and Verification. Advances in Computing Science. Springer, Vienna. https://doi.org/10.1007/978-3-7091-6355-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-7091-6355-9_11
Publisher Name: Springer, Vienna
Print ISBN: 978-3-211-83282-0
Online ISBN: 978-3-7091-6355-9
eBook Packages: Springer Book Archive