Username   Password       Forgot your password?  Forgot your username? 

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

Volume 13, Number 8, December 2017, pp. 1219-1232
DOI: 10.23940/ijpe.17.08.p5.12191232

Jing Liua, Junyang Wanga, Zhiwei Lia, Haiying Suna, Yuejun Wangb, Dehui Dua, Xiaohong Chena, Mingsong Chena

aNational Trustworthy Embedded Software Engineering Reseearch Centre, East China Normal University, Shanghai 200333, China
bShanghai Fuxin Intelligent Transportation Solutions Co.Ltd, Zhangjiang Hi-Tech Park, Shanghai 200120, China

(Submitted on October 11, 2017; Revised on November 9, 2017; Accepted on November 25, 2017)


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).


References: 17

      1. K. Bauer, “A new modelling language for cyber-physical systems”, Electronic Journal of Differential Equations, vol. 136, no. 2, pp. 281-286, 2012
      2. B. Bennett, “Spatial reasoning with propositional logics”, Principles of Knowledge Representation & Reasoning, pp.51-62, 1994
      3. 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
      4. 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
      5. 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
      6. P. Caspi and M. Pouzet, “A functional extension to Lustre”, International Symposium on Languages for Intentional Programming, 1995
      7. 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
      8. 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
      9. E. A. Lee, “Cyber Physical Systems: Design Challenges”, IEEE International Symposium on Object Oriented Real-Time Distributed Computing, pp.363-369, 2008
      10. 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
      11. P. Muller, “A qualitative theory of motion based on spatio-temporal primitives”, Principles of Knowledge Representation and Reasoning, pp. 131-141, 1998
      12. 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
      13. 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
      14. R. Rajkumar, I. Lee, L. Sha and J. Stankovic, “Cyber-physical systems: the next computing revolution”, Design Automation Conference IEEE, pp. 731-736, 2010
      15. 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
      16. 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
      17. F. Wolter and M. Zakharyaschev, “Spatio-temporal representation and reasoning based on RCC-8”, Principles of Knowledge Representation and Reasoning, pp. 3-14, 2000


          Please note : You will need Adobe Acrobat viewer to view the full articles.Get Free Adobe Reader

          This site uses encryption for transmitting your passwords.