Abstract: Modern software systems are inherently concurrent. They consist of components running simultaneously and sharing access to resources provided by the execution platform. The intrinsic concurrent nature of such interactions is the root cause of the sheer complexity of the resulting software, which becomes exponential in the number of software components. This makes wholistic a posteriori correctness verification extremely difficult. An alternative approach consists in ensuring correctness by construction. The Rigorous System Design 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.
In the first part of this talk, I will present the BIP (Behaviour-Interaction-Priority) framework and an approach we have developed for the design of correct-by-construction high-level behavioural models for nanosatellite On-Board Software (OBSW). In the second part of the talk, I will discuss the challenges of adapting this approach to general-purpose software, briefly presenting the JavaBIP variation of the BIP framework, highlighting some key differences between BIP and JavaBIP. One key difference is that, instead of generating source code from the BIP model, we use annotations to associate such a model to existing Java code.
Thursday 4 March 2021 15:45 - 16:30
