1 Rigorous System Design

Modern software systems are inherently concurrent. They consist of components running simultaneously and sharing access to resources provided by the execution platform. For instance, embedded control software in various domains, ranging from household robotics through operation of smart power-grids to on-board satellite software, commonly comprises, in addition to components responsible for taking the control decisions, a set of components driving the operation of sensing and actuation devices. These components interact through buses, shared memories and message buffers, leading to resource contention and potential deadlocks compromising mission- and safety-critical operations. Similar problems are observed in various kinds of software, including system, work-flow management, integration software, web services, etc.   Essentially, any software entity that goes beyond simply computing a certain function necessarily has to interact and share resources with other such entities.

Fig. 1
figure 1

A simplified example of the RSD flow instantiation (the blue items are the result of the previous stage; the black ones are provided as new input at the current stage)

Full size image

The intrinsic concurrent nature of such interactions is the root cause of the sheer complexity of the resulting software. Indeed, in order to analyse the behaviour of such a software system, one has to consider all possible interleavings of the operations executed by its components. Thus, the complexity of software systems is exponential in the number of their components, making a posteriori verification of their correctness practically infeasible. An alternative approach consists of ensuring correctness by construction, through the application of well-defined design principles [4, 20], imposing behavioural contracts on individual components [7] or by applying automatic transformations to obtain executable code from formally defined high-level models [33].

The Rigorous System Design (RSD) [33] approach enforces multiple levels of separation of concerns. It relies on a sequence of semantics-preserving transformations to obtain an implementation of the system from a high-level model while preserving all the properties established along the way.

Figure 1 illustrates a simplified instantiation of the RSD flow. One starts by designing the application model. The application model is verified to prove the elementary properties that are not assured by construction, such as absence of local deadlock, and satisfaction of basic requirements. These elementary properties, serve as a basis for the proof of global properties, obtained by construction.

The application model is then extended with additional components modelling the target platform to obtain the system model, which is used to perform platform specific analyses and the optimisation of performance through the exploration of the design space (memories, buses, mapping of software components to hardware elements, etc.).

Finally, the model is enriched with platform specific information (e.g.communication primitives) and, after removing components modelling hardware elements, executable code is automatically generated.

Proving that the assumptions made at the modelling level to justify the separation of concerns hold, indeed, at the platform level, guarantees that all the properties established throughout the design process also hold for the generated code.

Thus, the RSD approach applies—on the higher abstraction level of the system design process—the same principles as those provided by standard compilers for the generation of machine-executable code from programs written in languages such as Java or C++. It consists in decomposing the argument justifying the correctness of the entire process into several independent arguments justifying the correctness of individual transformations. Furthermore, it provides flexibility w.r.t.the target platforms by postponing design choices as far as possible and allowing for different transformations of the same model to be applied at every design stage. However, in drawing this parallel, it is appropriate to differentiate between commonly used compilers such as gcc, where the public trust originates mainly from the extensive usage experience, and verified compilers such as CompCert [29], where preservation of semantics at the various stages is formally verified. Although the second scenario is currently preferable for RSD tool sets due to lack of usage history comparable to that of compilers such as gcc, both can be relevant in practice.

Applications. Although the RSD approach as formulated by Sifakis [33] originates from the development of the BIP framework for the Embedded Software design (see, for example, [5, 6]), it is applicable in a much broader variety of domains, whereof we will mention below just a few.

Key issues of applying the RSD approach to the Cyber-Physical Systems (CPSs), which comprise components with both discrete and continuous underlying dynamics, are discussed in [11]. The authors argue that the objective of cyber-physical system modelling is twofold: providing the means for (1) the validation of the system design through simulation of such models and (2) the generation of executable code for the discrete control sub-system. The key point here is that the two design artefacts, i.e.the simulator and the code of the control sub-system are obtained through two branches of the design flow sharing a substantial prefix. Thus, the generated control sub-system is equivalent to—i.e.satisfies the same properties as—the corresponding components of the simulator by construction.

