Online formal verification of executable models

摘要

A system and method for automatic formal verification of an executable model includes an assertion monitor configured to verify a system against an assertion in a specification. The assertion monitor includes a parser configured to generate a propositional formula representing the assertion in the specification using Boolean propositions, a filter configured to generate a run of the system using truth assignments for the propositional symbols, and a trace verifier configured to verify the assertion using the run of the system using truth assignments for the propositional symbols and the propositional formula.