Pragmatic reuse for DSML development

An alternative approach to employing expert modellers is to allow domain users to model their systems themselves. To do so, they require means that are understandable even without extensive systems engineering training, experience or modeling knowledge. As displayed in Fig. 1, these approaches still operate on a generic level, but usually provide helpful features for the representation of system engineering concerns. Modeling languages such as the Unified Modeling Language (UML) [64], the Specification and Description Language (SDL) [48] or Modelica [34] raise the abstraction level and bring models closer to the system domains. They allow convenient abstractions to improve system design and reasoning, while still offering translation to various low-level formalisms or directly to software source code. However, even though these languages allow systems to be modelled at an abstraction level that is closer to the original, they tend to be still very generic and involve steep learning curves. For instance, users usually require several months of continuous exposure before they become proficient with UML [33]. This means that the main users of these languages tend to be professional system developers, rather than domain end-users, i.e. the people who will actually build and use the system on a daily basis. In fact, to enable domain users to also model their own systems, it is necessary to provide them with the capability to use modeling tools that operate in the system domain level, using the concepts, terminology and tools that the users are already familiar with. This approach removes steep learning curves and avoids the risk of confusion and misconceptions.

In the last few decades, this final domain-adaptation step has evolved in several forms, as shown in Fig. 1. A common approach is to adapt an existing modeling language by altering its concrete syntax (and sometimes its semantics) to more closely represent the features found in the actual system domain. Business process management models [78], for example, are inspired by Petri nets and allow the modeling and analysis of business workflows. The matching BPMN [62] language offers a graphical interface for simplified representation. In a similar way, the Architecture Analysis and Design Language (AADL) [75] can be extended using the AADL annex mechanism. Such annexes can be used to add discrete behaviour [29], continuous behaviour [2] or error modeling capabilities [23] to the language. UML can be adapted to various domains using UML profiles [36], a UML-native means to extend and adapt the language. The UML Profile for Modeling and Analysis of Real Time and Embedded systems (MARTE) [63] for instance, is an extension of standard UML that offers concepts for the modeling of real-time applications. The Systems Modeling Language (SysML) [65] is a well-known adaptation of UML that alters and extends a specific subset of UML to allow dedicated systems engineering. However, both SysML and MARTE can be seen as generic languages themselves, as they are not applicable to a specific target domain. A more concrete experience report of using UML profiles for implementing domain-specific modeling is described in [25], where the authors adapt the language specifically for robotic applications.

Another approach to incorporate domain knowledge into a modeling tool or language is the use of tool libraries. Especially when using versatile modeling platforms such as Simulink or Ptolemy II, it is possible to create domain libraries that aid users by providing reusable APIs or objects. The Modelica language is well-known for its large number of object libraries,¹ that add capabilities to model specific domains such as chemical processes, hydraulic flows or power systems.

A third method to close the semantic gap between model and domain is to create a dedicated modeling language for a specific target domain or application [69]. DSLs [80] raise the abstraction level of system models to facilitate model creation and reasoning, while at the same time hiding the underlying complexity of the modeling process. Ideally, this leads to DSLs that allow domain users to easily perform all their tasks using pre-existing knowledge and without the need to newly familiarise themselves with a tool or language. This increases productivity and makes the language easier to comprehend [39]. Language engineering experts work in concert with domain users to learn about their needs and trim the DSL according to these requirements. Hidden behind the DSL, the data are then executed using purpose-built tools or translated to other, well-established modeling languages in order to use already existing execution software. The recent popularity of DSLs is manifested in the numerous conferences and workshops organised on the topic, and seminal books such as [80] and  [28] show that the field is reaching maturity, with established best practices, available experience reports and educational resources. Despite all the benefits that they bring, the classical language engineering approach comes with a hefty price tag [79]. DSLs require a significant upfront investment into the initial creation and subsequent maintenance of their infrastructure [24]. Even small DSLs need at least the provision of a parser, a text editor and an execution engine or code generator (i.e. a translator to another language). Larger projects often require further development of a textual or graphical integrated development environment (IDE), auto-completion engines, static and dynamic code analysis tools, language and IDE versioning and version migration, interfaces to GPPLs, library support, etc. These needs and the popularity of DSLs led to the creation of language workbenches [27] such as Xtext [11], MetaEdit+ [77] and MPS [17], that promise help throughout the language design phase, but also convince through automatic out-of-the-box generation of many of the aforementioned artefacts. For instance, Xtext can generate a full-fledged IDE including parser, auto-suggestions and code analyser based on a DSL grammar alone. Its tight integration into the Eclipse Modeling Framework (EMF) [76] allows the facilitated development of code generators, model transformation engines or graphical editors for these languages. Nonetheless, even after the use of language workbenches, DSLs often require further customisation and subsequent maintenance effort that can easily become very costly in terms of time and development effort.

