ST-LUSTRE: A Novel Spatio-Temporal Language Towards Safety-Critical Cyber-Physical Systems

doi:10.23940/ijpe.17.08.p5.12191232

Abstract

Abstract: Safety-Critical Cyber-Physical Systems (SCCPSs) are a special kind of Cyber-Physical Systems (CPSs) which highlight the importance of system correctness and safety. To apply automatic testing or model checking technique in CPSs, a model that fully captures the features is required to serve as input. So, a novel efficient spatio-temporal language and the analysis techniques are demanded to support both temporal and spatial expression and reasoning. In fact, a synchronous language, LUSTRE, is widely used in safety-critical systems development. However, LUSTRE lacks spatial constructors. Thus, it is difficult to express the behaviors related to spatial features in SCCPSs. In this paper, we propose a language named ST-LUSTRE to support the unified modeling of spatial and temporal properties of CPSs. We define the syntax and semantics of ST-LUSTRE. Its semantics is interpreted on the topological space and natural number which is based on time sets. We also specify typical SCCPSs properties in ST-LUSTRE. ST-LUSTRE is successfully applied to a communication based train control system of Shanghai Fuxin Intelligent Transportation Solutions CO.,Ltd. (FITSCO).

Submitted on October 11, 2017; Revised on November 9, 2017; Accepted on November 25, 2017
References: 17

Jing Liu, Junyang Wang, Zhiwei Li, Haiying Sun, Yuejun Wang, Dehui Du, Xiaohong Chen, and Mingsong Chen. ST-LUSTRE: A Novel Spatio-Temporal Language Towards Safety-Critical Cyber-Physical Systems [J]. Int J Performability Eng, 2017, 13(8): 1219-1232.

Add to citation manager EndNote|Reference Manager|ProCite|BibTeX|RefWorks

References 0

	K. Bauer, “A new modelling language for cyber-physical systems”, Electronic Journal of Differential Equations, vol. 136, no. 2, pp. 281-286, 2012
	B. Bennett, “Spatial reasoning with propositional logics”, Principles of Knowledge Representation & Reasoning, pp.51-62, 1994
	B. Bennett, A. G. Cohn, F. Wolter and M. Zakharyaschev, “Multi-dimensional modal logic as a framework for spatio-temporal reasoning”, Applied Intelligence, vol. 17, no. 3, 239-251, 2002
	A. D. Bimbo, E. Vicario and D. Zingoni, “Symbolic description and visual querying of image sequences using spatio-temporal logic”, IEEE Transactions on Knowledge & Data Engineering, vol. 7, no. 4, pp. 609-622, 1995
	P. Caspi, D. Pilaud, N. Halbwachs and J. A. Plaice, “Lustre: A declarative language for programming synchronous systems”, Symposium on Principles of Programming Languages Acm, vol. 259, no. 89, pp. 911, 1987
	P. Caspi and M. Pouzet, “A functional extension to Lustre”, International Symposium on Languages for Intentional Programming, 1995
	I. Haghighi, A. Jones, Z. D. Kong, E. Bartocci, R. Gros and C. Belta, “SpaTeL: a novel spatial-temporal logic and its applications to networked systems”, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 2015
	N. Halbwachs, P. Caspi, P. Raymond and D. Pilaud, “The synchronous data flow programming language LUSTRE”, Proceedings of the IEEE, vol. 79, no. 9, pp. 1305-1320, 2000
	E. A. Lee, “Cyber Physical Systems: Design Challenges”, IEEE International Symposium on Object Oriented Real-Time Distributed Computing, pp.363-369, 2008
	S. Merz, M. Wirsing and J. Zappe, “A spatio-temporal logic for the specification and refinement of mobile systems”, In: Fundamental Approaches to Software Engineering, Springer Berlin Heidelberg, pp. 87-101, 2003
	P. Muller, “A qualitative theory of motion based on spatio-temporal primitives”, Principles of Knowledge Representation and Reasoning, pp. 131-141, 1998
	L. Nenzi, L. Bortolussi, V. Ciancia, M. Loreti and M. Massink, “Qualitative and quantitative monitoring of spatio-temporal properties.” Runtime Verification. Springer International Publishing, 2015
	D. A Randell, Z Cui and A. G. Cohn, “A Spatial Logic based on Regions and Connection”, Principles of Knowledge Representation and Reasoning, pp.165-176, 1992
	R. Rajkumar, I. Lee, L. Sha and J. Stankovic, “Cyber-physical systems: the next computing revolution”, Design Automation Conference IEEE, pp. 731-736, 2010
	L. Sha, S. Gopalakrishnan, X. Liu and Q. X. Wang, “Cyber-Physical Systems: A New Frontier”, IEEE International Conference on Sensor Networks, Ubiquitous, and Trustworthy Computing IEEE Computer Society, pp.3-13, 2008
	Y. Tan, M. C Vuran and S. Goddard, “Spatio-Temporal Event Model for Cyber-Physical Systems”, IEEE International Conference on Distributed Computing Systems Workshops, pp. 44-50, 2009
	F. Wolter and M. Zakharyaschev, “Spatio-temporal representation and reasoning based on RCC-8”, Principles of Knowledge Representation and Reasoning, pp. 3-14, 2000