Offering Formal Verification Capabilities for Industry Standard Case Tools: Challenges and Results

If formal verification techniques are to find their way into industrial design flows, then they must come disguised as sheep: they should appear to the designer of embedded control units as easy to use as, say, a simulator or a code generator. The talk presents a range of challenges which must be mastered to reach this far striving goal, touching upon such issues as diversity of commercially relevant modeling tools, semantic integration, complexity of models, handling of floating point variables, ease of use. Results are presented regarding solutions of these issues in offering verification support for the Statemate case tool of I-Logix, Inc, and its use in three application domains: avionics, automotive, and train systems.