Formal Methods, Event-B and UPPAAL Timed Automata
Formal methods are techniques to model and reason complex systems as mathematical objects. They are concerned with the application of a reasonably wide variety of theoretical computer science fundamentals. Formal methods are supported by formal languages (e.g., mathematical logic) and allow applying formal system verification which is essentially a compliment to usual system/software testing for making sure the behaviour of the system conforms to its requirements. While systems grow more complex and safety becomes a more serious issue, the formal approach to system design allows for an extra level of assurance.
Formal methods differ from other system design techniques through the utilization of formal verification systems, such as theorem provers and model-checkers. Formal methods are necessary to avoid building/developing incomplete and/or incorrect systems due to unfinished, incompatible or ambiguous requirements. Formal methods can be applied to all steps of the software life-cycle and on various levels of abstraction.
Event-B is a formal modelling method for developing a system and formalism is widely accepted for the modelling and verification of complex systems. Event-B features the use of set theory, the use of the refinement paradigm and the use of mathematical theorem proving for developing and verifying systems at different levels of abstraction and in a correct-by-construction manner.
Event-B is a state-based formalism for the specification and verification of complex and critical systems with a focus on the behavioural and safety aspects. Event-B follows the correct-by-construction paradigm wherein the system model is developed in a refinement-based stepwise manner. Theorem proving is the underlining tool for the verification of the system model.
The UPPAAL toolbox is an environment developed as a collaborative effort by the Uppsala University and Aalborg University and it is used for modelling, validation and verification of real-time systems. The models are implemented as networks of timed automata which can be extended with data types (bounded integers, arrays, etc.).
UPPAAL Timed Automata (UTA) is a state-based formalism with a clear focus on the modelling and verification of real-time systems. UTA is well-supported by the UPPAAL toolbox for the modelling, simulation and verification of real-time systems. Verification is performed with the efficient built-in model-checker.
