The Rigorous System Design (RSD) approach emphasizes multiple levels of separation of concerns. It enforces behavioural properties through semantics-preserving transformations. The RSD flow involves designing an application model, verifying elementary properties, extending the model with platform components, and generating executable code. The approach is applied to various domains, including embedded systems, cyber-physical systems, autonomous systems, and digital twins. The thesis summarises the key contributions of the author. The first part explores the classical semantics of BIP, a robust component framework central to the RSD methodology. It introduces the theory of architectures, a key element enabling the combination of predefined BIP design patterns to enforce desired behavioural properties. The design process, starting from system requirements and leading to the C++ implementation, is illustrated using the CubETH nano-satellite on-board software case study. The second part develops a formal algebraic framework for comparing the expressive power of component-based frameworks. It applies this framework to analyse the expressiveness of the BIP framework. Additionally, an alternative "offer" semantics of BIP is introduced, exploring its relationship with the classical semantics. The third part addresses the adaptation of the RSD approach to general-purpose software development. It introduces JavaBIP, a Java implementation of BIP-inspired coordination mechanisms. JavaBIP utilizes Java annotations and reflection mechanisms to define BIP models associated with Java objects. The chapter details the coordination mechanisms, modular architecture, and the dynamic addition/removal of components in JavaBIP. Two ongoing applications in Cloud Computing and Software Variability, leveraging JavaBIP, are highlighted.
defended on 08/03/2024