=Paper=
{{Paper
|id=Vol-2019/gemoc_2
|storemode=property
|title=CREST - A Continuous, REactive SysTems DSL
|pdfUrl=https://ceur-ws.org/Vol-2019/gemoc_2.pdf
|volume=Vol-2019
|authors=Stefan Klikovits,Alban Linard,Didier Buchs
|dblpUrl=https://dblp.org/rec/conf/models/KlikovitsLB17
}}
==CREST - A Continuous, REactive SysTems DSL==
https://ceur-ws.org/Vol-2019/gemoc_2.pdf
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.