Implementation of formally verified real time distributed systems: Simplified flight control system

The most common procedure to ensure the reliability of a design is simulation. Unfortunately simulation cannot fully inspect all the execution states of the system. The significant increase in the complexity and size of digital systems together with the nature of real time systems boosted up the need for a different approach for the validation of the behavior of a system in the early design stages. Formal verification is an approach to validate a system by formally reasoning the system behavior. In formal verification the system implementation is checked against the requirements or the properties to be satisfied. B method is one of the common paradigms used in formal verification. But in some cases some deviations from the verified model appears in the final implementation phase, so some of the verified properties are lost. This work aims to reach for a complete design flow for verification and implementation of a simplified flight control system, as an example of a system consisting of a number of distributed computing devices that are interconnected together through digital communication channels. The B method was used to formalize and verify, then the verified B model was transformed into VHDL implementation concerning exact mapping to maintain the properties of the verified model. The main objective is to avoid any discrepancies between the verified model and its implementation.