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

doi:10.1007/s11704-018-7054-8

Front. Comput. Sci.

2020, Vol. 14

Issue (1) : 105-129 https://doi.org/10.1007/s11704-018-7054-8

RESEARCH ARTICLE

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

Yuanrui ZHANG¹, Frédéric MALLET¹(

), Yixiang CHEN¹(

)

¹. MoE Engineering Research Center for Software/Hardware Co-design Technology and Application, East China Normal University, Shanghai 200062, China
². University Nice Sophia Antipolis, I3S, UMR 7271 CNRS, INRIA, 06900 Sophia Antipolis, France

Download: PDF(900 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Corresponding Author(s): Frédéric MALLET,Yixiang CHEN

Just Accepted Date: 22 January 2018 Online First Date: 15 November 2018 Issue Date: 24 September 2019

Cite this article:

Yuanrui ZHANG,Frédéric MALLET,Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-018-7054-8
https://academic.hep.com.cn/fcs/EN/Y2020/V14/I1/105

1	Y Chen. 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	H Wu, Y Chen, M Zhang. On denotational semantics of spatialtemporal consistency language—STeC. In: Proceedings of International Symposium on Theoretical Aspects of Software Engineering. 2013, 113–120
3	C A R Hoare. Communicating sequential processes. Communications of the ACM, 1978, 21(8): 666–677 https://doi.org/10.1145/359576.359585
4	R Milner. A Calculus of Communicating Systems. Secaucus, NJ, USA: Springer-Verlag New York, 1982
5	G M Reed, A W Roscoe. A timed model for communicating sequential processes. Theoretical Computer Science, 1988, 58(1–3): 249–261 https://doi.org/10.1016/0304-3975(88)90030-8
6	Y Wang. CCS+ time= an interleaving model for real time systems. In: Proceedings of International Colloquium on Automata, Languages and Programming. 1991, 217–228
7	L Cardelli, A D Gordon. Mobile ambients. Theoretical Computer Science, 2000, 240(1): 177–213 https://doi.org/10.1016/S0304-3975(99)00231-5
8	R Milner, J Parrow, D Walker. A calculus of mobile processes. Information and Computation, 1992, 100(1): 1–40 https://doi.org/10.1016/0890-5401(92)90008-4
9	C André, F Mallet. Clock constraint specification language: specifying clock constraints with UML/MARTE. Innovations in Systems and Software Engineering, 2008, 4(3): 309–314 https://doi.org/10.1007/s11334-008-0055-2
10	L Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978, 21(7): 558–565 https://doi.org/10.1145/359545.359563
11	OMG. UML profile for MARTE: modeling and analysis of real-time embedded systems. Technical Report, 2009
12	C Baier, J P Katoen. 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	R Gascon, F Mallet, J Deantoni. 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 https://doi.org/10.1109/TIME.2011.10
15	C André, F Mallet, R De Simone. Modeling time(s). In: Proceedings of the International Conference on Model Driven Engineering Languages and Systems. 2007, 559–573 https://doi.org/10.1007/978-3-540-75209-7_38
16	G Behrmann, A David, K G Larsen. A Tutorial on UPPAAL. Berlin Heidelberg: Springer, 2004, 200–236 https://doi.org/10.1007/978-3-540-30080-9_7
17	J Suryadevara, C Seceleanu, F Mallet, P Pettersson. Verifying MARTE/CCSL mode behaviors using UPPAAL. In: Proceedings of the International Conference on Software Engineering and Formal Methods. 2013, 1–15 https://doi.org/10.1007/978-3-642-40561-7_1
18	Y Zhang, F Mallet, Y Chen. Timed automata semantics of spatialtemporal consistency language STeC. In: Proceedings of Theoretical Aspects of Software Engineering Conference. 2014, 201–208
19	F Mallet, R Simone. Correctness issues on MARTE/CCSL constraints. Science of Computer Programming, 2015, 106: 78–92 https://doi.org/10.1016/j.scico.2015.03.001
20	C André. Syntax and semantics of the clock constraint specification language (CCSL). Research Report RR-6925 INRIA, 2009
21	F Mallet. Logical Time @ Work for the Modeling and Analysis of Embedded Systems. Saarbrücken Allemagn: LAP Lambert Academic Publishing, 2011
22	F Mallet, J V Millo, R Simone. Safe CCSL specifications and marked graphs. In: Proceedings of ACM/IEEE International Conference on Formal Methods and Models for Codesign. 2013, 157–166
23	R Alur, D L Dill. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183–235 https://doi.org/10.1016/0304-3975(94)90010-8
24	F Mallet. Automatic generation of observers from MARTE/CCSL. In: Proceedings of the 23rd IEEE International Symposium on Rapid System Prototyping. 2012, 86–92 https://doi.org/10.1109/RSP.2012.6380695
25	M Huth, M Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge: Cambridge University Press, 2004 https://doi.org/10.1017/CBO9780511810275
26	J Rumbaugh, I Jacobson, G Booch. Unified Modeling Language Reference Manual. Boston: Addison-Wesley, 2005
27	Y W Chen, Y X Chen, E Madelaine. Timed-pNets: a communication behavioural semantic model for distributed systems. Frontiers of Computer Science, 2015, 9(1): 87–110 https://doi.org/10.1007/s11704-014-4096-4
28	J Deantoni, F Mallet. 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 https://doi.org/10.1007/978-3-642-30561-0_4
29	J He. A clock-based framework for construction of hybrid systems. In: Proceedings of International Colloquium on Theoretical Aspects of Computing. 2013, 22–41
30	B Xu, L Zhang. 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	C André, F Mallet. 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 https://doi.org/10.1145/1542452.1542475
32	G Berry, G Gonthier. The esterel synchronous programming language: design, semantics, implementation. Science of Computer Programming, 1992, 29(2): 87–152 https://doi.org/10.1016/0167-6423(92)90005-V
33	L Yin, F Mallet, J Liu. 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 https://doi.org/10.1109/ICECCS.2011.14
34	G J Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 1997, 23(5): 279–295 https://doi.org/10.1109/32.588521

[1]

Download

[1]	Kazuhiro OGATA. A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions[J]. Front. Comput. Sci., 2019, 13(1): 51-72.
[2]	Anil Kumar KARNA, Yuting CHEN, Haibo YU, Hao ZHONG, Jianjun ZHAO. The role of model checking in software engineering[J]. Front. Comput. Sci., 2018, 12(4): 642-668.
[3]	Yu ZHOU, Nvqi ZHOU, Tingting HAN, Jiayi GU, Weigang WU. Probabilistic verification of hierarchical leader election protocol in dynamic systems[J]. Front. Comput. Sci., 2018, 12(4): 763-776.
[4]	Fei HE, Yuan GAO, Liangze YIN. Efficient software product-line model checking using induction and a SAT solver[J]. Front. Comput. Sci., 2018, 12(2): 264-279.
[5]	Laixiang SHAN,Xiaomin DU,Zheng QIN. Efficient approach of translating LTL formulae into Büchi automata[J]. Front. Comput. Sci., 2015, 9(4): 511-523.
[6]	Luxi CHEN,Linpeng HUANG,Chen LI,Tao ZAN. Integrating behavior analysis into architectural modeling[J]. Front. Comput. Sci., 2015, 9(1): 15-33.
[7]	Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[8]	Savas KONUR. A survey on temporal logics for specifying and verifying real-time systems[J]. Front. Comput. Sci., 2013, 7(3): 370-403.
[9]	Anh Tuan LUU, Jun SUN, Yang LIU, Jin Song DONG, Xiaohong LI, Thanh Tho QUAN. SeVe: automatic tool for verification of security protocols[J]. Front Comput Sci, 2012, 6(1): 57-75.
[10]	Conghua ZHOU, Bo SUN, Zhifeng LIU. Abstraction for model checking multi-agent systems[J]. Front Comput Sci Chin, 2011, 5(1): 14-25.
[11]	Jiaqi ZHU, Hanpin WANG, Zhongyuan XU, Chunxiang XU, . A new model for model checking: cycle-weighted Kripke structure[J]. Front. Comput. Sci., 2010, 4(1): 78-88.
[12]	Wanwei LIU, Ji WANG, Huowang CHEN, Xiaodong MA, Zhaofei WANG. symbolic model checking APSL[J]. Front Comput Sci Chin, 2009, 3(1): 130-141.

Viewed

Full text

Abstract

Cited

Shared

Discussed