Abstract
In this paper we report on an application and extension of the theory of Timed Modal Specifications (TMS) and its associated verification tool Epsilon. The novel feature with which Epsilon has been extended is the ability to automatically generate diagnostic information in cases of erroneous refinement steps.
This work has been supported by the Danish Basic Research Foundation project BRICS and the ESPRIT Basic Research Action 7166, CONNCUR2.
Chapter PDF
Similar content being viewed by others
Keyword Codes
Keywords
References
G. Boudol and K.G. Larsen. Graphical versus logical specifications. In Proceedings of CAAP’90, volume 431 of Lecture Notes in Computer Science, 1990.
A. BOrjesson, K.G. Larsen, and A. Skou. Generality in design and compositional verification using tay. In Proceedings of FORTE’92, 1992.
K. Cerâns. Decidability of bisimulation equivalences for processes with parallel timers. In Proceedings of CAV’92, 1992.
K. Cerâns, J.C. Godskesen, and K.G. Larsen. Timed modal specifications — theory and tools. In Proceedings of CAV’93, volume 697 of Lecture Notes in Computer Science. Springer Verlag, 1993.
Jens Chr. Godskesen and Kim G. Larsen. Synthesis of distinguishing formulae for real time systems. To appear, 1994.
J. Godskesen, K. Larsen, and M. Zeeberg. Tay (tools for automatic verification). users manual. Aalborg University. Denmark, 1989.
H. Mittel and K.G. Larsen. The use of static constructs in a modal process logic. In Proceedings of Logic at Botik’89, volume 363 of Lecture Notes in Computer Science. Springer-Verlag, 1989.
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the Association for Computing Machinery, pages 137–161, 1985.
K.G. Larsen. Modal specifications. In Proceedings of Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, 1990.
K. Larsen and B. Thomsen. A modal process logic. In Proceedings LICS’88, 1988.
K.G. Larsen and Y. Wang. Time abstracted bisimulation: Implicit specifications and decidability. In Proceedings of MFPS’93, 1990.
Robin Milner. Communication and Concurrency. Series in Computer Science. Prentice—Hall International, 1989.
D. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, 5th GI Conference, volume 104 of Lecture Notes in Computer Science, pages 167–183, 1981.
J. Parrow. Fairness Properties in Process Algebra. PhD thesis, Uppsala University, Sweden, 1985.
A. Tanenbaum. Computer Networks. Englewood Cliffs, 1988.
Y. Wang. Real—time behaviour of asynchronous agents. In Proceedings of CONCUR’90, volume 458 of Lecture Notes in Computer Science. Springer-Verlag, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Godskesen, J.C., Larsen, K.G., Skou, A. (1995). Automatic Verification of Real-Timed Systems Using Epsilon. In: Vuong, S.T., Chanson, S.T. (eds) Protocol Specification, Testing and Verification XIV. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34867-4_21
Download citation
DOI: https://doi.org/10.1007/978-0-387-34867-4_21
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6308-9
Online ISBN: 978-0-387-34867-4
eBook Packages: Springer Book Archive