Expanding on the above idea, it is clear that the RSD approach can be of great benefit for system design and operation involving the so-called Digital Twins where simulation becomes “a core functionality of systems by means of seamless assistance along the entire life cycle” [32].

Autonomous and (self-)adaptive systems constitute another significant domain for the application of the RSD approach. These include, for example, autonomous vehicles, Cloud and IoT applications. Indeed, such systems must react to changing environmental constraints and user requirements. Therefore, they are characterised by high dynamicity both of their behaviour and their structure. In particular, this implies that many of the underlying verification problems are undecidable [12, 19] emphasising the need for by-construction correctness provided by the RSD approach.

Key elements. The RSD approach relies on several fundamental elements, among which we highlight two. Firstly, methods and tools for the design of correct-by-construction high-level models are necessary to initiate the process. Although it is difficult to imagine a unique approach that would fit all the various application domains, it seems reasonable to expect that these approaches will share a common core, comprising, at the very least, some form of

  1. (1)

    Requirement elicitation and formalisation and

  2. (2)

    (semi-)automatic synthesis of parts of the models in order to discharge these requirements [34].

Secondly, defining and proving the validity of suitable domain-specific abstractions, such as architectures, protocols or design patterns (e.g.[1, 30, 31]), is key for implementing an RSD flow. Such abstractions are used to facilitate the design of correct-by-construction high-level models. The transformations along the RSD flow can then rely on platform-specific implementations of these abstractions to automatically generate refined models or executable code. Although these platform-specific implementations would have to be proven correct, such proofs need only be carried out once, reducing the overall complexity of the process and ensuring the trustworthiness of the resulting artefacts.

2 This issue

This special issue contains the extended versions of selected papers presented at the \(1\mathrm {st}\) and the \(2\mathrm {nd}\) International Workshops on Methods and Tools for Rigorous System Design (MeTRiD 2018–2019) held as satellite events of the corresponding European Joint Conferences on Theory and Practice of Software (ETAPS 2018–2019).

The goal of the MeTRiD workshop is to promote cross-fertilisation between research in academia and practical applications in the industry. On the one hand, we hope that, through the publication of research and tool papers, the workshop will contribute to raising awareness of the methods and tools available among the industrial players. On the other hand, presentation and exchange of realistic case studies should allow academic researchers to better fit their tools to industrial needs, thereby improving the dissemination of results.

The first, 2018 edition was a traditional workshop with peer-reviewed proceedings published as volume 272 of the Electronic Proceedings in Theoretical Computer Science (EPTCS) [10]. MeTRiD 2018 accepted three categories of papers: regular, tool and case-study papers. MeTRiD 2019 was by invitation with presentations of, both, already published results and ongoing work, and no proceedings.

This issue comprises 7 papers addressing the key elements outlined above. Papers [3, 18] contribute to the design of correct-by construction high-level models by defining a high-level modelling formalism [18] and by providing an approach for debugging CPS models [3]. Papers [9, 14, 22, 24, 28] contribute to the design and proof of domain-specific abstractions. They provide techniques for ensuring the correctness of randomised consensus protocols [9], program block parallelisation [14], usage control policies [22], and for ensuring optimality of partition schedules [24] and energy consumption [28].

Each of these papers was reviewed by at least three reviewers and extends one of the papers presented at MeTRiD 2018 or 2019.

  • The paper “Specifying and verifying usage control models and policies in TLA\({}^+\)” by Grompanopoulos, Gouglidis, and Mavridou [22] is an extension of the MeTRiD 2018 paper by the same authors [21]. It presents a case study on specification and model checking of usage control models and policies. The focus of the paper is on demonstrating how to express control policies in TLA\({}^+\). By doing so the authors also introduce their own policy model called UseCON.

  • The paper “Programming dynamic reconfigurable systems” by El Ballouli, Bensalem, Bozga, and Sifakis [18] is an extension of the ISoLA 2018 and FACS 2018 papers [16, 17] by the same authors. The paper focuses on programming dynamic reconfigurable systems. It presents an extension of Behaviour-Interaction-Priority (BIP) framework called Dynamic-Reconfigurable BIP (DB-RIP), which allows dealing with reconfigurable systems including different types of dynamism. The technical contribution of the paper consists of the formal definition of DR-BIP, i.e. its syntax and semantics. In addition, the paper describes a prototype implementation of the language in Java and illustrates the application of the approach to model 3 different examples from different domains.

  • The paper “Model-based optimization of ARINC-653 partition scheduling” by Han, Zhai, Nielsen, and Nyman [24] is an extension of the MeTRiD 2018 paper [23], by the same authors. This work introduces a framework for generating optimal ARINC-653 partitioned schedules, i.e.system partitions scheduled in mutual exclusion in order ensure temporal isolation of applications in safety-critical systems. The main challenge in synthesising optimal period and budget parameters for the partitions is the scalability problem, since the parameter space for larger systems rapidly grows in size and cannot be exhaustively explored. The proposed framework excludes, as early as possible, non-schedulable combinations of parameters by applying (in order of sequence) global schedulability tests, statistical model-checking and model-checking in Uppaal. Finally, an evolutionary algorithm for parameter exploration is applied that generalises the yes/no verdict of the schedulability question into a numeric fitness evaluation.

  • The paper “Correct Program Parallelisations” by Blom, Darabi, Huisman, and Safari [14] is an extension of the FASE 2015 and NFM 2017 [13, 15] papers by the first three authors. This paper presents a verification technique to reason about the correctness of compiler directives indicating which program blocks may potentially be executed in parallel without changing the behaviour of the program. To this end, the authors introduce an intermediate language for representing such programs, its formal semantics and a soundness proof for deductive proof rules that build on that semantics. The paper also discusses how OpenMP programs can be translated into the intermediate language and how the verification methodology can be implemented on top of the VerCors/Viper verification tool infrastructure.

  • The paper “Energy characterization of IoT systems through design aspect monitoring” by Lekidis, and Katsaros [28] is an extension of the MeTRiD 2018 paper [27] and a related presentation in MeTRiD 2019, by the same authors. This work proposes a model-driven approach for the energy cost estimation of Internet of Things design aspects (availability, reliability, dynamicity and security), by monitoring them. This paves the way to identify feasible architecture solutions that satisfy energy footprint requirements.

  • The paper “CPSDebug: Automatic failure explanation in CPS models” by Bartocci, Manjunath, Mariani, Mateis and Ni\(\check{c}\)kovi\(\acute{c}\) [3] is an extension of the SEFM 2019 paper [2] by the same authors. In particular, the authors introduce an approach for the detection of faults and their localisation in Stateflow/Simulink models of cyber-physical systems. This is challenging, when there are mixed discrete and continuous signals, while the faults may not physically manifest immediately. The method rests on simulation traces that satisfy or violate desired properties expressed in Signal Temporal Logic. Those traces that satisfy the properties are then used to mine additional specifications, and the method produces explanations from the analysis of failed traces with respect to the properties mined.

  • The paper “Verification of Randomized Consensus Algorithms under Round-Rigid Adversaries” by Bertrand, Konnov, Lazi\(\acute{c}\), and Widder [9] is an extension of paper [8] by the same authors. This work is focused on obtaining a fully automated proof of correctness—encompassing validity, agreement and almost-sure termination—of randomised consensus algorithms involving arbitrarily many (faulty) processes and rounds under round-rigid adversaries, i.e.adversaries that are weakly fair and that select actions in a “round-based” manner. The approach is based on the threshold automata formalism introduced in [25, 26].

We would like to thank all the authors of these papers for their contributions and the reviewers that we have solicited for their thorough evaluations. Furthermore, we would like to acknowledge the help of the OCS team and, particularly, Markus Frohme, whose help and reactivity throughout the preparation of the issue were crucial to its successful realisation.