The CREST project researches the modelling of small cyber-physical systems (CPS), such as smarthomes, office automation or gardening applications. It operates on three basic hypotheses:
Components of such CPS primarily operate on the the production, consumption and transformation of physical resources (e.g. light, water, heat, electricity). Influences between components can be characterised by the continuous resource flow between these components.
These types of CPS are often created by private endusers or domain experts without formal modelling experience. However, these users still want to verify that their systems will work correctly and not fail.
The users often do not have the the technical knowledge or financial means to use expert tools, theoretical formalisms or complicated languages.
CREST aims to provide formal modelling, simulation and verification means for the creators of resource-flow CPS. Indeed, when analysing the formalisms, languages and tools that are currently being used for the modelling of CPS, it becomes evident that very often these solutions have severe caveats. In many cases they operate on a wrong abstraction level, thereby requiring experience to be used effectively, are too generic, thereby introducing a wide semantic gap between model and system.either operate on the wrong abstraction level, or too complicated in their use.
This project investigates the creation of a domain-specific language (DSL) to overcome these issues. The DSL should be easy to learn and use, but flexible enough to be easily extended and adapted to its target use cases. So far, CREST is a formalism (incl. a formal syntax and semantics), and was implemented in two languages:
- CREST diagrams, a graphical language that is easy to understand
- crestdsl, an implementation of CREST as internal DSL in the Python langauge.
While CREST diagrams are a good means for communication and prototyping, crestdsl offers dynamic modelling, the implementation of a simulator and a formal verification module.