Lucent Technologies Inc.

Gerard Johan Holzmann

Mihalis Yannakakis

Doron A Peled

Kenneth Lane Thompson

Philip Steven Winterbottom

James J Striegel

Margaret H Holzmann

A method and apparatus for generating a covering set of test cases from a directed graph is provided. The directed graph includes nodes and edges connecting the nodes, and a test case is a path through the directed graph. To generate a partial set of test cases, a set of selected test cases is received. These test cases can be manually selected or they can be a maintained test case set. The edges or nodes on the directed graph (or requirements linked to nodes or edges) that are covered by the selected test cases are marked with an identifier. Test cases are then generated from the directed graph according to a coverage algorithm. Marked graph elements may, but need not, be included in the generated test cases. The resulting partial test case set together with the selected test cases satisfy the coverage criterion.

Automatic generation and regeneration of a covering test case set from a model

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.

Method and apparatus for testing event driven software

Techniques and testers for testing a system U including the steps of (a) defining a formal specification of a logical property P that system U is required not to satisfy; (b) generating a passive testing module T based upon property P to monitor system U; (c) invoking a function F at specific invocation points during the execution of system U to compute an abstract representation of the state of system U at the current point of execution; (d) passing the abstract representation computed by function F to passive testing module T in order to determine whether the abstract representation of the execution of system U to the current point matches illegal property P; and (e) declaring a 'fail' result if the abstract representation of the execution of system U to the current point matches illegal property P and declaring a 'pass' result if the abstract representation of the execution of system U to the current point does not match illegal property P.

Methods and apparatus for generating passive testers from properties

Apparatus and methods for communicating using protocols. The apparatus and methods employ protocol descriptions written in a device-independent protocol description language. A protocol is executed by employing a protocol description language interpreter to interpret the protocol description. Communication using any protocol for which there is a protocol description may be done by means of a general protocol. The general protocol includes a first general protocol message which includes a protocol description for a specific protocol. The protocol apparatus which receives the first protocol message employs a protocol description language interpreter to interpret the included protocol description and thereby to execute the specific protocol. The protocol apparatus may also be made to adapt to its environment by encaching protocol descriptions which were received in an earlier first general protocol message and interpreting an encached protocol description in response to a second general protocol message which includes a protocol identifier specifying the encached protocol description.

Apparatus and method for communicating data between elements of a

Apparatus and methods for editing message sequence charts and determining whether a message sequence chart is consistent with a semantic of the system which the message sequence chart represents. As an editor, the apparatus maintains an internal representation of the message sequence chart as a set of processes and events, displays an image of the message sequence chart, and modifies the internal representation in response to modifications of the image by the user. The internal representation can be used to produce further representations of the message sequence chart. One of the representations is an event list which lists send events and receive events in the message sequence chart in a visual order. The event list is used together with a semantic provided by the user of the apparatus to determine whether there is an inconsistency between the message sequence chart and the semantic.

Message sequence chart analyzer

An on-the-fly verification system which employs statically-available information to reduce the size of the state space required to verify liveness and safety properties of a target system consisting of asynchronous communicating processes. The verification system generates a verifier from a description of the target system and a specification of the property to be verified. The verifier models the target system as a set of finite state machines, constructs a state space containing a graph of nodes representing states of the target system and transitions between the states, and uses the state space to verify the property. The size of the state space is reduced by using information from the description and the specification to divide transitions from a node into per-process bundles and to determine which bundles of transitions must be included in the state space and which may be left out of the state space. The state space reduction technique never increases the size of the state space and often reduces it by orders of magnitude.

On-the-fly model checking with partial-order state space reduction

The present invention involves a method of deriving the height and width of a graphic image from raw graphical image data stored in a computer system. It includes commencing execution of a height-width derivation program in the computer system and, at least once, operating the height-width derivation program to perform a series of steps. These include calculating the area of the image size, e.g. using the total number of bytes, and calculating the square root of the area to obtain a first value, and then determining by assumption a first assumed width and a first assumed height. For example, these assumptions may be achieved by calculating one half of the first value to obtain a first assumed width value and dividing the area by the first assumed width value to obtain a first assumed height value. Next, the first assumed height value and first assumed width value are rounded to the nearest whole number, further adjusting said values by predetermined increments and the resulting adjusted values are multiplied until their product produces the closest value equal to the area of the image size to obtain a second assumed height value and a second assumed width value. The method also involves a series of iterations to determine error indexes for various altered assumed values and finding the values with the lowest error index.

Growing community of inventors

Murray Hill, NJ, United States of America

Gerard Johan Holzmann