Using Symbolic Execution to Check Global Temporal Requirements in an Application

• US 20100125832A1
• Filed: 11/14/2008
• Published: 05/20/2010
• Est. Priority Date: 11/14/2008
• Status: Active Grant

• Current Assignee: Fujitsu Limited
• Original Assignee: Fujitsu Limited
• Inventors: Rajan, Sreeranga P., Prasad, Mukul R., Ghosh, Indradeep
• Granted Patent: US 8,359,576 B2
• Time in Patent Office: Days
• US Class Current: 717/124
• CPC Class Codes: G06F 11/3604 Software analysis for verifying properties of programs byte-code verification G06F9/44589

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.

Claims

1. A method 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.

2. The method of claim 1, wherein solving a symbolic expression comprises:

negating the symbolic requirement;

generating a set of equations for the symbolic variables along each search path of the graph of the state space;

inserting one or more first branch points into the graph of the state space and keeping track of particular search path conditions along symbolic search paths in the graph of the state space associated with symbolic variables in branch conditions;

inserting one or more second branch points into the graph of the state space for symbolic events;

attempting to identify one or more solutions of the set of symbolic equations and search path conditions at an end of each search path of the graph of the state space, a solution indicating a violation of a global temporal requirement and comprising a counter example describing a failure causing the violation; and

if identified, communicating one or more solutions for presentation to a user as one or more test cases violating the global temporal requirement.

3. The method of claim 1, wherein the application is a web application.

4. The method of claim 1, wherein the business logic of the application is implemented in JAVA.

5. The method of claim 1, wherein the model of the application is implemented in JAVA.

6. The method of claim 1, wherein the model checker comprises an explicit state JAVA model checker.

7. The method of claim 1, wherein solving the symbolic expressions comprises using a decision procedure comprising one or more of integer linear programming (ILP), Boolean satisfiability (SAT) solving, or string finite state machine (FSM) solving, to attempt to identifying solutions to equations derived from the symbolic expressions, search path conditions, and the graph of the state space.

8. The method of claim 1, further comprising:

receiving from a user a selection of the one or more requirement templates in the library of requirement templates;

receiving from the user assignments of properties to the requirement templates, the assignments being expressed in a natural language; and

translating the assignments and the requirement templates to mathematically formal expressions comprehensible to the model checker, the translation generating the global temporal requirements of the application.

9. The method of claim 1, further comprising:

accessing source code of the application;

accessing the use cases for the application;

copying the business logic of the application from the source code;

generating one or more rudimentary models or empty stubs for one or more components of the application that are not business logic;

combining the copied business logic with the rudimentary models or the empty stubs to generate the model of the application.

10. Software embodied in one or more 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.

11. The software of claim 10, operable, to solve a symbolic expression, to:

negate the symbolic requirement;

generate a set of equations for the symbolic variables along each search path of the graph of the state space;

insert one or more first branch points into the graph of the state space and keeping track of particular search path conditions along symbolic search paths in the graph of the state space associated with symbolic variables in branch conditions;

insert one or more second branch points into the graph of the state space for symbolic events;

attempt to identify one or more solutions of the set of symbolic equations and search path conditions at an end of each search path of the graph of the state space, a solution indicating a violation of a global temporal requirement and comprising a counter example describing a failure causing the violation; and

if identified, communicate one or more solutions for presentation to a user as one or more test cases violating the global temporal requirement.

12. The software of claim 10, wherein the application is a web application.

13. The software of claim 10, wherein the business logic of the application is implemented in JAVA.

14. The software of claim 10, wherein the model of the application is implemented in JAVA.

15. The software of claim 10, wherein the model checker comprises an explicit state JAVA model checker.

16. The software of claim 10, operable, to solve the symbolic expressions, to use a decision procedure comprising one or more of integer linear programming (ILP), Boolean satisfiability (SAT) solving, or string finite state machine (FSM) solving, to attempt to identifying solutions to equations derived from the symbolic expressions, search path conditions, and the graph of the state space.

17. The software of claim 10, further operable to:

receive from a user a selection of the one or more requirement templates in the library of requirement templates;

receive from the user assignments of properties to the requirement templates, the assignments being expressed in a natural language; and

translate the assignments and the requirement templates to mathematically formal expressions comprehensible to the model checker, the translation generating the global temporal requirements of the application.

18. The software of claim 10, further operable to:

access source code of the application;

access the use cases for the application;

copy the business logic of the application from the source code;

generate one or more rudimentary models or empty stubs for one or more components of the application that are not business logic;

combine the copied business logic with the rudimentary models or the empty stubs to generate the model of the application.

19. A system 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.