Co-design and refinement for safety critical systems

In this paper we focus on design entry of complex systems, that is, the highest abstract tier of the global system without implementation choices to such and such technologies. At this very first level, the use of a formal specification language is more and more considered as the foundation of a real validation process. What we would like to emphasize is that from a formal design entry, project management can be formally controlled by formal refinement. We propose an architecture that is based upon stepwise refinement of a formal model to achieve controllable implementations. This leads to implementations that are highly effective, but remain formally related to the first formal specification. Partitioning, fault tolerance, and system management are seen as particular cases of refinement in order to conceptualize systems correct by proven construction. In this paper, we present the basic principles of system methodologies and describe the methodology based on the refinement paradigm. In order to prove this approach, we have developed the B-HDL Tool based on VHDL (digital circuits) and B method (formal language based on set theory and logic). The benefits of such tools would be an amazing productivity gain, a better reuse of automation and a formal redundancy management.