CREST - A Continuous, REactive SysTems DSL Stefan Klikovits Alban Linard Didier Buchs University of Geneva, Geneva, Switzerland firstname.lastname@unige.ch Abstract—The advance of cyber-physical systems in every- Sun day life requires powerful modeling capabilities. Existing for- Grow- Power mains lamp malisms often have severe limitations and require complicated Room notations. In this paper we introduce CREST, a domain-specific temperature language for modeling entity behavior and resource transfers in Plant CPS. CREST aims to support CPS architects through clarity, comprehensiveness and analyzability. Figure 1: Schematic representation of the plant growing study. Arrows represent resource influences: 1. Introduction & Motivation light , heat , electricity The advance of cyber-physical systems (CPS), unions of hardware sensors and actuators and software controllers, Section 3 introduces CREST and its graphical language. emphasizes the importance of analysis, validation and verifi- Section 4 outlines rules for exchange and re-use of CREST cation of such systems. The complexity of CPS often lies in components. Section 5 formalizes CREST’s syntax. Section their systems-of-systems architecture and mutual subsystem 6 explains how to use CREST for validation, simulation, influences. The analysis and development of CPS require a planning and controller synthesis and Section 7 concludes. clear and comprehensive means of modeling. In this paper we introduce CREST, a domain-specific 2. State of the Art language (DSL) for continuous and reactive systems. CREST focuses on the specification of CPS entities and Systems modeling has been an active field of study for resource influences between them. The language features decades. Our research touches many areas of the modeling state-based entity behavior and continuous resource trans- domain for instance concurrency, transaction and composi- fers. Through CREST’s homogeneous entity definition, the tion [1], [2]. We give an excerpt of related works. language encourages modular system-of-systems designs. While in the software area UML 2 [3] or SysML [4] are We will introduce CREST’s features using a plant commonly used, the modeling of hardware behavior requires growing system. This setup consists of several components additional information. MARTE [5] has been used to model (growing lamp, plant) and different kinds of resources (light, real-time behavior, timing constraints and similar embedded heat, electricity) that are transferred. Figure 1 shows a systems concepts. MARTE is a powerful means to model schematic representation of this scenario. Within we find hardware and software platforms but features a very broad hierarchical components, continuous value updates, discrete spectrum of concepts and diagrams. behavior and conversions between physical units. For ex- Architecture Description Languages (ADLs) have been ample, the lamp’s output, measured in lumen, influences the used to describe the connections of components using con- plant’s light input, which is measured in lux. The calculation nectors and interfaces. There are several well-known rep- of the light impact requires various parameters such as resentatives for ADLs similar to CREST, which have been distance, illuminated surface and illumination angle. employed for CPS. AADL [6] is very powerful and allows While usually a CPS model’s purpose is simulation, analyses for feasibility, optimization, timing of compositions CREST additionally aims to provide various other usage of hard- and software. π -ADL [7] is based on the π -calculus possibilities. These include the validation of CPS using the and introduces typed ports and their verification. CREST mathematical equations that describe physical processes, the differs from most ADLs by providing execution semantics efficient scheduling of inputs to the system, the synthesis that allow verification and simulation, as opposed to a pure of software controllers and the formal verification of CPS. architectural description. CREST aims to facilitate CPS modeling using features Hardware modeling languages such as VHDL [8] or Ver- such as continuous evaluation of variable values, reactive ilog [9] mostly focus on low-level description of electronic resource/data passing and a system-of-systems architecture. systems. Bond graphs [10], state-space representations [11] The rest of this paper is organized as follows: Section 2 and similar allow for the precise modeling of physical reflects on the current state of the art in CPS modeling. aspects within dynamic systems. They abstract away from Growing lamp room temperature + 4 electricity: temperature: 0 (Watt) 22 (Celsius) room temp. switch = off ∨ electricity < 100 switch: on time: off (Switch) On Off +δt 0 (Time) switch = on ∧ electricity = 100 0 room temperature: light: 22 (Celsius) 0 (Lumen) 800 Figure 2: A basic CREST entity with three inputs, two outputs, two states and transitions, one local and update functions real-world representation and describe pure physical system Entities are graphically depicted as CREST diagrams. behavior. They however require a precise knowledge of the The model for our system’s growing lamp is presented exact behavior. Further, it is difficult to represent real-world in Figure 2. The lamp’s interface is defined by its inputs systems that are influenced by digital information or on/off (switch and electricity) and outputs switches for example. (temperature and light), which respectively represent There exists a plethora of tools for the design, simulation the sources and targets of resource or signal transfers be- and analysis for embedded systems and models. Examples tween entities. Each of these so-called ports is linked to a are Ptolemy II [12], 20-sim [13] and Simulink [14]. They resource and has a value from the resource’s domain. support of a wide variety of different systems and offer An entity’s behavior is specified by an automaton (or a large libraries of pre-defined entities and components. In our formalism that maps to automata, e.g. Petri nets to model use-case they present themselves as potential simulation and concurrency), consisting of states and transitions. Our lamp state-space exploration platforms. has two states: Off and On, a short arrow points to the Finally we relate our approach to the Discrete EVent initial/current state. Transitions are represented as arrows be- System specification (DEVS) [15]. DEVS can be used to tween states and annotated with guard conditions (Boolean model discrete event systems using time stamps. It fea- queries on port values). Transitions trigger as soon as their tures hierarchical composition and internally uses a state- guards evaluate to true. based approach. Information between subsystems is passed Internally the lamp defines a third type of port, namely through events and transitions fire according to an internal a local variable , that can be used to store information. time advance function or external events. Due to its nature Locals can only be accessed by the entity itself. The lamp continuous value updates or internal events are not possible. defines on time to measure the total amount of time it CREST uses specific terms such asentities, influences was turned on. Local port and output values can be changed and resources for domain concepts. They might be related to using update functions ( ). These functions are continu- concepts of other, more generic languages (e.g. components, ously evaluated if the automaton is in the corresponding connections, types). As CREST is a DSL however, we state. In order to allow analysis and verification of CREST choose to use terminology that closely describes its purpose. models, updates have access to a δ t variable that represents the duration since the last call of the update. This permits simulation (value discretization by time steps) and verifi- 3. CREST Language cation (topological discovery of the significant behaviour times). This aspect of the modeling makes link between To satisfy the need for a continuous, reactive language continous and discrete aspect of time. we developed CREST. CREST has three main notions: Entities can be grouped together within an enclosing resources, defining measurement units and the domains that entity. A system is thus a hierarchical system-of-systems values can take, entities, representing physical or logical and represented by one “parent”-entity. Figure 3 displays the objects, and influences, modeling relations between entities. plant growing system, an example for such a composition. Resources are value types such as physical units or sig- A composed entity can, additionally to the already intro- nals that can be transferred using influences. In our system duced features (ports, locals, automaton), use other entities we use several resources for modeling data transfers, such as subentities. The subentities’ interfaces are linked via as Time (value domain: R+ ) for time measures in hours, influences. Influences link between child-entity interfaces, as Lumen (N) for luminous flux, Switch ([On,Off]) for an well as between the parent’s ports and the ports of its direct electrical device’s switch. children. As influences denote the transfer of resources, it is Plant growing system room temperature 22 (Celsius) SPLIT Growing lamp room temperature temperature 22 (Celsius) 22 (Celsius) MAX switch switch off (Switch) off (Switch) ADD electricity electricity light lamp 0 (Watt) 0 (Watt) 0 (Lumen) 0 (Lumen) add light external 0 (lux) 0 (Lux) Plant lamp/0.25 +external light light 0 (Lux) 0 (Lux) temperature 22 (Celcius) Figure 3: An entity that is composed of two subentities. To increase legibility the internal behavior of the Growing lamp, Plant, SPLIT and MAX was omitted. the responsibility of the modeler to specify a transformation When it comes to compatibility of interfaces we require of the source’s resource to the target’s resource. Also note, two consistency properties. Firstly, the number of required that CREST only permits a maximum of one input and and provided ports needs to be consistent. This means that output per interface port. This is uncommon for modeling an entity can be replaced if it requires the same number or languages which usually define specific connectors (e.g. less input ports and if it provides at least the same outputs additive, averaging) for such cases. To overcome this re- that the original entity provided. The reasoning is that in striction we define logical entities (entities without real-life order to define a sound replacement a new component must counterpart) such as splitters, adders and similar to divide not specify more requirements or provide less services than and combine resource signals. This constraint facilitates the original. This concept resembles a form of subtyping analyzability and verification of CREST models. relationship that is well-known in the software engineering In the example in Figure 3, the growing lamp’s light domain as Liskov’s substitution principle [17]. output is specified in lumen, but the plant’s input in lux. Figure 4a depicts an example of an entity with two inputs The plant’s total light exposure is the lamp’s lumen value and two outputs. Of the four candidates for replacement only divided by the illuminated surface (0.25 m2 ), added to 4b and 4e are directly acceptable as replacements since they the external light. The calculation is performed in a require fewer or provide more services to the system. 4c logical entity ADD (dashed edge). It features one state demands an interface that might not be available and 4d (add) and one update function that continuously modifies does not provide an output that is potentially required. The the output value. Figure 3 shows two more logical entities two rejected entities can be used if the former’s new input (split and max) that send signals to multiple targets is optional (e.g. a port for optional debug information) and and select the highest value, respectively. These are, due the latter’s missing output was not connected to any other to spatial constraints, displayed in abstract form as dashed entity. circles. Secondly, all inputs and outputs need to accept and provide the same values as the original, respectively. 4. Entity Compatibility and Replacement 5. CREST Formalization CREST’s modularity and hierarchical specification con- cept facilitates the reuse, exchange and modification of In the following section we provide the formal definition systems. When it comes to replacing an entity with another of a CREST model. While the graphical notation is primarily component it is important to assert the interface compatibil- used for system development, we provide the syntax below ity.1 in a top-down approach. 1. We do not discuss behavioral or semantic compatibility, as e.g. We define a system to be a quadruple hT, R, E, ei, where described in [16]. T is the system’s time-base values (e.g. T = [0, inf) ), R is X X (b) Fewer (c) More (d) Fewer (e) More inputs inputs outputs outputs (a) Original Figure 4: An entity with two inputs and outputs (a) and several replacement candidates (b) - (e) a set of resource types, E a set of entities within the system, Updates assign a function name to a state. The cor- as defined inductively below, and e ∈ E , the system’s root responding functions continuously modify local variables element. Below we introduce several classical notations. and output values as time passes in a state. An update’s evaluation is applied to binding, a port (either output or Definition 1. Resources are defined by a set of resource local), and an elapsed time. The evaluation returns the types R = {R1 , . . . Rn }. Each type Ri represents a set computed value for the port. of possible values for a specific resource unit, for instance electricity in Watts or the state of a switch (on/off). The set Definition 7. The updates of an entity e are given by Ue : Se → Fe , where Fe is the set of function names 2 . F of all resource values R is defined as R = i Ri . Evaluation is performed by: The distinction of both the resource type (electricity) and its unit (Watts) is important to avoid conversion problems, eval : Fe × Be × (Oe ∪ Le ) × T → R which are known to create failures in CPS, such as in the b, p, t 7→ resource(p) Mars Climate Orbiter [18]. Each e ∈ E within the set of entities E describing the where b is a binding, p a local or output port and t the time system is defined as: that has passed since the last update. All applicable updates are performed concurrently, updating their referenced ports Definition 2. e = hPe , resourcee , T Se , Ue , entitiese , Infe i, at the same time. where T Se is a transition system, Ue the update functions and Infe the influences within e. An entity’s direct subentities are defined by the entities function. An entity e’s set of ports (Pe ) is the disjoint union of inputs, outputs and locals. Each port is assigned a resource Definition 8. entities : E → P(E), where P(E) is the using a resource function. power-set of E . Definition 3. Pe = Ie t Oe t Le , where Ie are inputs, Oe We also demand that the subentity structure forms a outputs and Le local variables. The function (resource : rooted tree. PE → R) assigns a resource to each port. The composition of entities is based on the concept of influences. Influences represent resource/signal transfers Entity behavior is defined by a transition system TS of between and entity’s ports and its subentities’ ports and states and transitions. amongst an entity’s subentity ports. Formally, an entity e’s Definition 4. TS = hSe , →e i, where Se are the entity’s influences Infe is a function that, given two ports, returns a states, and →e is guarded transition relation between states translation function between source’s values to the target’s (→e ⊆ Se × Se × Ge ). values. Guards Ge are function names whose corresponding Definition 9.     functions can be evaluated using a function eval. An eval- [ [ uation with a binding the function returns a Boolean value. Inf e : Ie ∪ Oe0  × Oe ∪ Ie0  → Te e0 ∈entities(e) e0 ∈entities(e) Definition 5. eval : Ge × Be → B. where Te is a homomorphism between the source s and We do not provide a full syntax for guards here, due target t of the resources: to spatial constraints. We impose no limitation on guard expressions, as long as they return boolean values. T : R → R, s.t. Bindings Be are total functions mapping ports to cor- Definition 10. The signature of the translation function must rectly typed resource values. conform to the resources in the ports of the influence, thus Definition 6. The set of possible bindings Be is defined as ∀hs, ti 7→ f ∈ Infe , f : resource(s) → resource(t) the set of possible mappings: 2. Graphical CREST can annotate updates with the function itself instead Be : Pe → R s.t. ∀p ∈ Pe , p 7→ r ∈ resource(p) of its name. We demand ports to only have one incoming and one 6.3. Simulation, Planning, Optimization outgoing influence. ∀p, While the execution of an individual entity’s model  q ∈ Pe :    might be used for behaviour visualization, CREST’s goal |hp, x, yi ∈ Infe | ≤ 1 ∧ |hx, q, yi ∈ Infe | ≤ 1 is to aid the development of multi- and many-entity assem- This increases uniformity as signal splitters and combi- blies. Simulation of such compositions can help system ar- nators have to be modeled as (logical) entities instead of chitects discover optimized parameters within a state-space. separate port behavior. Applied on the plant growing example a simulation can Semantics. CREST’s formal semantics are beyond provide lamp schedules to optimize electricity consumption the scope of this publication. We will however outline it or lamp placements for ideal light exposure. CREST models as follows: An entity’s behavior is controlled by reactive can be translated to existing formalisms and simulation port observation, continuous update function execution and platforms such as 20-sim and Simulink. transition guard evaluation. The inter-entity semantics link The scheduling of actions can also be expressed as a ports and modify resource transfers using influence func- planning domain. In the context of the International Plan- tions, such as the lumen-lux conversion. ning Competition (IPC) the Planning Domain Definition Language (PDDL) [20] was defined to standardize their 6. Advanced Usage of CREST definition. CREST models can be translated to PDDL (after discretization) in which scheduling and optimization prob- While the modeling and graphical visualization of CPS lems can be solved. greatly facilitate communication and clarify the flow of resources throughout the system, CREST aims to address 7. Conclusions & Future Work some even more important purposes. This paper introduces CREST, a domain-specific lan- 6.1. Validation guage for the modeling of continuous, reactive systems. CREST focuses on modeling the physical transmission of CREST was designed with validation in mind. The con- resources and signals between system entities. It features cept of specifying a continuous system using mathematical automata for the representation of entity states and in- equations (in update functions and guard conditions) instead put/output ports for the transfer of information. Using a of defining state transitions based on pre-defined time ad- reactive mapping of port values and continuous variable vance functions (as in DEVS for instance), allows for the updates, a discretization of behavior, as in other formalisms, calculation of the exact moment when a guard condition is avoided. In fact, a discretization is only needed for the is satisfied. An example for this is the calculation of the execution and simulation of the model. time when a transition fires. Assuming a water tank entity CREST’s hierarchical, composition-based approach al- that changes to state full when a local variable reaches a lows developers to create models that closely reflect a real- certain value. CREST can continuously track the fill-level world system. This feature facilitates extension and re-use over time (fill-level = water in∗δt) and trigger the transition of models, and the exchange of subsystems. as soon as the guard condition applies. Discrete formalisms The language is an ideal basis for further research. on the contrary only provide certain time slots to test guard In particular, we aim to advance our efforts into area of conditions. automatic model validation. Next to that, our efforts go For the validation of CREST behavior, i.e. the automa- towards automatic synthesis of control software that allow ton, we intend the use of region-based verification, as known for system optimizations. This means that an eventual con- in timed automata [19]. By splitting the variable value troller should operate autonomously and perform choices space into equivalence regions, using the guard conditions as that will optimize a choice of parameters in the system. Such discriminator one can reduce the number of testing regions. optimizations include the creation of best operation condi- tions for all entities or the minimization of resource usage. 6.2. Controller Synthesis Extensions of this approach could involve the addition of learning models that adapt the entity’s behavior according Based on the behavior information encoded within a to lessons learned. An example is a growing system where CREST model we plan on synthesizing software controllers a plant is monitored and the plant model adapted according that manage the dynamic behavior of the system. As visi- to the observations. ble in the plant growing system, certain inputs (e.g. lamp and heating switches) and outputs (electricity consumption, temperature readings, light exposure) would usually be read and set by a software program. These readings and controls Acknowledgements could be displayed via a user interface in the form of a su- This project is supported by: FNRS STRATOS : Strategy pervisory controls and data acquisition (SCADA) software, based Term Rewriting for Analysis and Testing Of Software, or, be used to autonomously issue system commands for Hasler Foundation, 1604 CPS-Move and COST IC1404: predefined programs. MPM4CPS References [11] K. Hangos, R. Lakner, and M. Gerzson, Intelligent Control Systems: An Introduction with Examples, ser. Applied Optimization. Springer, 2001. [1] O. Biberstein, D. Buchs, and N. Guelfi, “Object-oriented nets with algebraic specifications: The CO-OPN/2 formalism,” in Advances in [12] C. Ptolemaeus, Ed., System Design, Modeling, and Simulation Petri Nets on Object-Orientation, ser. LNCS. Springer, 2001, pp. using Ptolemy II. Ptolemy.org, 2014. [Online]. Available: http: 70–127. //ptolemy.org/books/Systems [2] D. Buchs, S. Chachkov, and D. Hurzeler, “Modelling a Secure, Mobile [13] C. Products, “20-sim,” http://www.20sim.com/, 2017, accessed: 2017- and Transactional System with CO-OPN,” in Proc. Int. Conf. on 07-12. Application of Concurrency to System Design, Guimarães, Portugal. [14] MathWorks, “Simulink: Getting Started Guide, Accessed: 2017-07- IEEE CS Press, 2003, pp. 82–91. 12,” http://www.mathworks.com/help/pdf\ doc/simulink/sl\ gs.pdf, 2017. [3] Object Management Group, Unified Modeling Language (UML) Spec- ification. Version 2.5, Mar. 2015, OMG Document formal/2015-03- [15] B. P. Zeigler, Multifaceted Modelling and Discrete Event Simulation. 01. London: Academic Press, 1984. [4] ——, OMG Systems Modeling Language. Version 1.5, May 2017, [16] M. Weidlich, R. Dijkman, and M. Weske, Deciding Behaviour Com- OMG Document formal/2017-05-01. patibility of Complex Correspondences between Process Models. Springer Berlin Heidelberg, 2010. [5] ——, UML Profile for MARTE: Modeling and Analysis of Real- Time Embedded Systems. Version 1.1, Jun. 2011, OMG Document [17] B. H. Liskov and J. M. Wing, “A Behavioral Notion of Subtyping,” formal/2011-06-02. ACM Trans. Program. Lang. Syst., vol. 16, no. 6, pp. 1811–1841, Nov. 1994. [6] P. Feiler, D. Gluch, and J. Hudak, “The Architecture Analysis & Design Language (AADL): An Introduction,” Software Engineering [18] Mars Climate Orbiter Mishap Investigation Board, “Mars Climate Or- Institute, Carnegie Mellon University, Tech. Rep. CMU/SEI-2006- biter Mishap Investigation Board Phase I Report,” NASA, Technical TN-011, 2006. report, 1999. [19] R. Alur and D. L. Dill, “A theory of timed automata,” Theoretical [7] F. Oquendo, “Pi-ADL: an Architecture Description Language based Computer Science, vol. 126, no. 2, pp. 183–235, Apr. 1994. on the higher-order typed pi-calculus for specifying dynamic and mobile software architectures,” SIGSOFT Softw. Eng. Notes, pp. 1–14, [20] D. McDermott, M. Ghallab, A. Howe, C. Knoblock, A. Ram, 2004. M. Veloso, D. Weld, and D. Wilkins, “PDDL - The Planning Domain Definition Language,” Yale Center for Computational Vision and [8] P. J. Ashenden, The Designer’s Guide to VHDL, 3rd ed. San Control, Tech. Rep., 1998. Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 2008. [9] D. Thomas and P. Moorby, The Verilog Hardware Description Lan- guage, ser. The Verilog Hardware Description Language. Kluwer Academic Publishers, 1996. [10] H. Paynter, Analysis and Design of Engineering Systems: Class Notes for M.I.T. Course 2,751. M.I.T. Press, 1961.