Abstract
This article presents CREST, a novel domain-specific language for the modelling of cyber-physical systems. CREST is designed for the simple and clear modelling, simulation and verification of small-scale systems such as home and office automation, smart gardening systems and similar. The language is designed to model the flow of resources throughout the system. It features synchronous system evolution and reactive behaviour. CREST’s formal semantics allow real-valued time advances and the modelling of timed system evolution. The continuous time concept permits the precise simulation of future system behaviour by automatically calculating next transition times. We present CREST in a practical manner, and elaborate on the Python-based DSL implementation and simulator.
This project is supported by: FNRS STRATOS: Strategy based Term Rewriting for Analysis and Testing Of Software, the Hasler Foundation, 1604 CPS-Move, and COST IC1404: MPM4CPS
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
Section 4 shows how Python is used as a host language for implementing transition guards and other parts of CREST.
- 3.
- 4.
- 5.
- 6.
References
Ashenden, P.J.: The Designer’s Guide to VHDL, 3rd edn. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (2008)
Berry, G., Gonthier, G.: The Esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19, 87–152 (1992)
Black, D.C., Donovan, J., Bunton, B., Keist, A.: SystemC: From the Ground Up. Springer, New York Inc, Secaucus, NJ, USA (2010)
Bourke, T., Pouzet, M.: Zélus: a synchronous language with ODEs. In: 16th International Conference on Hybrid Systems: Computation and Control (2013)
Brooks, C., Cataldo, A., Lee, E.A., Liu, J., Liu, X., Neuendorffer, S., Zheng, H.: Hyvisual: a hybrid system visual modeler. Technical Report UCB/ERL M05/24, EECS Department, University of California, Berkeley (2005)
Carloni, L.P., Passerone, R., Pinto, A., Angiovanni-Vincentelli, A.L.: Languages and tools for hybrid systems design. Found. Trends Electron. Des. Autom. 1, 1–193 (2006)
Colgren, R.: Basic Matlab, Simulink And Stateflow. AIAA (American Institute of Aeronautics & Ast (2006)
De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Proceedings 14th International Conference Tools and Algorithms f.t. Construction and Analysis of Systems (2008)
Feiler, P., Gluch, D., Hudak, J.: The architecture analysis & design language (AADL): an introduction. Technical Report CMU/SEI-2006-TN-011, Software Engineering Institute, Carnegie Mellon University (2006)
Fischer, J., Holz, E., Löwis, M., Prinz, A.: SDL-2000: a language with a formal semantics. in: Rigorous Object-Oriented Methods 2000 (2000)
Franca, R.B., Bodeveix, J.P., Filali, M., Rolland, J.F., Chemouil, D., Thomas, D.: The AADL behaviour annex – experiments and roadmap. In: 12th IEEE International Conference on Engineering Complex Computer Systems (2007)
Haber, A., Ringert, J.O., Rumpe, B.: Montiarc - architectural modeling of interactive distributed and cyber-physical systems (2014)
Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language LUSTRE. In: Proceedings of the IEEE (1991)
Hamon, G., Rushby, J.: An operational semantics for stateflow. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 229–243. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24721-0_17
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)
Khedker, U.P., Sanyal, A., Sathe, B.: Data Flow Analysis - Theory and Practice. CRC Press (2009). http://www.crcpress.com/product/isbn/9780849328800
Klikovits, S., Linard, A., Buchs, D.: CREST formalization. Technical report, Software Modeling and Verification Group, University of Geneva (2018). https://doi.org/10.5281/zenodo.1284561
Object Management Group: UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded Systems (OMG MARTE) Version 1.1 (2011). https://www.omg.org/spec/MARTE/1.1/PDF, OMG Document Number: formal-2011-06-02
Object Management Group: OMG Systems Modeling Language (OMG SysML) Version 1.5 (2017). https://www.omg.org/spec/SysML/1.5/PDF, OMG Document Number: formal-2017-05-01
Ptolemaeus, C. (ed.): System Design, Modeling, and Simulation using Ptolemy II. Ptolemy.org (2014)
Raskin, J.: An introduction to hybrid automata. In: Hristu-Varsakelis D., Levine W.S. (eds.) Handbook of Networked and Embedded Control Systems (2005)
Ringert, J.O., Rumpe, B., Wortmann, A.: Architecture and Behavior Modeling of Cyber-Physical Systems with MontiArcAutomaton (2015)
Thomas, D., Moorby, P.: The Verilog Hardware Description Language. The Verilog Hardware Description Language. Kluwer Academic Publishers, San Francisco (1996)
Vlaovič, B., Vreže, A., Brezočnik, Z., Kapus, T.: Verification of an SDL Specification — a Case Study. Elektrotehniški vestnik (Electrotechnical Review) (2005)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Klikovits, S., Linard, A., Buchs, D. (2018). CREST - A DSL for Reactive Cyber-Physical Systems. In: Khendek, F., Gotzhein, R. (eds) System Analysis and Modeling. Languages, Methods, and Tools for Systems Engineering. SAM 2018. Lecture Notes in Computer Science(), vol 11150. Springer, Cham. https://doi.org/10.1007/978-3-030-01042-3_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-01042-3_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-01041-6
Online ISBN: 978-3-030-01042-3
eBook Packages: Computer ScienceComputer Science (R0)