TIMED CONCURRENT STATE MACHINES

Wiktor B. Daszczuk

doi:10.7494/csci.2007.8.3.23

Authors

Wiktor B. Daszczuk Warsaw University of Technology

DOI:

https://doi.org/10.7494/csci.2007.8.3.23

Keywords:

formal methods, model checking, real time verification, timed automata

Abstract

Timed Concurrent State Machines are an application of Alur Timed Automata concept tocoincidence-based (rather than interleaving) CSM modeling technique. TCSM support theidea of testing automata, allowing to specify time properties easier than temporal formulas.Also, calculation of a global state space in real-time domain (Region Concurrent State Machines)is defined, allowing to store a verified system in ready-to-verification form, and tomultiply it by various testing automata.

Downloads

Download data is not yet available.

Author Biography

Wiktor B. Daszczuk, Warsaw University of Technology

Institute of Computer Science

References

Alur R., Dill D. L.: A Theory of Timed Automata. Theoretical Computer Science, Vol. 126, 1994, p. 183–235

Alur R.: Timed Automata. in 11th International Conference on Computer-Aided Verification, LNCS 1633, Springer-Verlag, 1999, p. 8–22

Alur E., Courcoubetis C., Dill D. L.: Model-checking in dense real-time. Information and Computation, Vol 104, No. 1, 1993, p. 2–34

Daszczuk W.B.: Verification of Design Decisions in Communication Protocol by Evaluation of Temporal Logic Formulas. Institute of Computer Science, WUT, ICS Research Report No 22, 1998

Daszczuk W.B., Mieścicki J., Nowacki M., Wytrbowicz J.: System Level Specification and Verification Using Concurrent State Machines and COSMA Environment. Proc. 8th International Conference on Mixed Design of Integrated Circuits and Systems, MIXDES 2001, June 21–23, Zakopane, Poland, 2001, p. 525–532

Daszczuk W.B., Grabski W., Mieścicki J., Wytrębowicz J.: System Modeling in the COSMA Environment. Proc. Euromicro Symposium on Digital Systems Design Architectures, Methods and Tools, September 4–6,Warsaw, Poland, IEEE Computer Society, Los Alamos, CA, 2001, p. 152–157

Daszczuk W.B.: Verification of Temporal Properties in Concurrent Systems, Ph.D. thesis, Warsaw University of Technology, 2003

Daszczuk W.B.: Timed Concurrent State Machines, Institute of Computer Science, WUT, ICS Research Report No 27, 2003

Mieścicki J.: Concurrent System of Communicating Machines, Institute of Computer Science, WUT, ICS Research Report No 35, 1992

Mieścicki J., Baszun M., Daszczuk W.B., Czejdo B.: Verification of Concurrent Engineering Software Using CSM Models, Proc. 2nd World Conf. on Integrated Design and Process Technology, Austin, Texas, USA, 1 4 Dec. 1996, 322–330

Mieścicki J., Czejdo B., Daszczuk W.B.: Model checking in the COSMA environment as a support for the design of pipelined processing. Proc. European Congress on Computational Methods in Applied Sciences and Engineering ECCOMAS

, Jyvaskyla, Finland, 24–28 July 2004

Mieścicki J., Czejdo B., Daszczuk W.B., Multi-phase model checking of a threestage pipeline using the COSMA tool, Proc. European Congress on Computational Methods in Applied Sciences and Engineering ECCOMAS 2004, Jyvaskyla, Finland,

–28 July 2004

Mieścicki J.: Verification of UML State Diagrams Using Concurrent State Machines, IFIP Working Conference on Software Engineering Techniques SET’2006, October 17–20 2006, Warsaw, Poland

Zhang Z.: An Approach to Hierarchy Model Checking via Evaluating CTL Hierarchically. Proc. of the 4th Asian Test Symposium, ATS’95, IEEE 1995, 45–49