Method and apparatus for testing event driven software

• US 6,353,896 B1
• Filed: 12/15/1998
• Issued: 03/05/2002
• Est. Priority Date: 12/15/1998
• Status: Expired due to Term

• Current Assignee: WSOU Investments, LLC (WSOU Holdings, LLC)
• Original Assignee: Lucent Technologies, Inc. (Nokia Corporation)
• Inventors: Winterbottom, Philip Steven, Thompson, Kenneth Lane, Holzmann, Gerard Johan
• Primary Examiner(s): Ray, Gopal C.
• Application Number:
  US09/211,967
• Time in Patent Office: 1,176 Days
• Field of Search: 714/25, 714/38, 714/32, 714/33, 717/1, 717/4, 717/5, 709/302, 703/13, 703/16, 703/17
• US Class Current: 714/38.1
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013
• CPC Class Codes: G06F 11/3688 for test execution, e.g. scheduling of test suites
• CPC Class Codes: G06F 8/436 Semantic checking

Abstract

A technique for testing event driven software. In accordance with the technique, the source code of the event driven software is directly converted to an automation based model useful in verifying that the program code complies with the desired properties defined by the user. More particularly, the event driven system program code is translated into a target language for a particular model checker. Such a translation results in a model which contains statements directed at whether execution of the program code will affect the behavior of the event driven system. Thus, this model extraction process can be used as input to a logic model checker for determining whether event driven system complies with the desired correctness properties specified by the user. Advantageously, the model extraction process and application of the model checker occurs in a direct and dynamic fashion from the subject event driven system program code without the need for user intervention.

Claims

1. A software testing method comprising:

providing a source program of the software, the source program including a plurality of instructions which contain a first source code segment for causing a computer to execute a event driven system;

the first source code segment including a first plurality of instructions defining a plurality of control states, the plurality of control states being associated with the event driven system, a second plurality of instructions defining a plurality of events of the event driven system, and a third plurality of instructions defining a plurality of actions of the event driven system, each control state of the plurality of control states having an individual identifier within the first plurality of instructions of the first source code segment, the individual identifier being a programming symbol which is common to all the identified control states, and a second source code segment containing at least one plurality of instructions defining a sequential control of the computer executing the event driven system;

parsing the source program to identify the plurality of control states and converting the source program to a state machine format;

applying a translation map to the plurality of instructions of the source program;

converting the state machine format of the source program to a verification program;

applying an environmental model to the verification program; and

testing the software in a verification tool using the verification program.

2. The software testing method of claim 1, wherein the translation map includes a plurality of mapping instructions.

3. The software testing method of claim 2, wherein the applying the translation map operation includes:

comparing the plurality of mapping instructions to the plurality of instructions of the source program to detect a match; and

converting particular ones of the mapping instructions which match particular ones of the instructions of the source program to an input language of a model checker.

4. The software testing method of claim 2, wherein the environmental model includes a plurality operational attributes of the event driven system.

5. The software testing method of claim 1, wherein the verification tool is a model checker tool.

6. The software testing method of claim 5, wherein the model checker tool is a SPIN model checker tool.

7. A software testing apparatus comprising:

means for providing a source program of the software, the source program containing a first source code segment for causing a computer to execute an event driven system, the first source code segment including a first plurality of instructions defining a plurality of control states, the plurality of control states being associated with the event driven system, a second plurality of instructions defining a plurality of events of the event driven system, and a third plurality of instructions defining a plurality of actions of the event driven system, each control state of the plurality of control states having an individual identifier within the first plurality of instructions of the first source code segment, the individual identifier being a programming symbol which is common to all the identified control states, and a second source code segment containing at least one plurality of instructions defining a sequential control of the computer executing the event driven system;

means for parsing the source program to identify the plurality of control states and means for converting the source program to a state machine format;

means for applying a translation map to the plurality of instructions of the source program;

means for converting the state machine format of the source program to a model checker program in an input language of a model checker;

