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.
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 complete a posteriori verification of their correctness practically infeasible. An alternative approach consists in ensuring correctness by construction.
The term “Rigorous System Design” (RSD) denotes the design approach that is based on a formal, accountable and iterative process for deriving trustworthy and optimised implementations from models of application software, its execution platform and its external environment. A system implementation is derived from a set of appropriate high-level models by applying a sequence of semantics-preserving transformations. An instance of the RSD flow is shown in the figure below.
It involves four essential steps:
- A high-level, functional application model is defined based on the relevant user requirements, specifications of the functional behaviour of system components and coordination constraints imposed on their interaction.
At this stage, behavioural properties, such as deadlock-freedom, can be established by analysing component interactions.
- An abstract system model is obtained by combining the application model defined in the previous step with a model of the execution platform architecture and a mapping between application and platform components.
At this stage, performance can be evaluated by simulation based on the characteristics of the execution platform components.
- A concrete system model is obtained by model transformation from the abstract system model, incorporating platform-specific communication primitives. Typically, at this stage, high-level interaction mechanisms are replaced by appropriate primitives provided by the execution platform, e.g. message passing or shared memory regions.
- Finally, executable code is separately generated for each processing element of the target platform.
The RSD approach has a number of advantages over conventional design processes. In particular:
- All relevant concerns are strongly separated, each being specified using a dedicated model in a suitable formalism.
- Design decisions are only taken when strictly necessary, ensuring that all design space restrictions are justified and traceable to clearly stated requirements, expressed in languages or formalisms with clear semantics.
- Properties established at any step of the design flow are preserved throughout the subsequent steps including the executable implementation. Thus resulting systems are correct by construction.