Skip to main content
SpringerLink
Log in

Shared-Variable Concurrency, Continuous Behaviour and Healthiness for Critical Cyberphysical Systems

  • Conference paper
  • First Online:
Formal Techniques for Safety-Critical Systems (FTSCS 2016)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 694))

Abstract

In the effort to develop critical cyberphysical systems, existing computing formalisms are extended to include continuous behaviour. This may happen in a way that neglects elements necessary for correct continuous properties and correct physical properties. A simple language is taken to illustrate this. Issues and risks latent in this kind of approach are identified and discussed under the umbrella of ‘healthiness conditions’. Modifications to the language in the light of the conditions discussed are described. An example air conditioning system is used to illustrate the concepts presented, and is developed both in the original language and in the modified version.

The work reported here was done while Richard Banach was a visiting researcher at E.C.N.U. The support of E.C.N.U. is gratefully acknowledged.

Huibiao Zhu is supported by National Natural Science Foundation of China (Grant No. 61361136002) and Shanghai Collaborative Innovation Center of Trustworthy Software for Internet of Things (ZF1213).

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

Access this chapter

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

Institutional subscriptions

Notes

  1. 1.

    In this paper we wish to sidestep the race conditions that arise when two (packages of) updates which read each others’ left hand side variables execute at exactly the same moment.

  2. 2.

    The period of time during which the solution exists may be very short indeed. If \({\varvec{x}}_0\) is right at the boundary of X and F is directed towards the exterior of XY, then \(\tau _{{\varvec{x}}_0}\) may equal 0, and the initial value may be all that there is. This makes the \(\mathcal {DE}\) execution equivalent to \(\mathbf {skip}\).

  3. 3.

    That is to say, it evaluates to false, or fails to evaluate at all.

References

  1. Alur, R.: Principles of Cyberphysical Systems. MIT Press, Cambridge (2015)

    Google Scholar 

  2. Lee, E., Shesha, S.: Introduction to Embedded Systems: A Cyberphysical Systems Approach, 2nd edn. (2015). LeeShesha.org

  3. Hoare, T., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)

    MATH  Google Scholar 

  4. Zhou, C., Hoare, T., Ravn, A.: A calculus of durations. Inf. Process. Lett. 40, 269–276 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  5. Walter, W.: Ordinary Differential Equations. Graduate Texts in Mathematics, vol. 182. Springer, New York (1998)

    MATH  Google Scholar 

  6. Horn, R., Johnson, C.: Matrix Analysis. Cambridge University Press, Cambridge (1985)

    Book  MATH  Google Scholar 

  7. Horn, R., Johnson, C.: Topics in Matrix Analysis. Cambridge University Press, Cambridge (1991)

    Book  MATH  Google Scholar 

  8. DO-178C. http://www.rtca.org

  9. ISO 26262. http://www.iso.org/iso/home/store/catalogue_tc/catalogue_detail.ht m? csnumber=54591

  10. IEC 62304. https://webstore.iec.ch/preview/info_iec62304ed1.0en_d.pdf

  11. CENELEC EN 50128. https://www.cenelec.eu/dyn/www/f?p=104:105

  12. Sztipanovits, J.: Model integration and cyber physical systems: a semantics perspective. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, p. 1. Springer, Heidelberg (2011). doi:10.1007/978-3-642-21437-0_1. http://sites.lero.ie/download.aspx?f=Sztipanovits-Keynote.pdf

    Chapter  Google Scholar 

  13. Willems, J.: Open dynamical systems: their aims and their origins. Ruberti Lecture, Rome (2007). http://homes.esat.kuleuven.be/~jwillems/Lectures/2007/Rubertilecture.pdf

  14. National Science and Technology Council. Trustworthy cyberspace: strategic plan for the federal cybersecurity research and development program (2011). http://www.whitehouse.gov/sites/default/files/microsites/ostp/fed_cybersecurity_rd_strategic_plan_2011.pdf

  15. Geisberger, E., Broy M. (eds.): Living in a networked world. Integrated research agenda cyber-physical systems (agendaCPS) (2015). http://www.acatech.de/fileadmin/user_upload/Baumstruktur_nach_Website/Acatech/root/de/Publikationen/Projektberichte/acaetch_STUDIE_agendaCPS_eng_WEB.pdf

  16. Carloni, L., Passerone, R., Pinto, A., Sangiovanni-Vincentelli, A.: Languages and tools for hybrid systems design. Found. Trends Electron. Des. Autom. 1, 1–193 (2006)

    Article  MATH  Google Scholar 

  17. Henzinger, T.: The theory of hybrid automata. In: Proceedings of IEEE LICS-96, pp. 278–292. IEEE (1996). http://mtc.epfl.ch/~tah/Publications/the_theory_of_hybrid_automata.pdf

  18. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993). doi:10.1007/3-540-57318-6_30

    Chapter  Google Scholar 

  19. Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  20. Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010)

    Book  MATH  Google Scholar 

  21. Symbolaris. http://www.symbolaris.org

  22. Banach, R., Butler, M., Qin, S., Verma, N., Zhu, H.: Core hybrid event-B I: single hybrid event-B machines. Sci. Comput. Prog. 105, 92–123 (2015)

    Article  Google Scholar 

  23. Banach, R., Butler, M., Qin, S., Zhu, H.: Core hybrid event-B II: multiple cooperating hybrid event-B machines. Sci. Comp. Prog. (2017, to appear)

    Google Scholar 

  24. Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Book  MATH  Google Scholar 

  25. Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)

    Book  MATH  Google Scholar 

  26. Clearsy. http://www.clearsy.com/en/

  27. Zhu, H., Qin, S., He, J., Bowen, J.: PTSC: probability, time and shared-variable concurrency. Innov. Syst. Softw. Eng. 5, 271–284 (2009)

    Article  Google Scholar 

  28. Zhu, H., Yang, F., He, J., Bowen, J., Sanders, J., Qin, S.: Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language. J. Log. Alg. Prog. 81, 2–25 (2012)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, University of Manchester, Oxford Road, Manchester, M13 9PL, UK

    Richard Banach

  2. Shanghai Key Laboratory of Trustworthy Computing, MOE International Joint Laboratory of Trustworthy Software, International Research Center of Trustworthy Software, East China Normal University, Shanghai, 200062, China

    Huibiao Zhu

Authors
  1. Richard Banach
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Huibiao Zhu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Richard Banach .

Editor information

Editors and Affiliations

  1. KTH Royal Institute of Technology , Stockholm, Sweden

    Cyrille Artho

  2. Dept of Informatics, University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Banach, R., Zhu, H. (2017). Shared-Variable Concurrency, Continuous Behaviour and Healthiness for Critical Cyberphysical Systems. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2016. Communications in Computer and Information Science, vol 694. Springer, Cham. https://doi.org/10.1007/978-3-319-53946-1_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-53946-1_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-53945-4

  • Online ISBN: 978-3-319-53946-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation