FORMAL VERIFICATION OF REAL TIME DISTRIBUTED SYSTEMS USING B METHOD

Throughout the previous years, the complexity and size of digital systems has increased dramatically, as a result design flow phases changed a lot. Simulation used to be the most common procedure to assure the correctness of a system under design, but it cannot exhaustively examine all the execution scenarios of the system. A different approach to validate a system by formally reasoning the system behavior is Formal verification, where the system implementation is checked against the requirements or the properties to be satisfied. The most common paradigms are based on theorem proving, model checking and language containment. This paper presents an application of the B method to the formalization and verification 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.