Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Engineering Methods

ICFEM 2019: Formal Methods and Software Engineering pp 517–521Cite as

Spatio-Temporal Specification Language for Cyber-Physical Systems

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11852))

Abstract

Specifying spatio-temporal aspects with changes of spatial entities in dense time is one of the important areas in cyber-physical systems. The major problem is the complexity and verifiability of dense time and real-valued variables of the spatio-temporal properties of cyber-physical systems. We propose a spatio-temporal specification language, named STSL, which integrates Signal Temporal Logic (STL) with a spatial logic S4\(_u\) to deal with the changes of real values spatial entities in dense time. We present a Hilbert-style axiomatization for the proposed STSL and provide the soundness and completeness result. Further, we provide the satisfiable relation of spatio-temporal formulas and the corresponding complexity and a decision procedure is present to check the satisfiability problem of the decidable fragment of STSL. Besides, spatio-temporal model is monitored at runtime for the changes of spatial signals over time using MATLAB.

The work is supervised by Prof. Jing Liu, and partially supported by funding under National Key Research and Development Project 2017YFB1001800, NSFC 61572195 and Shanghai SHEITC Project 2017-GYHLW-01036.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Balbiani, P., Fernández-Duque, D., Lorini, E.: Exploring the bidimensional space: a dynamic logic point of view. In: The 16th Conference on Autonomous Agents and MultiAgent Systems, pp. 132–140. Springer (2017)

    Google Scholar 

  2. Bartocci, E., Gol, E.A., Haghighi, I., Belta, C.: A formal methods approach to pattern recognition and synthesis in reaction diffusion networks. IEEE Trans. Control of Network Syst. 5(1), 308–320 (2018)

    Article  MathSciNet  Google Scholar 

  3. Bennett, B., Cohn, A.G., Wolter, F., Zakharyaschev, M.: Multi-dimensional modal logic as a framework for spatio-temporal reasoning. Applied Intell. 17(3), 239–251 (2002)

    Article  Google Scholar 

  4. Bersani, M.M., Rossi, M., San Pietro, P.: An SMT-based approach to satisfiability checking of MITL. Inf. Comput. 245, 72–97 (2015)

    Article  MathSciNet  Google Scholar 

  5. Ciancia, V., Gilmore, S., Grilletti, G., Latella, D., Loreti, M., Massink, M.: Spatio-temporal model checking of vehicular movement in public transport systems. Int. J. Software Tools Technol. Transf. pp. 1–23 (2018)

    Google Scholar 

  6. Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Gros, R., Belta, C.: Spatel: a novel spatial-temporal logic and its applications to networked systems. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 189–198. ACM (2015)

    Google Scholar 

  7. Li, T., Jing, L., Dongdong, A., Haiying, S.: A sound and complete axiomatisation for spatio-temporal specification language. In: The 31st International Conference on Software Engineering & Knowledge Engineering, pp. 153–204. KSI (2019)

    Google Scholar 

  8. Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties with SSTL. Logical Meth. Comput. Sci. 14(4) (2017)

    Google Scholar 

  9. Schäfer, A.: A calculus for shapes in time and space. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 463–477. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31862-0_33

    Chapter  Google Scholar 

  10. Sun, H., Liu, J., Chen, X., Du, D.: Specifying cyber physical system safety properties with metric temporal spatial logic. In: 2015 Asia-Pacific Software Engineering Conference (APSEC), pp. 254–260. IEEE (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, 200062, China

    Tengfei Li

Authors
  1. Tengfei Li
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tengfei Li .

Editor information

Editors and Affiliations

  1. IRIT/INPT - ENSEEIHT, Toulouse, France

    Yamine Ait-Ameur

  2. Teesside University, Middlesbrough, UK

    Shengchao Qin

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Li, T. (2019). Spatio-Temporal Specification Language for Cyber-Physical Systems. In: Ait-Ameur, Y., Qin, S. (eds) Formal Methods and Software Engineering. ICFEM 2019. Lecture Notes in Computer Science(), vol 11852. Springer, Cham. https://doi.org/10.1007/978-3-030-32409-4_36

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32409-4_36

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32408-7

  • Online ISBN: 978-3-030-32409-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation