Abstract
We present in this paper a method to transform ET-LOTOS expressions in a subclass of timed automaton with timers, where a timer is not restarted before its reset. We show that this subclass is equivalent to timed automata and we show that this model can be used for ET-LOTOS verification. We have implemented this transformation method and interfaced our tool with the KRONOS model-checker. It is then possible to verify temporal properties, expressed in TCTL, on ET-LOTOS specifications. We illustrate our tool with a small robot controller example.
Chapter PDF
Similar content being viewed by others
References
R. Alur and C. Courcoubetis and D.L. Dill (1990). Model-checking for real-time systems, in Proceedings of the 5th Symposium on Logic Computer Science, pages 414–425.
R. Alur, C. Courcoubetis, N. Hallbwachs, T.A. Henzinger, P.-H HO, X. Nicollin, A. Olivero, J. Sifakis and S. Yovine (1995). The algorithmic analysis of hybrid systems, in TCS 138, pages 3–34.
J.-P. Courtiat and R.C. de Oliveira (1995). A Reachability Analysis of RT-LOTOS Specifications, in Formal Description techniques VIII, chapman & Hall, pages 117–124.
C. Daws and A. Olivero and S. Tripakis and S. Yovine (1996). The tool KRONOS, in Hybrid Systems III, Lecture Notes in Computer Science 1066, Springer-Verlag
C. Daws and A. Olivero and S. Yovine (1994). Verifying ET-LOTOS programs with KRONOS, in Seventh International Conference on Formal Description Techniques, Chapman & Hall, pages 227–242.
T. A. Henzinger and P. H. Ho (1994). HyTech: the cornell HYbrid TECHnology tool, in Hybrid Systems II, Lecture Notes in Computer Science 999, Springer-Verlag, pages 265–294.
C. Hernalsteen (1997). Timed automaton with semi timers for ET-LOTOS verification, Technical report TR-363, Computer science department, Free University of Brussels.
C. Hernalsteen and T. Massart (1995). An extended timed automaton to model ET-LOTOS Specification, in participant’s proceedings of DARTS’95, pages 95–112
Luc Léonard and Guy Leduc (1994). An Enhanced Version of Timed LOTOS and Its Application to a Case Study, in FORTE-VI, pages 483500, North-Holland.
X. Nicollin and J. Sifakis (1991). An overview and synthesis on timed process algebra, in Proc. 3rd Workshop on Computer-Aided Verification.
P. Varaiya (1997). SHIFT: A language for simulating Interconnected Hybrid Systems, in Hybrid and Real-Time Systems, Lecture Notes in Computer Science 1201, Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Hernalsteen, C. (1997). A timed automaton model for ET-LOTOS verification. In: Mizuno, T., Shiratori, N., Higashino, T., Togashi, A. (eds) Formal Description Techniques and Protocol Specification, Testing and Verification. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35271-8_12
Download citation
DOI: https://doi.org/10.1007/978-0-387-35271-8_12
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5260-1
Online ISBN: 978-0-387-35271-8
eBook Packages: Springer Book Archive