Formal Verification as a Design Tool - The Transponder Lock Example

We describe a methodology for the construction and validation of embedded systems with real-time constraints. Our methodology is based on object-oriented techniques and synchronous programming. This greatly eases the use of formal verification to analyse the system, particularly to support design decisions. We use model checking to verify reactive behaviors and theorem proving to verify datatype behaviors. Our approach has been applied to develop industrial products. It is illustrated here with such a development, a transponder lock.