TAPAS

The formal design and verification of safety-critical systems demand to consider both functional and time aspects from the very beginning and with the same importance. However, in State-Based Formal Methods, handling time is still a challenge as it is often addressed too late, after several refinement steps, using manual and ad-hoc solutions. Also, there are lots of optimized solutions to handle rich models of time but with a rather limited consideration for other kinds of requirements and weak, if any, integration with proof assistants. We focus on time but we intend to deal with other non functional properties. However many of them directly or indirectly depend on time (energy, heat, security). Time by nature has also a particular importance in hybrid systems or in cyber-physical systems when the physical processes are ofter captured as differential equations demanding a clear integration of time. We propose a platform and a methodology for a joint use of Event-B and clock-based models to address both functional and time requirements, making time a first class citizen. It makes the proof assistants more efficient by cutting long proofs with the help of model-checkers when considering decidable parts. It goes beyond the current limitations of model-checkers restricted to a bounded domains by using inductive reasoning to generalize results from bounded domains to infinite ones. This would achieve a breakthrough in the formal guarantees offered by formal methods for critical systems by making the best of both communities that tend to operate separately.