This project will address two fundamental challenges for the implementation of the Rigorous System Design approach to general-purpose software: 1) obtaining behavioural models of the coordinated software entities and 2) detecting the deviations between these models and the corresponding executable code in the face of software evolution.
Larisa Safina is working on this project
This project, supported by the I-SITE ULNE “Support for young researchers 2020” programme starting on the 1st of January 2021, focuses on the building blocks used for the rigorous design of concurrent software. The Rigorous System Design (RSD) approach has been initially proposed in the context of embedded systems. It strives for the by-construction correctness of software systems through enforcing multiple levels of separation of concerns. This is achieved by applying 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.
The RSD approach relies on the existence of a unifying component framework with unambiguous formal semantics. This is crucial to demonstrating the preservation of properties across the stages of the RSD flow. For this purpose, the project builds on my previous work on the BIP framework for the coordination of concurrent components. A BIP model consists of a set of components and connectors that define all possible synchronisations among the components. Overall behaviour of the application is defined by the fully formalised operational semantics of BIP. It is enforced at run-time by the BIP engine.
JavaBIP—a Java implementation of the BIP coordination mechanisms—does not implement the RSD approach due to the difficulty of combining automatic code generation (as in BIP) with continuous software evolution. Instead, it realises the coordination of existing concurrent software components in an exogenous manner, relying on component specifications that provide an abstract view of the software under development.
This raises two fundamental challenges that the project will address: 1) obtaining behavioural models of the coordinated software entities and 2) detecting the deviations between these models and the corresponding executable code in the face of software evolution.
