Using symbolic execution to check global temporal requirements in an application
First Claim
1. A method executed by at least one processor, comprising:
- accessing one or more global temporal requirements of an application specified using one or more requirement templates from a library of requirement templates, the application comprising business logic;
accessing a model of the application, the model comprising the business logic of the application and one or more use cases for the application;
generating one or more symbolic requirements from one or more variables in one or more of the global temporal requirements specified as symbolic variables;
generating one or more symbolic expressions and one or more search path conditions for one or more variables in one or more of the global temporal requirements with values from symbolic inputs derived from one or more use cases for the application;
searching a state space of the application model with a model checker, the search comprising constructing and analyzing a graph of the state space and creating and maintaining one or more symbolic expressions and one or more search paths during the search;
monitoring the search of the state space for events in the state space encompassed by the symbolic requirements and modifying the construction of the graph of the state space to record potential occurrence of one or more events encompassed by the symbolic requirements;
solving one or more symbolic expressions from one or more of the symbolic requirements at one or more ends of one or more search paths in the graph of the state space to determine whether one or more of the symbolic requirements are valid; and
communicating whether one or more of the symbolic requirements are valid for presentation to a user.
1 Assignment
0 Petitions
Accused Products
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.
-
Citations
19 Claims
-
1. A method executed by at least one processor, comprising:
-
accessing one or more global temporal requirements of an application specified using one or more requirement templates from a library of requirement templates, the application comprising business logic; accessing a model of the application, the model comprising the business logic of the application and one or more use cases for the application; generating one or more symbolic requirements from one or more variables in one or more of the global temporal requirements specified as symbolic variables; generating one or more symbolic expressions and one or more search path conditions for one or more variables in one or more of the global temporal requirements with values from symbolic inputs derived from one or more use cases for the application; searching a state space of the application model with a model checker, the search comprising constructing and analyzing a graph of the state space and creating and maintaining one or more symbolic expressions and one or more search paths during the search; monitoring the search of the state space for events in the state space encompassed by the symbolic requirements and modifying the construction of the graph of the state space to record potential occurrence of one or more events encompassed by the symbolic requirements; solving one or more symbolic expressions from one or more of the symbolic requirements at one or more ends of one or more search paths in the graph of the state space to determine whether one or more of the symbolic requirements are valid; and communicating whether one or more of the symbolic requirements are valid for presentation to a user. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9)
-
-
10. Software embodied in one or more non-transitory computer-readable tangible media and when executed operable to:
-
access one or more global temporal requirements of an application specified using one or more requirement templates from a library of requirement templates, the application comprising business logic; access a model of the application, the model comprising the business logic of the application and one or more use cases for the application; generate one or more symbolic requirements from one or more variables in one or more of the global temporal requirements specified as symbolic variables; generate one or more symbolic expressions and one or more search path conditions for one or more variables in one or more of the global temporal requirements with values from symbolic inputs derived from one or more use cases for the application; search a state space of the application model with a model checker, the search comprising constructing and analyzing a graph of the state space and creating and maintaining one or more symbolic expressions and one or more search paths during the search; monitor the search of the state space for events in the state space encompassed by the symbolic requirements and modifying the construction of the graph of the state space to record potential occurrence of one or more events encompassed by the symbolic requirements; solve one or more symbolic expressions from one or more of the symbolic requirements at one or more ends of one or more search paths in the graph of the state space to determine whether one or more of the symbolic requirements are valid; and communicate whether one or more of the symbolic requirements are valid for presentation to a user. - View Dependent Claims (11, 12, 13, 14, 15, 16, 17, 18)
-
-
19. A system comprising:
-
a processor; a memory storing executable instructions for execution by the processor, the instructions further comprising; means for accessing one or more global temporal requirements of an application specified using one or more requirement templates from a library of requirement templates, the application comprising business logic; means for accessing a model of the application, the model comprising the business logic of the application and one or more use cases for the application; means for generating one or more symbolic requirements from one or more variables in one or more of the global temporal requirements specified as symbolic variables; means for generating one or more symbolic expressions and one or more search path conditions for one or more variables in one or more of the global temporal requirements with values from symbolic inputs derived from one or more use cases for the application; means for searching a state space of the application model with a model checker, the search comprising constructing and analyzing a graph of the state space and creating and maintaining one or more symbolic expressions and one or more search paths during the search; means for monitoring the search of the state space for events in the state space encompassed by the symbolic requirements and modifying the construction of the graph of the state space to record potential occurrence of one or more events encompassed by the symbolic requirements; means for solving one or more symbolic expressions from one or more of the symbolic requirements at one or more ends of one or more search paths in the graph of the state space to determine whether one or more of the symbolic requirements are valid; and means for communicating whether one or more of the symbolic requirements are valid for presentation to a user.
-
Specification