Internal DSLs [39] are an alternative to the creation of standalone languages where DSLs are embedded inside another, usually more generic language (e.g. a GPPL). This approach is related to the creation of tool libraries, so that it is hard to clearly distinguish between domain-specific libraries and internal DSLs. Generally, it can be said that—in contrast to tool libraries—internal DSLs tend to embed advanced features such as their own semantics inside their host languages, allowing for sound execution and verification. Further, internal DSLs often “use, and abuse, the host language” [31] by using metaprogramming, reflection and clever language tricks to implement domain-specific behaviour. Next to the reduced initial DSL development time and cost, users can rely on their pre-existing familiarity with compilers, IDE, code analysis frameworks and development best practices. Internal DSLs are usually easily extensible and integrate better into existing language infrastructure and tooling [20]. This is also reflected in their increased interoperability with other tools and third-party libraries. Depending on the particular host language, numerous software packages are available to further extend the DSL’s capabilities.

A well-known example of an internal DSLs is SystemC [12], a hardware description language that is implemented in C++and distributed as a software library. Models are created using regular C++source code that instantiates library classes and executes macros. SystemC’s semantics are implemented in a simulator module that is shipped alongside the library. Other wide-spread examples for internal DSLs include various testing frameworks (e.g. jMock [31], XUnit [8], Chai²) and extensions for programming languages such as Ruby [32] (e.g. Ruby on Rails [4]), Groovy and Scala [39].

Internal vs. External DSLs The clear advantage of using internal DSLs lies evidently in the reuse of the host language’s syntax and execution environment [38]. One disadvantage of this reuse, however, is the lack of static checking support. Internal DSLs often require models to be setup in a certain manner, use specific properties (e.g. inherit from specific base classes) or prohibit the use of some host language features (e.g. introspection, certain libraries, etc). While the lack of static checking is a DSL problem in general [44], external DSLs can benefit from static type and syntax checking offered by language workbenches. This means, that external languages can be defined to natively enforce these rules inside the parser or interpreter and display the results directly in the IDE. Internal languages on the other hand have to build these features outside of the GPPL’s infrastructure, such that users have to manually trigger syntactic and semantic sanity checks. In the best case, they might use language reflection and introspection APIs to create validation scripts and thereby inform the user of potential problems. However, typically manual execution of these scripts is required, which delays the feedback and might even cause frustration if the suggestions are incomprehensible.

Another issue might arise from choosing the wrong host language. The benefit of reusing the syntax also means that the host language’s syntax cannot be adapted or extended. For instance, Matlab requires an ellipsis (“...”) to be written at the end of each line of multi-line expressions. This feature can become problematic when designing so-called fluent interfaces that chain many method calls as described in [73]. In such situations, external DSLs show more flexibility, as they can support a highly customised syntax. The disadvantage here however often lies in the need to define the entire language and interpretation from scratch. Especially when it comes to adding “basic building blocks” such as mathematical expressions, operators, character string manipulations and type systems, the development process can easily become tedious. Modern language workbenches attempt to provide reusable blocks of syntax and grammar (e.g. Xtext’s support for Mixins and Traits [71]), but still require the execution environment to be defined and adapted for the newly created language.

Summarising, one can see that external DSLs provide more powerful, flexible and customisable features, that require time and effort to be created. Internal DSLs on the other hand take advantage of the out-of-the box features, but are limited by the host language’s syntax, execution platform and IDEs. In the end, it depends on the language developer’s insights to decide whether the benefit of a familiar GPPL syntax and cheap reuse of existing execution platforms outweighs the flexibility of external DSLs.

The approach we followed for this project is driven by the practical need of a tool or language, that brings the benefits of modeling and simulation to smaller-scale systems. While the research effort of the last few decades has produced a plethora of modeling formalisms, languages and tools that have been applied to various projects in industries such as transportation, avionics, manufacturing, heavy industry and safety-critical systems, very little effort has been made to transfer these developments to the end-user market. In particular, our target user group are creators of CPSs such as smarthomes, office automation installations and automated plant growing applications. Even though such systems usually are not classically safety-critical, i.e. do not pose harm to health or life, their correct functionality is nonetheless important. A plant watering setup that is assembled by a private end-user might cause to water spillage and break wooden floors or electrical devices, thereby creating significant financial damages. Similarly, a misconfigured office automation system that was installed by a non-expert building manager might lead to high bills if e.g. the lights and heating are run even if no employees are present. In the current situation, such users might shy away from creating their applications as the risk of faulty installations is high and they lack the time, capacity and financial means to use existing modeling and verification solutions.

Before starting the development, we first designed three case study systems that allowed us to evaluate the main requirements of resource-flow CPSs. Attention was paid to choose applications that represent the heterogeneity of our target domain. While a full description of each would exceed the scope of this article, we still provide a brief outline. A complete description of the individual case studies can be found in [50]. The three systems were designed as follows:

A comparison of these systems resulted in the discovery of two important similarities. First, the types of systems we target in our study are commonly composed of off-the-shelf components. This means, it is highly unusual that system creators use custom components. Instead, they buy devices (e.g. lamps, home appliances, IoT gadgets) according to their needs and connect them to compose their system. Second, despite modern communication interfaces, the influences between the individual components are in the physical domain. For example, a dishwasher consumes hot water and electricity, a vacuum cleaner uses electricity to clean the floor and creates noise in exchange, and plants require sunshine or artificial light on a daily basis.

Next to these two principal paradigms, we identified ten aspects that have to be supported by a modeling language or tool, in order to be able to address all necessary system concerns. These aspects can be split into two groups, such that the first seven describe “functional” properties that can be objectively analysed:

The remaining three language criteria largely depend on the target users, their pre-existing knowledge and preferences. This means that while they first seven key aspects, can be objectively evaluated, the additional criteria result from the proper integration of the key aspects and their good correspondence from a syntactic and semantic point of view. Evidently, a sound, formal language definition supports this integration.

Equipped with these ten criteria, we set out to find a suitable language for the modeling of our case study systems. However, to the best of our knowledge, we did not find any language or tool that supports all our key properties, is usable by non-experts and novice system engineers and suitable for the modeling of smaller-scale resource-flow CPSs. Existing languages and tools that offer physical resources modeling usually target expert engineers from financially potent enterprises in the industrial sector. Their typical application domains include large scale systems such as oil rigs and power plants. Other, academic tools lack usability and therefore also require a long training phase. The tools that we selected for closer evaluation represent a range of different modeing languages that are actively being used in the domain of CPS modeling. We aimed to cover a broad spectrum of approaches, covering general purpose languages (e.g. MARTE, SDL), architecture description languages (e.g. AADL [75], MontiArcAutomaton [72]), hardware description languages, synchronous programming languages (e.g. Esterel [10], Lustre [42], Zélus [13]), event-based approaches (e.g. the quantised state [54] extension of PowerDEVS [9]) and modeling platforms such as Simulink/Stateflow and Modelica. The selection is based on an informal upfront evaluation and feature comparison. For languages that are very similar, we chose the more promising candidate. Table 1 shows our evaluation based on the previously obtained requirements. It can be seen that most languages lack at least one of the key requirements. MARTE and Modelica appear to be favourable candidates, although both of them are inapt in terms of usability and suitability. MARTE for instance builds upon UML’s fourteen diagram types and requires the knowledge of even more languages such as the Object Constraint Language (OCL).⁴ This significantly expands the language’s learning phase. Furthermore, the language adds timing annotations to the system which can be (ab-)used to describe continuous variable evolution, but does not provide dedicated concepts. Modelica on the other hand provides this possibility, but requires the creation of a domain library to augment its usability for our target domain, which is a non-trivial task. Furthermore, its textual syntax is difficult to understand for newcomers and requires a lot of experience for proficiency. A more complete and detailed description of our evaluation, including discussion of the other languages and formalisms is provided in [50] and [52].

Based on the previous evaluation and the lack of an appropriate modeling language for the CPSs and system creators targeted by our research, we decided to develop CREST as a standalone project, rather than an extension or adaptation of an existing product. CREST ’s goal is to provide an easily comprehensible and usable solution to CPS modeling. Thus, for instance, from a user’s perspective, CREST should be easy to learn and use, but flexible enough to model the broad range of devices that are installed in modern smarthome and office automation projects. On the development side, we decided to reuse well-known abstractions and parts from established modeling formalisms and languages. This allows us to rely on a large body of knowledge, build on existing tools by transforming CREST models and cater to the knowledge of users with pre-existing modeling skills.

CREST ’s main purpose is to support its users through three principal modeling tasks namely, the modeling, i.e. the creation of a system model, simulation, i.e. the evaluation of dynamic runtime behaviour and verification, i.e. the formally sound evaluation whether a model can reach certain beneficial or malicious states at all.

For the modeling itself, developers require a tool or language that helps in the rapid prototyping and subsequent refinement of their system and components. The provided modeling means has to be both easy to handle and also serve as an understandable resource for discussion. During the aforementioned evaluation of other modeling languages, we observed that these two requirements are often opposing. Graphical modeling languages such as UML or SDL encode data using easily understood information such as shape, size, colour and position. Their advantage over textual languages is the facilitated comprehensibility and the quick identification of required modifications [59]. The problematic however lies behind the scene. A clear graphical syntax has to be carefully engineered [67] and the creation of complex graphical models often requires the use of cumbersome graphical editors [18] which demand manual positioning and sizing of components, drawing of connection edges and frequent switching between keyboard and mouse. Especially in the prototyping phase, where models have to be edited and redrawn frequently, the creation of graphical models can quickly become a tedious task. Figure 3 shows a screenshot of the wide-spread Papyrus Modeling Editor, a common tool for UML modeling. Note, how several views need to be used in combination for navigation and model creation.

Textual modeling languages such as Modelica and SystemC overcome these problems by using well-structured text to express system architecture and behaviour. Models encode relationships between components and subcomponents using keywords, similar to programming languages. The advantage of these types of modeling languages is the quick model creation and manipulation, since the focus remains on the actual model, rather than positioning, shape or size of its representation. They also tend to be more powerful in terms of “intelligent editors and copy&paste support” [1]. Further, they often benefit from advanced features such as IDEs, static analysis, code suggestions, as they are more easily created for textual than graphical languages. On the other hand, it is clear that textual models usually are not self-explanatory and thus require secondary notions such as accompanying documents or code comments to carry additional information for developers and users [67].

In the CREST project, we follow a pragmatic approach that resulted in the creation of a textual and a graphical language, such that their respective concrete syntax implements the same formalism. Thus they share the same abstract syntax and operational semantics. CREST diagrams, the graphical language, reuses abstractions and concrete syntax from other widespread languages to increase comprehensibility and usability. To build upon pre-existing knowledge, CREST diagrams reuse notational conventions from well-known formalisms such as automata and architecture description languages. Evidently, the language suffers from the same drawbacks as other graphical languages, in that the positioning and resizing of elements is intricate and time consuming. Thus, to increase the development speed and add the benefits from textual modeling, we created crestdsl, an internal DSL in Python. It offers the same expressive modeling power as CREST diagrams and adds reusability to the modeling by supporting classic programming concepts such as inheritance and shared code. crestdsl further poses as a flexible bridge to the implementation of advanced modeling tasks such as simulation and verification. The DSL facilitates the model creation and invites the development object and domain libraries, providing scripting APIs that also support user-developed language extensions and tooling. Due to their expressive equivalence, CREST diagrams and crestdsl models can be transformed from one representation into the other, and, crestdsl does in fact provide functionality to create interactive CREST diagrams based on its models. A discussion of the translation functionality is provided in Sect. 5. The next two sections introduce both CREST diagrams and crestdsl, and highlight our design choices.

CREST diagrams [50, 53] are a graphical modeling language geared towards usability. Its purpose is the modeling of physical resource flows between the components of CPSs. Thus, it contains dedicated features to address concerns such as continuous flows and component hierarchies. The language implements a formal syntax and structure specification that clearly states requirements and constraints of CREST models (see Appendix 1). In this section, we use CREST diagrams to introduce the structure of a typical CREST model. Note, that the CREST diagram syntax reuses modeling notions known from other modeling languages to increase familiarity.

For simplicity, CREST diagrams combine architectural and behavioural system aspects within the same language. The advantage of this approach is that especially novice modellers have all information directly displayed to them, without the need to switch between different viewpoints.

Architecturally, CREST models are primarily defined through a system structure whose components (entities) are arranged strictly hierarchically. Thus, each entity only has one parent and a CREST system has only one, single root entity that defines the system’s scope. CREST ’s behaviour description is inspired by finite state machines (FSMs) and hybrid automata. This means, that every entity defines a state-automaton that represents its behaviour modes. In each state, the system can expose different behaviour, such that a device might produce other output when it is turned on than when it is turned off, for instance.

Entities enforce CREST ’s locality requirement and hide their internal structure from the outside. Hence, an entity’s automaton states cannot be read from another entity and it is not possible that one entity’s state automaton directly influences the output of another entity. Another advantage is that within the entity hierarchy, a subentity can be treated as coherent “black box”, whose system state is always up to date and does not have pending state updates. This concept is very important for CREST ’s semantics (see Sect. 4.1), which revolve around the creation of such “stable” system states, by locally searching for fixpoints on the lowest entity levels and recursively ascending in the entity hierarchy and stabilising until the entire system is stable.

An entity’s black box view also exposes its communication interface, consisting of input ( ) and output ( ) ports. Similar to some common architecture description languages (e.g. MontiArc [40]), CREST ’s ports define which type of value they accept. These types (called resources) consist of a unit (e.g. Celsius or Lumen) and a value domain such as natural numbers \(\mathbb {N}\), real numbers \(\mathbb {R}\) or discrete sets (e.g. \(\{\text {on},\text {off}\}\)). Next to its name and resource, a port also defines its current valuation. Inputs and outputs are complemented by a third type of port: locals ( ). This port type is not part of the communication interface, but rather serves as internal storage of data.

CREST ’s behaviour definition is inspired by FSMs. Thus, each entity defines a set of states and guarded transitions (e.g. ). Transitions relate two states and a guard function, such that the automaton switches to the new state if the transition is enabled, i.e. if its guard condition holds. Usually, guard functions will access the entity’s port values for their evaluation. Note, that the locality principle is enforced here as well. Thus, to preserve consistency, transition guards can only use their own entity’s ports and the output ports of subentities for the computation.

Continuous behaviour, i.e. the flow of resources, can be modelled in several forms. The most fundamental way are update functions ( ). Updates extend the automaton behaviour in a similar way to hybrid automata (HA). However, instead of defining each variable’s rate in each state (as in HA), updates only modify specific port values. Specifically, an update relates a function to an automaton state and a target port, such that the function is continuously executed while the automaton is in its related state and the result is written to the port. For instance, a device might define that an update modifies the value of a specific output port while it is in state on. To add timing behaviour to the language, an update function also has access to \(\delta t \in \mathbb {R}_{\ge 0}\), the amount of time that has passed since it was last executed. This means that in theory, updates are executed in infinitesimal intervals (\(\delta t = \varepsilon \)) to produce continuous behaviour. Practically though, CREST ’s implementation is responsible to execute updates as often as needed and often very coarse time steps can be achieved.

CREST further offers influences ( ) to statically link two ports. Each influence relates two ports and a function in a way, such that the function is executed with the source port’s value as parameter and the result is written to the target port. Actions ( ) are similar to updates, except that they are executed at the exact point when a transition is triggered. This also means that they do not have access to a \(\delta t\) value. Note that influences and actions are purely syntactic extensions of CREST to increase the DSL’s usability. When required (e.g. for static analysis purposes) influences can be replaced by sets of updates, actions by introducing additional automaton states and transitions.⁵

Note, that neither the CREST formalism (i.e. the abstract syntax), nor CREST diagrams prescribe a specific definition language for update and influence functions. This makes the language flexible and adjustable to the knowledge of its users. For instance, in the example in Fig. 4 we use a mathematical notation for updates that uses \(\delta t\) to explicitly highlight timing behaviour in updates and use \(\textit{value} - 5 * \delta t\). However, due to CREST ’s flexibility it would be possible to adopt an ordinary differential equation notation by e.g. writing \(\textit{value}' = -5\) instead. One problem of such genericity is that in principle any kind of functions and notations can be used and defined, causing potential risks to the calculability of CREST systems. To restrict the situation, CREST ’s formalisation defines limitations by specifying the formal update/influence functions’ signatures and the enforced function return value, to assert it matches the target port’s value type. Additionally, there are limitations as to which ports’ values can be used for the return value calculation, so as to not infringe upon CREST ’s locality principle.

Figure 4 depicts the CREST diagram of a simple air conditioning unit with an automatic timer. Its functionality depends largely on the values provided by the two input ports for temperature and switch, which influence the two output ports for cooling power and statuslight. Internally, the local port ontime measures how long the AC has been in the On state. Due to the shown abstraction level, the entire component can be modelled as a single entity, although we could imagine a refined version that uses sub-entities to e.g. model separate heating and cooling elements. Such a refined system would however exceed the purpose of this article.

The working principle of the AC unit is rather straightforward: Provided that the temperature input reads more than 22 degrees and the switch is on, the AC unit will run for 30 time units, or until the temperature or switch conditions are invalid. This is expressed using the condition \((\textit{switch} = \textit{off})\) \(\wedge \) \((\textit{ontime} \ge 30)\) \(\wedge \) \((\textit{temperature} \le 22)\). After a maximum of 30 time units, the device switches back to the Off state and remains there until the timer reaches zero again. The timer functionality is modelled using two updates that modify the ontime port. When in state On, the port’s value is continuously increased according to the time that passes. This means, that the update calculates the result of \(\textit{ontime} + \delta t\) and writes that value to ontime. In state Off, the value is decreased towards zero by five times that rate (i.e. \(\mathrm {max}(0, \text {ontime} - 5* \delta t)\)) until it reaches zero.⁶ Two more updates are used to modify the coolingpower output, depending on the automaton state. When Off, the AC produces 0 Watt, when On, the power increases by 50 Watt for every degree over 22C. Finally, an influence is used to set the statuslight’s colour: green when the switch is on, red otherwise.

The CREST diagram in Fig. 4 uses mathematical notation for updates and transition guards, and pseudo-code for the influence’s functionality specification. As introduced above, the notational form can be easily adapted to the modeller’s knowledge and preferences. For instance, for more practical projects a programming language could be used specify each function’s behaviour. This approach is followed in crestdsl, CREST ’s implementation in the Python GPPL, as introduced in the next section.

Note, that the ports of Fig. 4 display the initial values of the system (including its initial inputs). Though these values are theoretically part of the model’s environmental embedding, we allow their definition. This (rather operational) view, is founded in the fact that similarly sensors often output a default value (e.g. 24C) or special value (e.g. None, undefined) before the first, actual reading.

In many cases, system developers prefer the use of textual over graphical languages. Even though graphical representations can be more easily understandable when used correctly [67], in recent years numerous tools were developed that allow textual modeling, followed by a conversion to a graphical representation.⁷ Inspired by these tools, we aimed to create a textual DSL that is both simple to learn and write for programmers, but also offers a native conversion to CREST diagrams for system developers who prefer graphical models.

crestdsl uses Python as host language for several reasons. First, it is easy to learn and use, and experiences growing popularity. This fact is also manifested in a large number of third-party libraries, numerous tutorials and a helpful online community. From a DSL development view, Python offers many attractive features such as a flexible meta-class system that allows customisation of object creation, function and class annotations (so-called decorators), and the availability of a powerful reflection API. Furthermore, many external tools such as SMT solvers, theorem provers and formal verification engines offer Python bindings and thus a native integration. The latter is a vital advantage for implementing the DSL and its execution engine.

During the development of crestdsl we paid attention to make its use as simple as possible, while at the same time support common Python development best practices. The software is available through the Python package index⁸ and can be installed through Python’s pip program. Thereafter, crestdsl can be used by importing, just as any other Python library.

crestdsl entities are modelled as instances of the class. Features that belong to that entity (e.g. its ports, states, transitions, updates) are modelled as entity attributes. To simplify the creation of several similar entities, crestdsl provides entity types. These types are classes that inherit from the class. The type’s structure is then defined using class attributes and methods. Listing 1 shows an entity type that models the architectural parts of our air conditioning unit. It features two inputs, two outputs and two states. Note that just as CREST diagrams, crestdsl also requires every port to have a resource and current value specified. Similarly, every entity has to have one state designated as state.

Upon instantiation, the class’s constructor and metaclass work to provide a correctly instantiated object. crestdsl supports class inheritance to create specialised or extended versions of an entity type. This feature is not a general CREST concept, but significantly increases crestdsl ’s usability. Listing 2 for instance, shows the extension of by adding transitions, updates and an influence to the class. Note, that the listing shows two ways to specify transitions and updates. The first one is similar to the definition of ports and states: A object is created and assigned as class attribute. The required transition guard is specified either as a lambda-expression or using a function. Alternatively, it is possible to define the transition guard as a class method. By using the decorator, it is then possible to convert the method into a transition. The listing also shows the specification of updates via object and decorator, and the creation of an influence using .

Class inheritance is a powerful concept, as it can also be used to adjust entity behaviour. Python’s multiple inheritance functionality allows class fragments (a.k.a. mixins) to be added to the language. This enables modular development and the separation of specific concerns (e.g. reusable component fragments for adding value inspection or signal probing) into individual classes, that can then be reused where required. If used correctly, this feature permits advanced users to create reusable component fragments and thereby even add aspect-oriented system design to the DSL. The inheritance design principle invites code reuse and the creation of object libraries. For this purpose, crestdsl also provides parametrisable entity types using class constructors.

Without the provision of a separate example, we want to highlight that system composition follows the same DSL design, where subentities are defined by assigning entity objects as class attributes.

To test whether the system model was correctly assembled, a class can be used. This static system analysis performs a number of sanity checks such as testing the entity hierarchy and asserting that each entity defines a current state. Its purpose is to help crestdsl users debug their model quickly and find potential causes for misbehaviour. If necessary, users can also extend the class and implement their own static analysis routines that assert certain system setups (e.g. testing for specific architecture setups, port type conformance, etc.).

To support the combination of aspects from several formalisms (FSM, architecture descriptions, hybrid systems), it is necessary to pay careful attention to the precise meaning of each element. For this reason, CREST ’s semantics have been formally defined to assert consistency with the key principles that we obtained in the requirements evaluation. Thus, it is paramount, that the operational semantics uphold the reactivity, synchronism, parallelism, locality, continuity and non-determinism that are essential for the expression of our systems. In this section, we outline CREST ’s semantics and highlight the relation to other languages and formalisms, such as data-flow languages and hybrid automata. Note, that this section focuses on providing a high-level description of the semantics and its effects in the simulation of CREST. The actual formalisation, including its structured operational semantics (SOS) rules, is provided in Appendix 1. A more elaborate description, that exceeds the scope of this publication can be found in [50].

CREST foresees two ways of model interaction. First, the change of the root entity’s input port values, and second, the advance of time. After each of these, the model has to be stabilised until a “fixpoint” is reached. Fixpoints are system states where the model is stable and will not change without another interaction.

Input value change The external modification of input port values represents changes in the system’s environment to which it should react. Thus, such a modification can only occur at the hierarchical top level. This is due to CREST ’s locality principle, which requires every entity—hence also the root—to be treated as coherent black box that only exposes its communication interface (input and output ports). Once a port value change is observed, the semantics require the stabilisation to be triggered, which then propagates the updated information throughout the system. The process starts by performing the stabilisation first on the system’s root-entity, which then recursively calls stabilisation on its subentities. Evidently, modifiers (i.e. influences, updates and subentities) within an entity can depend on each other. For instance, Fig. 5 shows an excerpt of such a CREST system. It is clear, that sub2 depends on the output value of sub1. Thus, to assert a correct system state, it is necessary to first make sure that sub1 has been stabilised and reached a fixpoint, before executing influence\(_1\) to propagate the value of sub1-output to sub2-input\(_1\).

This brief example illustrates the need to establish a modifier execution order. The creation of this execution order is closely related to the use of Kahn process networks [49] and commonly used for the execution of data-flow languages such as e.g. Lustre [42]. The ordered modifiers are then executed one by one. This means that in this order, each update function is evaluated and the result written to its target port, and subentities are recursively stabilised (see Fig. 6).

Only after all modifiers have been executed, the transitions from the current state are tested whether they are enabled. If no transition can be triggered, the process ends and the entity is stabilised. Otherwise, one transition is chosen and executed. CREST does not prescribe a resolution strategy in case multiple transitions are enabled at the same time. This means, that any enabled transition can be triggered, which is CREST ’s way of introducing non-deterministic behaviour—a vital concept and one of CREST ’s key aspects. After a transition is executed, the stabilisation process has to recursively call itself again, to assert that updates that are related to the new automaton state—and are thus newly active—are executed.

Note, that the semantics in Fig. 6 do not mention influences and actions, as these are syntactic sugar and can be expressed through updates and states alone, as described in Sect. 3. This trait both simplifies the formal semantics and CREST ’s system analysis.

It is also of interest to mention that generally, the reaching of a fixpoint cannot be guaranteed. Especially in the presence of Zeno behaviour (i.e. an infinite number of transitions in finite time [82]) or cycles of continuously enabled transitions it can happen that infinitely many actions are executed without ever reaching a stable state. Even though CREST ’s implementation provides a few configurable heuristics to detect these kinds of situations, it is up to the system designer to avoid the modeling of such problematic behaviour.

For instance, when looking at the time-based behaviour of the air condition, we observe that—provided the input values do not change—the model will alternate between on and off states, so that it is 30 time units in state on, followed by 6 time units in state off, before switching to on again. Figure 7 shows a trace of this behaviour. Evidently, when simulating continuous time systems, it is important to choose the right step-size for the current system behaviour. Advancing in too small time intervals might cause a high calculation overhead and perhaps even render the simulator unusable. Too coarse step sizes can lead to “missing” an important point in time, which either requires the simulator to step back and retry with a smaller step size, or, if undiscovered, might even lead to wrong simulation results. CREST ’s semantics assume the existence of a next transition time function, that calculates the precise amount of time until a behaviour change (i.e. a state transition) occurs. This means, that calling the function when the air condition system is in state on and ontime has a value of 18.7, should return the exact value of 11.3 time units, since at this time the port’s value reaches 30 and thus a transition should be triggered (see Fig. 8).

crestdsl implements next transition time using an SMT approach. Whenever it is necessary to calculate the time until a transition event, the simulation engine translates the update functions and influences that potentially affect the value of a transition guard into a set of SMT constraints (see details in the next section). This constraint set is then handed to Microsoft’s Z3 Theorem Prover [22], which either calculates a value for \(\delta t\) that solves these constraints and hence enables the transition, or alternatively signals that the constraint set cannot be solved and therefore the transition cannot be enabled by the advance of time alone.

Once the simulator obtains the knowledge at what point in time the next transition becomes enabled, advancing time is merely a matter of iteratively stepping forward to the next transition point and triggering the stabilisation process after every step. Note, that in this case the stabilisation process has to trigger updates with the correct \(\delta t\)-value, to consider the timing behaviour when calculating the updates’ target port values.

CREST ’s formal semantics (see Appendix 1) do not specify how the next transition time should be calculated. Thus, CREST can be used for any type of system. The implementation’s SMT approach however relies on the use of Z3, which is not capable of solving nonlinear optimisation problems. This means, that even though crestdsl produces a nonlinear constraint set, it cannot be solved and the simulation is likely to run into issues in the presence of nonlinear dynamics. At the moment, we are aiming to extend crestdsl to add support for nonlinear systems by using theorem provers with nonlinear optimisation capabilities such as dReal [37].

Using CREST ’s formal semantics and crestdsl it is possible to create a simulation engine that helps answering “What happens if...?” questions. Users can try out system interactions and observe possible usage scenarios. Listing 4 shows the example code of a simulation scenario. The listing uses the standard that follows CREST ’s semantics and implements non-determinism. However, crestdsl provides two other simulation engines that allow slightly altered usage. The first one, , prompts the user to choose an enabled transition anytime a non-deterministic situation is encountered. This allows users to explore specific scenarios despite non-deterministic models. Finally, can be used to define strategies on how to deal with non-determinism. This scenario can be used to model controllers that, given a range of similar transition choices, will choose one according to a pre-defined policy. The can also be used to follow a specific execution trace that is e.g. discovered by state space exploration or similar verification techniques, as described further below.

CREST ’s semantics allow the construction of state spaces and the use of formal verification techniques, such as model checking, thereon. Based on existing approaches, logic formulas can be defined and their truth-value examined on a model’s state space. Since CREST is a hybrid formalism, it is however necessary to extend the classical temporal logics (e.g. LTL, CTL) to incorporate timing aspects in their language. Given CREST ’s non-determinism, and thus its branching behaviour, we use the timed computation tree logic (TCTL) [45], a timed extension of CTL, and its operators and formulas for the specification of system behaviour. We will not elaborate on the foundations of classic and temporal model checking, but instead refer the interested reader to seminal works such as [3] and [14]. In general, TCTL formulas are composed of a set of operators, which are inductively defined:where \(p \in AP\) is an atomic proposition, and I is an interval in CREST ’s time base that defines the timing aspect of the \(EU_I\) and \(AU_I\) operators. Based on these operators, further abbreviation operators can be defined, such as \(EF_{I}\,\phi \,=\,\texttt {True}\,EU_{I}\,\phi \) and \(AG_{I}\,\phi \,=\,\lnot \,EF_{I}\,\lnot \,\phi \). Note, that in comparison to classical CTL, there is no X (“next”) operator, since in continuous formalisms there is no “next point in time”.

Subsequently, we can test these formulas on timed Kripke structures [57]. Timed Kripke structures are graph-based encodings of a system’s state space, whose nodes represent discrete system states and edges are timed transitions between them. Each node is annotated with a set of APs that represent certain behaviour (e.g. “the AC is on” or “the coolingpower output is above 100 Watt”). CREST ’s continuous semantics demand that the transitions be annotated with the amount of time it takes to pass from one state to another. Figure 9 shows an example of a timed Kripke structure.

Following some minor adaptation of the timed Kripke structure, the TCTL formulas can then be evaluated using graph search algorithms that are inspired by classical CTL model checking approaches. Details on these algorithms are provided in [57] and an elaborated description of the creation and adaptation of timed Kripke structures for CREST models is described in [50].

crestdsl implements a Python-native subpackage that provides APIs for the specification of system configurations, the creation of a model’s state space and the search of that behaviour within that state space. System states are specified as checks, which can be used to either define that an entity is in a given automaton state (e.g. ), or to compare a port against a constant or another port value (e.g. ). crestdsl also allows to create composed checks as conjunctions, disjunctions and negations of other checks.

Checks can then either be evaluated directly on a system state using by calling its method. Alternatively, they can be used for the formal verification of a crestdsl model’s state space. To do so, crestdsl provides two APIs. The first is crestdsl ’s convenience verification API. It provides interfaces for users that are unfamiliar with model checking and formal verification. Modellers are provided with a set of functions that can be executed for common verification tasks. For instance, the function, verifies that a given condition can never be invalid. Similarly, asserts that it is possible to reach a given state and asserts that a given system configuration can never be reached. Table 2 shows some convenience API functions and their TCTL equivalent formulas, Listing 5 shows their programmatic usage.

crestdsl also implements an expert API, that allows to manually create complex TCTL formulas and obtain direct control over the model checking process. By directly creating and using the object, it is possible to gradually explore a state space. This allows crestdsl ’s routines to be used in some infinite state spaces. The API groups implementations of all TCTL operators, so that experienced modellers can create complex formulas to be evaluated. Listing 6 provides an example of the expert verification API.