means for applying an environmental model to the model checker program;

means for testing the software in the model checker using the model checker program; and

means for displaying a result of the testing of the software.

8. The software testing apparatus of claim 7, wherein the translation map includes a plurality of mapping instructions.

9. The software testing apparatus of claim 8, wherein the means for applying the translation map includes:

means for comparing the plurality of mapping instructions to the plurality of instructions of the source program to detect a match; and

means for converting particular ones of the mapping instructions which match particular ones of the instructions of the source program to the input language of the model checker.

10. The software testing apparatus of claim 9, wherein the environmental model includes a plurality operational attributes of the event driven system.

11. A machine-readable medium having stored thereon a plurality of instructions, the plurality of instructions including instructions that, when executed by a machine, cause the machine to perform a method of:

testing event driven software by parsing a source program of the software to identify a plurality of control states and converting the source program to a state machine format, the source program containing a first source code segment for causing a computer to execute the event driven system, the first source code segment including a first plurality of instructions defining a plurality of control states, the plurality of control states being associated with the event driven system, a second plurality of instructions defining a plurality of events of the event driven system, and a third plurality of instructions defining a plurality of actions of the event driven system, each control state of the plurality of control states having an individual identifier within the first plurality of instructions of the first source code segment, the individual identifier being a programming symbol which is common to all the identified control states, and a second source code segment containing at least one plurality of instructions defining a sequential control of the computer executing the event driven system;

applying a translation map to the source program;

converting the state machine format of the source program to a verification program; and

applying an environmental model to the verification program, and testing the software by applying the verification program to a verification system.

12. The machine-readable medium of claim 11, wherein the verification system applies the verification program to a SPIN model checker.

13. The machine-readable medium of claim 12, wherein the event driven system is a telecommunications service application, the telecommunications service application having at least one event associated with extending a telephone call through a communications network.

14. The machine-readable medium of claim 13, wherein the state machine format is converted using a specification defined by a user.

15. A software testing system comprising:

a computer having at least one memory;

means for receiving a series of programming language statements in the memory, the series of programming language statements comprising a first source code segment and a second source code segment for causing the computer to execute an event driven system, the first source code segment including a first plurality of instructions defining a plurality of control states of the event driven system, a second plurality of instructions defining a plurality of events of the event driven system, and a third plurality of instructions defining a plurality of actions of the event driven system, each control state of the plurality of control states having an individual identifier within the first plurality of instructions of the first source code segment, the individual identifier being a programming symbol which is common to all the identified control states, the second source code segment containing at least one plurality of instructions defining a sequential control of the computer in executing the event driven system;

means for parsing the first source code segment to identify the plurality of control states and means for converting the first source code segment and the second source code segment to a state machine format;

means for applying a translation map to the first source code segment and the second source code segment;

means for converting the state machine format to a model checker program in an input language of a model checker;

means for applying an environmental model to the model checker program;

means for testing the software in the model checker using the model checker program; and

means for displaying a result of the testing of the software.

16. The software testing system of claim 15, further comprising:

means for compiling the first source code segment and the second source code segment into an object program in the memory; and

means for executing the object program in the computer to provide the event driven system.

17. The software testing system of claim 16, wherein the means for testing uses at least one set of properties defined by a user associated with the execution of the event driven system.

18. The software testing system of claim 17, wherein the translation map is specified by the user.

19. The software testing system of claim 18, wherein the translation map, the environmental model, and the series of programming statements are each written in a C programming language.

20.The software testing system of claim 16, wherein the model checker is a SPIN model checker.

22. The software testing system of claim 15, wherein the event driven system is a telecommunications service application, the telecommunications service application having at least one event associated with extending a telephone call through a communications network.

20. The software testing system of claim 20, wherein the state machine format is converted using a specification defined by a user.

21. The software testing system of claim 20, wherein the displayed result includes at least one full automaton representation of the event driven system.