Skip to main content
SpringerLink
Log in

Formal Specification of Cyber Physical Systems: Case Studies Based on Hybrid Relation Calculus

  • Conference paper
Multimedia and Ubiquitous Engineering

Part of the book series: Lecture Notes in Electrical Engineering ((LNEE,volume 308))

Abstract

Hybrid system is a dynamic mixture of continuous physical world and discrete control part. In hybrid systems, continuous and discrete dynamic behaviors are displayed by the continuous and discrete components of the system respectively. Due to the complicated mixture mechanism, it becomes very difficult for us to model such a system accurately and explicitly. To simplify the modeling process, Jifeng He proposes a hybrid parallel programming language. It is in the light of his intellectual work that we can model physical world as well as its interaction with the control program. This paper aims to apply the programming language proposed by Jifeng He to the specification of hybrid systems. To describe this language specifically, we used a simple system which consists of a motor boat on a lake modeled by the space R2 .This example illustrates that using hybrid relation calculus to specify hybrid systems can make every subsystem less complicated and more detailed, so that we can get easy access to observe the physical mechanism of the system.

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 169.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. COMPUTING E. Cyber-physical systems (2009)

    Google Scholar 

  2. Bingqing, X., Jifeng, H., Lichen, Z.: Specification of Cyber Physical Systems Based on Clock Theory (2013)

    Google Scholar 

  3. Simpson, H.R.: Four-slot fully asynchronous communication mechanism. Computers and Digital Techniques, IEE Proceedings E 137(1), 17–30 (1990)

    Article  Google Scholar 

  4. He, J.: Hybrid Relation Calculus. In: 2013 18th International Conference on Engineering of Complex Computer Systems (ICECCS), p. 2. IEEE (2013)

    Google Scholar 

  5. Sanchez, C., Julian, B., Belleville, P., et al.: Applications of hybrid organic–inorganic nanocomposites. Journal of Materials Chemistry 15(35-36), 3559–3592 (2005)

    Article  Google Scholar 

  6. Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HyTech: A model checker for hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 460–463. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  7. Dolbeau, R., Bihan, S., Bodin, F.: HMPP: A hybrid multi-core parallel programming environment. In: Workshop on General Purpose Processing on Graphics Processing Units (GPGPU 2007) (2007)

    Google Scholar 

  8. Blackburn, P., Seligman, J.: Hybrid languages. Journal of Logic, Language and Information 4(3), 251–272 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  9. Bauer, K.: A New Modelling Language for Cyber-physical Systems. Verlag Dr. Hut (2012)

    Google Scholar 

  10. Zhu, L., Zhao, Y., Zhu, H., Xu, Q.: Towards a modeling language for cyber-physical systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 394–411. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  11. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM (JACM) 32(1), 137–161 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  12. Man, K.L., Schiffelers, R.R.H.: Formal specification and analysis of hybrid systems. Dissertation Abstracts International 68(01) (2006)

    Google Scholar 

  13. Bingqing, X., et al.: Specification of Cyber Physical Systems by Clock. In: AST 2013, Yeosu, South Korea. ASTL, vol. 20, pp. 111–114 (2013)

    Google Scholar 

  14. Alur, R., Grosu, R., Hur, Y., Kumar, V., Lee, I.: Modular specification of hybrid systems in CHARON. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 6–19. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  15. Jifeng, H.: A clock-based framework for construction of hybrid systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol. 8049, pp. 22–41. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Wenli Zhang, Lichen Zhang & Haibin Cai

Authors
  1. Wenli Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lichen Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Haibin Cai
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Seoul University of Science & and Technology (SeoulTech), Seoul, Korea, Republic of (South Korea)

    James J. (Jong Hyuk) Park

  2. School of Computing and Information Sciences, Florida International University, Miami, Florida, Florida, USA

    Shu-Ching Chen

  3. School of IT Engineering, Catholic University of Daegu, Kyungsan-shi, Korea, Republic of (South Korea)

    Joon-Min Gil

  4. School of Computer Science and Engineeri, The University of Aizu, Aizu-Wakamatsu City, Fukushima, Japan

    Neil Y. Yen

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zhang, W., Zhang, L., Cai, H. (2014). Formal Specification of Cyber Physical Systems: Case Studies Based on Hybrid Relation Calculus. In: Park, J., Chen, SC., Gil, JM., Yen, N. (eds) Multimedia and Ubiquitous Engineering. Lecture Notes in Electrical Engineering, vol 308. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54900-7_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-54900-7_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-54899-4

  • Online ISBN: 978-3-642-54900-7

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation