This technique has been used in the verification of various
systems of industrial complexity such as aircraft controllers,
robotics systems and the PCI local bus, demonstrating that the
method proposed can be used to help solving practical problems.
Verus - A Compiler/Verifier for Real-Time Systems
To find out more about Verus, check out the (short) paper:
S. Campos, E. Clarke and M. Minea. The Verus tool: a quantitative approach to the formal verification
of real-time systems. In: Conference on Computer Aided Verification, 1997.
You can install Verus and see for yourself all its advantages (and disadvantages):
For more information, a good reference is:
Carnegie Mellon's model checking project home page
Back to the main