Online formal verification of executable models
First Claim
Patent Images
1. A method for verifying a system against an assertion in a specification, the method comprising the steps of:
- generating a propositional formula representing an assertion in the specification using Boolean propositions, each Boolean proposition being associated with an atomic assertion in the assertion;
generating a test case designed to assess the a behavior of the system with respect to the assertion;
generating configuration data in response to a simulation of the test case on the system;
converting the configuration data into propositional symbols;
generating a run of the system using the propositional symbols;
converting the run of the system to propositional symbols so that the propositional symbols hold data from the configuration data and from the run of the system; and
verifying the assertion using the propositional symbols and the propositional formula.
8 Assignments
0 Petitions
Accused Products
Abstract
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.
-
Citations
17 Claims
-
1. A method for verifying a system against an assertion in a specification, the method comprising the steps of:
-
generating a propositional formula representing an assertion in the specification using Boolean propositions, each Boolean proposition being associated with an atomic assertion in the assertion; generating a test case designed to assess the a behavior of the system with respect to the assertion; generating configuration data in response to a simulation of the test case on the system; converting the configuration data into propositional symbols; generating a run of the system using the propositional symbols; converting the run of the system to propositional symbols so that the propositional symbols hold data from the configuration data and from the run of the system; and verifying the assertion using the propositional symbols and the propositional formula. - View Dependent Claims (2, 3, 4, 5, 6, 11)
-
-
7. A non-transitory computer-readable medium tangibly embodying computer-executable instructions for:
-
generating a propositional formula representing an assertion in the specification using Boolean propositions, each Boolean proposition being associated with an atomic assertion in the assertion; generating a test case designed to assess a behavior of a system with respect to the assertion; generating configuration data in response to a simulation of the test case on the system; converting the configuration data into propositional symbols; generating a run of the system using the propositional symbols; converting the run of the system to propositional symbols so that the propositional symbols hold data from the configuration data and from the run of the system; and verifying the assertion using the propositional symbols and the propositional formula. - View Dependent Claims (8, 9, 10)
-
-
12. An assertion monitor configured to verify a system against an assertion in a specification, the assertion monitor comprising:
-
a computer with a memory running an assertion monitor program that 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 propositional symbols; a converter configured to convert the run of the system to propositional symbols so that the propositional symbols hold data from the configuration data and from the run of the system; and a trace verifier configured to verify the assertion using the propositional symbols and the propositional formula. - View Dependent Claims (13, 14, 15, 16, 17)
-
Specification