A verification framework for spatio-temporal consistency language with CCSL as a specification language

Abstract

The Spatio-Temporal Consistency Language (STeC) is a high-level modeling language that deals natively with spatio-temporal behaviour, i.e., behaviour relating to certain locations and time. Such restriction by both locations and time is of first importance for some types of real-time systems. CCSL is a formal specification language based on logical clocks. It is used to describe some crucial safety properties for real-time systems, due to its powerful expressiveness of logical and chronometric time constraints. We consider a novel verification framework combining STeC and CCSL, with the advantages of addressing spatio-temporal consistency of system behaviour and easily expressing some crucial time constraints. We propose a theory combining these two languages and a method verifying CCSL properties in STeC models. We adopt UPPAAL as the model checking tool and give a simple example to illustrate how to carry out verification in our framework.

Keywords

spatio-temporal consistency / real-time systems / spatio-temporal systems / high-level modelling language / clock constraint specification / model checking / verification framework

References

[1] Chen Y. STeC: a location-triggered specification language for real-time systems. In: Proceedings of the 15th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops. 2012, 1–6

[2] Wu H, Chen Y, Zhang M. On denotational semantics of spatialtemporal consistency language—STeC. In: Proceedings of International Symposium on Theoretical Aspects of Software Engineering. 2013, 113–120

[3] Hoare C A R. Communicating sequential processes. Communications of the ACM, 1978, 21(8): 666–677

[4] Milner R. A Calculus of Communicating Systems. Secaucus, NJ, USA: Springer-Verlag New York, 1982

[5] Reed G M, Roscoe A W. A timed model for communicating sequential processes. Theoretical Computer Science, 1988, 58(1–3): 249–261

[6] Wang Y. CCS+ time= an interleaving model for real time systems. In: Proceedings of International Colloquium on Automata, Languages and Programming. 1991, 217–228

[7] Cardelli L, Gordon A D. Mobile ambients. Theoretical Computer Science, 2000, 240(1): 177–213

[8] Milner R, Parrow J, Walker D. A calculus of mobile processes. Information and Computation, 1992, 100(1): 1–40

[9] André C, Mallet F. Clock constraint specification language: specifying clock constraints with UML/MARTE. Innovations in Systems and Software Engineering, 2008, 4(3): 309–314

[10] Lamport L. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978, 21(7): 558–565

[11] OMG. UML profile for MARTE: modeling and analysis of real-time embedded systems. Technical Report, 2009

[12] Baier C, Katoen J P. Principles of Model Checking (Representation and Mind Series). Cambridge, Mass: The MIT Press, 2008

[13] IEEE. IEEE standard for property specification language (PSL). New York: Institute of Electrical and Electronics Engineers, 2010

[14] Gascon R, Mallet F, Deantoni J. Logical time and temporal logics: comparing UML MARTE/CCSL and PSL. In: Proceedings of the 18th International Symposium on Temporal Representation and Reasoning. 2011, 141–148

[15] André C, Mallet F, De Simone R. Modeling time(s). In: Proceedings of the International Conference on Model Driven Engineering Languages and Systems. 2007, 559–573

[16] Behrmann G, David A, Larsen K G. A Tutorial on UPPAAL. Berlin Heidelberg: Springer, 2004, 200–236

[17] Suryadevara J, Seceleanu C, Mallet F, Pettersson P. Verifying MARTE/CCSL mode behaviors using UPPAAL. In: Proceedings of the International Conference on Software Engineering and Formal Methods. 2013, 1–15

[18] Zhang Y, Mallet F, Chen Y. Timed automata semantics of spatialtemporal consistency language STeC. In: Proceedings of Theoretical Aspects of Software Engineering Conference. 2014, 201–208

[19] Mallet F, Simone R. Correctness issues on MARTE/CCSL constraints. Science of Computer Programming, 2015, 106: 78–92

[20] André C. Syntax and semantics of the clock constraint specification language (CCSL). Research Report RR-6925 INRIA, 2009

[21] Mallet F. Logical Time @ Work for the Modeling and Analysis of Embedded Systems. Saarbrücken Allemagn: LAP Lambert Academic Publishing, 2011

[22] Mallet F, Millo J V, Simone R. Safe CCSL specifications and marked graphs. In: Proceedings of ACM/IEEE International Conference on Formal Methods and Models for Codesign. 2013, 157–166

[23] Alur R, Dill D L. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183–235

[24] Mallet F. Automatic generation of observers from MARTE/CCSL. In: Proceedings of the 23rd IEEE International Symposium on Rapid System Prototyping. 2012, 86–92

[25] Huth M, Ryan M. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge: Cambridge University Press, 2004

[26] Rumbaugh J, Jacobson I, Booch G. Unified Modeling Language Reference Manual. Boston: Addison-Wesley, 2005

[27] Chen Y W, Chen Y X, Madelaine E. Timed-pNets: a communication behavioural semantic model for distributed systems. Frontiers of Computer Science, 2015, 9(1): 87–110

[28] Deantoni J, Mallet F. Timesquare: treat your models with logical time. In: Proceedings of the 50th International Conference on Modelling Techniques and Tools for Computer Permance Evaluation. 2012, 34–41

[29] He J. A clock-based framework for construction of hybrid systems. In: Proceedings of International Colloquium on Theoretical Aspects of Computing. 2013, 22–41

[30] Xu B, Zhang L. Formal specification of cyber physical systems: three case studies based on clock theory. In: Proceedings of IEEE International Conference on Green Computing and Communications (Green- Com) and IEEE Internet of Things (iThings) and IEEE Cyber, Physical and Social Computing (CPSCom). 2013, 804–811

[31] André C, Mallet F. Specification and verification of time requirements with CCSL and Esterel. In: Proceedings of ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems. 2009, 167–176

[32] Berry G, Gonthier G. The esterel synchronous programming language: design, semantics, implementation. Science of Computer Programming, 1992, 29(2): 87–152

[33] Yin L, Mallet F, Liu J. Verification of MARTE/CCSL time requirements in Promela/SPIN. In: Proceedings of the 16th IEEE International Conference on Engineering of Complex Computer Systems. 2011, 65–74

[34] Holzmann G J. The model checker SPIN. IEEE Transactions on Software Engineering, 1997, 23(5): 279–295

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature