The lack of explicit and precise specifications of software interfaces between components often leads to integration issues during development and maintenance. To address this, we have developed a framework named ComMA (Component Modeling and Analysis) that supports model-based engineering of high-tech systems by precisely defining components and their interfaces. The framework is a family of Domain Specific Languages (DSLs) for modeling component interfaces, protocol state machines, time and data constraints, and constraints on relations between events of multiple interfaces. From these models a number of artifacts can be generated automatically to support analysis and various engineering tasks. ComMA has been developed in close collaboration with the Philips IGT business unit that develops minimally-invasive X-ray systems. This paper presents the experience we gained in creating the ComMA framework and its application in industrial practice. We describe and reflect on the technical, organizational and process-related aspects of deploying a non-trivial MDE solution in an industrial setting.

We present our vision for creating an industrial legacy software rejuvenation toolchain. The goal is to semi automatically remove code smells from stateful software used in Cyber Physical Systems (CPS). Compared to existing tools that remove code smells, our toolchain can remove more than one type of code smell. Additionally, our approach supports multiple programming languages because we use abstract models obtained by means of model learning. Supporting more than one programming language is often lacking in state of art refactoring tools.

At Philips IGT, we develop and produce interventional X-ray systems. For a controller in these systems, we have an approximately five years old domain specific language. Like general programming languages, domains specific languages also evolve. These languages co-evolve together with their domain. The language used at IGT was initially created for one system instance. Because of our positive experiences with the language, we want to evolve the language to support a family of systems. In this paper, we report on our experiences with the modifications we made to the original language. We made these changes preserving the behavior of the existing system instance. To prevent confidentiality issues, we use a Lego robot in our examples.

The construction of a co-simulation for large cyber-physical systems can be very time consuming. We have defined a domain specific language called CoHLA that facilitates this construction based on the standards FMI and HLA. Scalability of this approach is investigated by the application to Internet of Things (IoT) systems. Because of the repetitive nature of these systems, we developed a separate domain specific language that allows the user to describe the system and easily generate a co-simulation definition for CoHLA. Additionally, we extended CoHLA to speed up the co-simulation execution by distributing the simulation across multiple nodes. This method also allows the co-simulation to be executed in the cloud easily.

Cyber-physical systems consist of many hardware and software components.Over the life-cycle of these systems, components are replaced or updated.To avoid integration problems, good interface descriptions are crucial for component-based development of these systems.For new components, a Domain Specific Language (DSL) called Component Modeling & Analysis (ComMA) can be used to formally define the interface of such a component in terms of its signature, state and timing behavior.Having interfaces described in a model-based approach enables the generation of artifacts, for instance, to generate a monitor that can check interface conformance of components based on a trace of observed interface interactions during execution.The benefit of having formal interface descriptions also holds for legacy system components.Interfaces of legacy components can be reverse engineered manually.In order to reduce the manual effort, we present an automated learner.The learner can reverse engineer state and timing behavior of a legacy interface by examining event traces of the component in operation.The learner will then generate a ComMA model.

Gaining insight in the properties of an Internet of Things (IoT) system during the design phase is difficult. The cosimulation of such a system would be very useful, but creating it is usually time consuming. By means of domain specific languages (DSLs) we support the fast construction of large co-simulations of IoT systems. This approach includes the use of CoHLA, a DSL that generates co-simulation code based on the HLA and FMI standards. Due to the large number of connected sensors and actuators in an IoT system, the time needed for simulation can be a blocking factor. Hence we facilitate distributed co-simulation in the cloud. To do that efficiently, we have conducted a set of experiments to analyse scalability and the performance impact of distribution methods. From these experiments, lessons were learned on how to distribute the co-simulation of IoT systems.

Contains fulltext : 191723.pdf (Publisher’s version ) (Open Access)

The development of cyber-physical systems (CPSs) is a multi-disciplinary process. A model-based approach during the design of a system is important for making design decisions during the exploration of alternatives. However, all disciplines use different modelling tools and techniques, which makes the integration of these models difficult and time-consuming. The use of the High Level Architecture (HLA) simplifies this problem, but still requires quite an effort to implement. Our work focuses on minimising the effort required to construct co-simulations. We have created a Domain Specific Language (DSL) to define a system design consisting of different types of models. We demonstrate how this DSL can be used to experiment with alternative designs of the system quickly. The DSL allows us to build virtual prototypes of CPSs without the large overhead of constructing the co-simulation.

Contains fulltext : 173201.pdf (Publisher’s version ) (Open Access)

The high-tech industry produces complex devices in which software plays an important role. Since these devices have been developed for many decades, an increasing part of the software can be classified as legacy which is difficult to maintain and to extend. To improve the maintainability of legacy components, domain specific languages (DSLs) provide promising perspectives. We present a DSL for creating configuration files that describe the topology of a fieldbus. This DSL improves the maintainability and extensibility of a legacy component. Compared to the current way-of-working, the configuration files generated by the DSL are of higher quality due to the concise representation of DSL instances and additional validation checks. To raise the level of abstraction even more, we have created a second DSL which allows a concise description of system configurations and the generation of topologies.

We evaluate the effect of applying the commercial formal technique Analytical Software Design (ASD) to an industrial project. In ASD, interfaces and software designs are modelled using a formal tabular notation. The ASD tool set supports formal checks of these models, such as deadlock freedom and interface compliance. In addition, full code can be generated from design models. ASD has been applied at Philips Healthcare to develop parts of the software of interventional X-ray systems. We report about the experiences with the embedding of ASD into the development processes. The quality of the resulting code and the productivity has been analysed and compared to code developed with other techniques. We observe that the use of ASD leads to a strong reduction of the number of defects and an increase in productivity. The results are also compared to the literature about standards and related projects at other companies.

To improve the design of a power control unit at Philips, two Domain Specific Languages (DSLs) have been used.The first DSL provides a concise and readable notation for the essential state transitions.It is used to generate both configuration files and analysis models.In addition, we also generate instances of a second DSL which represents test traces.This second DSL is used to generate test cases for the power control unit.The use of DSLs not only improved productivity, but also the quality of the configuration files and the test set.• How much time is needed to learn the tools and techniques?• How much effort is needed to migrate the current legacy component to a component which is defined by a highlevel human-usable DSL?• Does the DSL approach support the combination with analysis techniques such as simulation tools and formal

The dependability of high-volume embedded systems, such a consumer electronic devices, is threatened by a combination of quickly increasing complexity, decreasing\ntime-to-market, and strong cost constraints. This poses challenging research questions that are investigated in the Trader project, following the industry-as-lab approach. We\npresent the main vision of this project, which is based on a model-based control paradigm, and the current status of the project results.

We describe an approach to support UML-based development of embedded systems by formal techniques. A subset of UML is extended with timing annotations and given a formal semantics. UML models are translated, via XMI, to the input format of formal tools, to allow timed and non-timed model checking and interactive theorem proving. Moreover, the Play-Engine tool is used to execute and analyze requirements by means of live sequence charts. We apply the approach to a part of an industrial case study, the MARS system, and report about the experiences, results and conclusions.

We present a formal approach to the top-down design of real-time components that communicate using a shared data space. The approach is compositional, that is, only the formal specifications of the components are used to reason about their combined behaviour Formal reasoning is supported by the interactive theorem prover PVS. Our shared data space model is based on the so are architecture SPLICE, that allows loosely-coupled components. Our formalism is illustrated by the top-down design of a smallflight-tracking-and-display system, which contains an event-driven and a time-driven component. Formal correctness is established, given suitable assumptions about the environment of the system and relations between timing parameters.

A formal approach for the development of real-time control systems is described. Our development process consists of two phases: the platform-independent phase, which includes specification programming and verification and the second phase, where execution platform considerations (i.e. resource constraints) are taken into account. This development process supports the use of end-to-end timing constraints through the whole design process without splitting them apart. A real-time application is modeled as a parallel composition of objects communicating by means of asynchronous message passing. This work concentrates on a compositional framework that combines the specification and verification of functional requirements and end-to-end timing constraints into one consistent formal model. In this paper we apply the approach to the mine pump control system. The formal analysis shows that a previously published implementation of the mine pump control system is incorrect.

Concerns the formal specification and mechanical verification of transaction processing systems aimed at distributed databases. In such systems, a standard set of ACID (Atomicity, Consistency, Isolation and Durability) properties must be ensured by a combination of concurrency control and recovery protocols. In the existing literature, these protocols are often studied in isolation, making strong assumptions about each other. The problem of combining them in a formal way has been largely ignored. To study the formal verification of combined protocols, we specify a transaction processing system, integrating strict two-phase locking, undo/redo recovery and two-phase commit. In our method, the locking and undo/redo mechanism at distributed sites is defined by state machines, whereas the interaction between sites according to the two-phase commit protocol is specified by assertions. We have proved, using the interactive proof checker of PVS, that our system satisfies atomicity, durability and serializability properties.

The formal specification and mechanical verification of an atomic commitment protocol (ACP) for distributed real-time and fault-tolerant databases is presented. As an example, the non-blocking ACP of Babaoglu and Toueg (1993) is analyzed. An error in their termination protocol for recovered participants has been detected. We propose a new termination protocol which has been proved correct formally. To stay close to the original formulation of the protocol, timed state machines are used to specify the processes, whereas the communication mechanism between processes is defined using assertions. Formal verification has been performed incrementally: adding recovery from crashes only after having proved the basic protocol. The verification system PVS was used to deal with the complexity of this fault-tolerant protocol.

Abstract To specify and verify real-time systems, we consider a real-time version of temporal logic called Explicit Clock Temporal Logic. Timing properties are specified by extending the classical framework of temporal logic with a special variable which explicitly refers to a global notion of time. Programs are written in an Occam-like real-time language with synchronous message passing. To show that a program satisfies a specification, we formulate a proof system which is proved to be sound and relatively complete. The proof system is compositional, which makes it possible to decompose the design of a large system into the design of subsystems. This is shown by the verification of a small part of an avionics system.

Abstract Classical Hoare triples are modified to specify and design distributed real-time systems. The assertion language is extended with primitives to express the timing of observable actions. Further the interpretation of triples is adapted such that both terminating and nonterminating computations can be specified. To verify that a concurrent program, with message passing along asynchronous channels, satisfies a real-time specification, we formulate a compositional proof system for our extended Hoare logic. The use of compositionality during top-down design is illustrated by a process control example of a chemical batch processing system.

To specify and verify distributed real-time systems, we use a formalism based on Hoare triples. The framework has been adapted to deal with safety as well as liveness properties, and a compositional proof method has been formulated. The formalism is applied to a distributed real-time arbitration protocol in which concurrent modules compete to get control over a common bus.>

A compositional proof system is presented to axiomatize the real-time behavior of asynchronously communicating processes. Programs are written in a real-time version of CSP where processes asynchronously send and receive messages along channels that are capable of buffering an arbitrary number of messages. Timing properties are expressed in explicitly clock temporal logic, which extends linear temporal logic with a special time variable, referring to a global clock.>