Rigorous Systems Engineering

Background

Many software intensive systems of today, such as aircrafts and heavy trucks, are incredibly complex. They are a result of thousands of man-years of engineering, and contain thousands of components. Many of these systems are also safety critical. A recent example is autonomous cars. Furthermore, the engineering companies strive to make development more efficient by adopting agile methods, continuous integration, and product line thinking. The latter means that not only one product is developed but rather a family of products from which the customer can select a single configuration. This results in, not only added product complexity, but also in that the engineering of these systems becomes extremely complex.

To cope with the above challenges, the engineering methodology needs to go beyond traditional ”systems engineering”. Therefore, in our research, we aim for a systems engineering approach that is ”rigorous”. By this we mean that the whole methodology is founded in a theoretical formal framework. However, we acknowledge that many activities of engineering are informal in its nature, and rely on skilled humans. Therefore, our framework must support and be able to include artefacts resulting from such informal engineering.

We focus on the following areas:

- A framework for systems engineering of heterogeneous systems founded in a formal language. A particular focus is on contract-based specification and compositional verification.

- Automatic generation of assurance cases, with formal arguments for dependability attributes such as safety (then called safety case).

- Analysis, by formal reasoning and inference, of product properties and dependability attributes.

- A general support for product lines. This includes specification of artefacts, generation of assurance cases, and analysis of product properties.

- Formal verification of C-code, Simulink models, and requirements decompositions.

- How to formally capture uncertainties resulting from informal engineering using probabilities.

SMP-tool

Within the scope of Rigorous Systems Engineering, a Matlab app for dependability analyses of safety-critical systems has been released. The app is known as "SMP-tool" and is a freeware.

APProVe toolchain

The APProVe toolchain automates the process of deductive verification, through automatic inference of annotations needed in tools such as Frama-C.

APProVe toolchain