-The advance of cyber-physical systems in everyday life requires powerful modeling capabilities. Existing formalisms often have severe limitations and require complicated notations. In this paper we introduce CREST, a domain-specific language for modeling entity behavior and resource transfers in CPS. CREST aims to support CPS architects through clarity, comprehensiveness and analyzability. 1. Introduction & Motivation
The advance of cyber-physical systems (CPS), unions of hardware sensors and actuators and software controllers, emphasizes the importance of analysis, validation and verification of such systems. The complexity of CPS often lies in their systems-of-systems architecture and mutual subsystem influences. The analysis and development of CPS require a clear and comprehensive means of modeling.
In this paper we introduce CREST, a domain-specific language (DSL) for continuous and reactive systems. CREST focuses on the specification of CPS entities and resource influences between them. The language features state-based entity behavior and continuous resource transfers. Through CREST’s homogeneous entity definition, the language encourages modular system-of-systems designs.
We will introduce CREST’s features using a plant growing system. This setup consists of several components (growing lamp, plant) and different kinds of resources (light, heat, electricity) that are transferred. Figure 1 shows a schematic representation of this scenario. Within we find hierarchical components, continuous value updates, discrete behavior and conversions between physical units. For example, the lamp’s output, measured in lumen, influences the plant’s light input, which is measured in lux. The calculation of the light impact requires various parameters such as distance, illuminated surface and illumination angle.
While usually a CPS model’s purpose is simulation, CREST additionally aims to provide various other usage possibilities. These include the validation of CPS using the mathematical equations that describe physical processes, the efficient scheduling of inputs to the system, the synthesis of software controllers and the formal verification of CPS. CREST aims to facilitate CPS modeling using features such as continuous evaluation of variable values, reactive resource/data passing and a system-of-systems architecture.
The rest of this paper is organized as follows: Section 2 reflects on the current state of the art in CPS modeling. Sun
Growlamp Plant
Power mains
Room temperature Section 3 introduces CREST and its graphical language. Section 4 outlines rules for exchange and re-use of CREST components. Section 5 formalizes CREST’s syntax. Section 6 explains how to use CREST for validation, simulation, planning and controller synthesis and Section 7 concludes.
Systems modeling has been an active field of study for decades. Our research touches many areas of the modeling domain for instance concurrency, transaction and composition [1], [2]. We give an excerpt of related works.
While in the software area UML 2 [3] or SysML [4] are commonly used, the modeling of hardware behavior requires additional information. MARTE [5] has been used to model real-time behavior, timing constraints and similar embedded systems concepts. MARTE is a powerful means to model hardware and software platforms but features a very broad spectrum of concepts and diagrams.
Architecture Description Languages (ADLs) have been used to describe the connections of components using connectors and interfaces. There are several well-known representatives for ADLs similar to CREST, which have been employed for CPS. AADL [6] is very powerful and allows analyses for feasibility, optimization, timing of compositions of hard- and software. -ADL [7] is based on the -calculus and introduces typed ports and their verification. CREST differs from most ADLs by providing execution semantics that allow verification and simulation, as opposed to a pure architectural description.
Hardware modeling languages such as VHDL [8] or
Verilog [9] mostly focus on low-level description of electronic
systems. Bond graphs [
On
room temperature + 4 switch = off _ electricity < 100 switch = on ^ electricity = 100 800
Off room temp.
+ t 0 temperature: 22 (Celsius) on time: 0 (Time)
light: 0 (Lumen) real-world representation and describe pure physical system behavior. They however require a precise knowledge of the exact behavior. Further, it is difficult to represent real-world systems that are influenced by digital information or on/off switches for example.
There exists a plethora of tools for the design, simulation
and analysis for embedded systems and models. Examples
are Ptolemy II [
Finally we relate our approach to the Discrete EVent
System specification (DEVS) [
CREST uses specific terms such asentities, influences and resources for domain concepts. They might be related to concepts of other, more generic languages (e.g. components, connections, types). As CREST is a DSL however, we choose to use terminology that closely describes its purpose.
To satisfy the need for a continuous, reactive language we developed CREST. CREST has three main notions: resources, defining measurement units and the domains that values can take, entities, representing physical or logical objects, and influences, modeling relations between entities.
Resources are value types such as physical units or signals that can be transferred using influences. In our system we use several resources for modeling data transfers, such as Time (value domain: R+) for time measures in hours, Lumen (N) for luminous flux, Switch ([On,Off]) for an electrical device’s switch.
Entities are graphically depicted as CREST diagrams. The model for our system’s growing lamp is presented in Figure 2. The lamp’s interface is defined by its inputs (switch and electricity) and outputs (temperature and light), which respectively represent the sources and targets of resource or signal transfers between entities. Each of these so-called ports is linked to a resource and has a value from the resource’s domain.
An entity’s behavior is specified by an automaton (or a formalism that maps to automata, e.g. Petri nets to model concurrency), consisting of states and transitions. Our lamp has two states: Off and On, a short arrow points to the initial/current state. Transitions are represented as arrows between states and annotated with guard conditions (Boolean queries on port values). Transitions trigger as soon as their guards evaluate to true.
Internally the lamp defines a third type of port, namely a local variable , that can be used to store information. Locals can only be accessed by the entity itself. The lamp defines on time to measure the total amount of time it was turned on. Local port and output values can be changed using update functions ( ). These functions are continuously evaluated if the automaton is in the corresponding state. In order to allow analysis and verification of CREST 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 verification (topological discovery of the significant behaviour times). This aspect of the modeling makes link between continous and discrete aspect of time.
Entities can be grouped together within an enclosing entity. A system is thus a hierarchical system-of-systems and represented by one “parent”-entity. Figure 3 displays the plant growing system, an example for such a composition. A composed entity can, additionally to the already introduced features (ports, locals, automaton), use other entities as subentities. The subentities’ interfaces are linked via influences. Influences link between child-entity interfaces, as well as between the parent’s ports and the ports of its direct children. As influences denote the transfer of resources, it is room temperature 22 (Celsius)
SPLIT
the responsibility of the modeler to specify a transformation of the source’s resource to the target’s resource. Also note, that CREST only permits a maximum of one input and output per interface port. This is uncommon for modeling languages which usually define specific connectors (e.g. additive, averaging) for such cases. To overcome this restriction we define logical entities (entities without real-life counterpart) such as splitters, adders and similar to divide and combine resource signals. This constraint facilitates analyzability and verification of CREST models.
In the example in Figure 3, the growing lamp’s light output is specified in lumen, but the plant’s input in lux. The plant’s total light exposure is the lamp’s lumen value divided by the illuminated surface (0:25 m2), added to the external light. The calculation is performed in a logical entity ADD (dashed edge). It features one state (add) and one update function that continuously modifies the output value. Figure 3 shows two more logical entities (split and max) that send signals to multiple targets and select the highest value, respectively. These are, due to spatial constraints, displayed in abstract form as dashed circles.
CREST’s modularity and hierarchical specification concept facilitates the reuse, exchange and modification of systems. When it comes to replacing an entity with another component it is important to assert the interface compatibility.1
1. We do not discuss behavioral or semantic compatibility, as e.g.
described in [
When it comes to compatibility of interfaces we require
two consistency properties. Firstly, the number of required
and provided ports needs to be consistent. This means that
an entity can be replaced if it requires the same number or
less input ports and if it provides at least the same outputs
that the original entity provided. The reasoning is that in
order to define a sound replacement a new component must
not specify more requirements or provide less services than
the original. This concept resembles a form of subtyping
relationship that is well-known in the software engineering
domain as Liskov’s substitution principle [
Figure 4a depicts an example of an entity with two inputs and two outputs. Of the four candidates for replacement only 4b and 4e are directly acceptable as replacements since they require fewer or provide more services to the system. 4c demands an interface that might not be available and 4d does not provide an output that is potentially required. The two rejected entities can be used if the former’s new input is optional (e.g. a port for optional debug information) and the latter’s missing output was not connected to any other entity.
Secondly, all inputs and outputs need to accept and provide the same values as the original, respectively.
In the following section we provide the formal definition of a CREST model. While the graphical notation is primarily used for system development, we provide the syntax below in a top-down approach.
We define a system to be a quadruple hT; R; E ; ei, where T is the system’s time-base values (e.g. T = [0; inf ) ), R is (b) Fewer inputs (c) More inputs (d) Fewer outputs (e) More outputs (a) Original a set of resource types, E a set of entities within the system, as defined inductively below, and e 2 E , the system’s root element. Below we introduce several classical notations. Definition 1. Resources are defined by a set of resource types R = fR1; : : : Rng. Each type Ri represents a set of possible values for a specific resource unit, for instance electricity in Watts or the state of a switch (on/off). The set of all resource values R is defined as R = Fi Ri.
The distinction of both the resource type (electricity) and
its unit (Watts) is important to avoid conversion problems,
which are known to create failures in CPS, such as in the
Mars Climate Orbiter [
Each e 2 E within the set of entities E describing the system is defined as: Definition 2. e = hPe; resourcee; T Se; Ue; entitiese; I nfei, where T Se is a transition system, Ue the update functions and I nfe the influences within e.
An entity e’s set of ports (Pe) is the disjoint union of inputs, outputs and locals. Each port is assigned a resource using a resource function.
Definition 3. Pe = Ie t Oe t Le, where Ie are inputs, Oe outputs and Le local variables. The function (resource : PE ! R) assigns a resource to each port.
Entity behavior is defined by a transition system TS of states and transitions. (!e Definition 4. TS = hSe; !ei, where Se are the entity’s states, and !e is guarded transition relation between states
Se Se Ge).
Guards Ge are function names whose corresponding functions can be evaluated using a function eval. An evaluation with a binding the function returns a Boolean value.
Be ! B.
We do not provide a full syntax for guards here, due to spatial constraints. We impose no limitation on guard expressions, as long as they return boolean values.
Bindings Be are total functions mapping ports to correctly typed resource values.
Definition 6. The set of possible bindings Be is defined as the set of possible mappings:
Be : Pe ! R s.t. 8p 2 Pe; p 7! r 2 resource (p) Updates assign a function name to a state. The corresponding functions continuously modify local variables and output values as time passes in a state. An update’s evaluation is applied to binding, a port (either output or local), and an elapsed time. The evaluation returns the computed value for the port.
Definition 7. The updates of an entity e are given by Ue : Se ! Fe, where Fe is the set of function names 2. Evaluation is performed by: eval : Fe
Be (Oe [ Le)
T ! R b; p; t 7! resource (p) where b is a binding, p a local or output port and t the time that has passed since the last update. All applicable updates are performed concurrently, updating their referenced ports at the same time.
An entity’s direct subentities are defined by the entities function.
Definition 8. entities : E ! P (E), where P (E) is the power-set of E.
We also demand that the subentity structure forms a rooted tree.
The composition of entities is based on the concept of influences. Influences represent resource/signal transfers between and entity’s ports and its subentities’ ports and amongst an entity’s subentity ports. Formally, an entity e’s influences I nfe is a function that, given two ports, returns a translation function between source’s values to the target’s values.
0 1 0 1 Inf e : @Ie [ Oe0 A e02entities(e) [
[ @Oe [ Ie0 A ! Te e02entities(e) where Te is a homomorphism between the source s and target t of the resources:
T : R ! R; s :t : Definition 10. The signature of the translation function must conform to the resources in the ports of the influence, thus 8hs; ti 7! f 2 I nfe; f : resource (s) ! resource (t) 2. Graphical CREST can annotate updates with the function itself instead of its name.
We demand ports to only have one incoming and one outgoing influence.
8p; q 2 Pe : jhp; x; yi 2 Infej 1 ^ jhx; q; yi 2 Infej 1
This increases uniformity as signal splitters and combinators have to be modeled as (logical) entities instead of separate port behavior.
Semantics. CREST’s formal semantics are beyond the scope of this publication. We will however outline it as follows: An entity’s behavior is controlled by reactive port observation, continuous update function execution and transition guard evaluation. The inter-entity semantics link ports and modify resource transfers using influence functions, such as the lumen-lux conversion.
While the modeling and graphical visualization of CPS greatly facilitate communication and clarify the flow of resources throughout the system, CREST aims to address some even more important purposes.
CREST was designed with validation in mind. The concept of specifying a continuous system using mathematical equations (in update functions and guard conditions) instead of defining state transitions based on pre-defined time advance functions (as in DEVS for instance), allows for the calculation of the exact moment when a guard condition is satisfied. An example for this is the calculation of the time when a transition fires. Assuming a water tank entity that changes to state full when a local variable reaches a certain value. CREST can continuously track the fill-level over time (fill-level = water in t) and trigger the transition as soon as the guard condition applies. Discrete formalisms on the contrary only provide certain time slots to test guard conditions.
For the validation of CREST behavior, i.e. the
automaton, we intend the use of region-based verification, as known
in timed automata [
Based on the behavior information encoded within a CREST model we plan on synthesizing software controllers that manage the dynamic behavior of the system. As visible 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 could be displayed via a user interface in the form of a supervisory controls and data acquisition (SCADA) software, or, be used to autonomously issue system commands for predefined programs.
While the execution of an individual entity’s model might be used for behaviour visualization, CREST’s goal is to aid the development of multi- and many-entity assemblies. Simulation of such compositions can help system architects discover optimized parameters within a state-space. Applied on the plant growing example a simulation can provide lamp schedules to optimize electricity consumption or lamp placements for ideal light exposure. CREST models can be translated to existing formalisms and simulation platforms such as 20-sim and Simulink.
The scheduling of actions can also be expressed as a
planning domain. In the context of the International
Planning Competition (IPC) the Planning Domain Definition
Language (PDDL) [
This paper introduces CREST, a domain-specific language for the modeling of continuous, reactive systems. CREST focuses on modeling the physical transmission of resources and signals between system entities. It features automata for the representation of entity states and input/output ports for the transfer of information. Using a reactive mapping of port values and continuous variable updates, a discretization of behavior, as in other formalisms, is avoided. In fact, a discretization is only needed for the execution and simulation of the model.
CREST’s hierarchical, composition-based approach allows developers to create models that closely reflect a realworld system. This feature facilitates extension and re-use of models, and the exchange of subsystems.
The language is an ideal basis for further research. In particular, we aim to advance our efforts into area of automatic model validation. Next to that, our efforts go towards automatic synthesis of control software that allow for system optimizations. This means that an eventual controller should operate autonomously and perform choices that will optimize a choice of parameters in the system. Such optimizations include the creation of best operation conditions for all entities or the minimization of resource usage. Extensions of this approach could involve the addition of learning models that adapt the entity’s behavior according to lessons learned. An example is a growing system where a plant is monitored and the plant model adapted according to the observations.
This project is supported by: FNRS STRATOS : Strategy based Term Rewriting for Analysis and Testing Of Software, Hasler Foundation, 1604 CPS-Move and COST IC1404: MPM4CPS