Using symbolic execution to check global temporal requirements in an application
US8359576B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Nov 14, 2008 |
| Grant date | Jan 22, 2013 |
| Priority date | — |
| Expiry date | Nov 23, 2031 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3604
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
In one embodiment, a method include accessing one or more global temporal requirements of an application specified using one or more requirement templates from a library of requirement templates, accessing a model of the application, generating one or more symbolic expressions of one or more of the global temporal requirements of the application, searching a state space of the application model with a model checker, monitoring the search of the state space for events in the state space encompassed by the symbolic expressions and modifying construction of a graph of the state space in response to occurrence of one or more events encompassed by the symbolic expressions, evaluating the symbolic expressions based on the graph of the state space to determine whether one or more of the global temporal requirements are valid, and communicating one or more results of the evaluation of the symbolic expressions for presentation to a user.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.