Data processing: software development – installation – and managem – Software program development tool – Translation of code
Reexamination Certificate
1998-03-30
2001-09-11
Powell, Mark (Department: 2122)
Data processing: software development, installation, and managem
Software program development tool
Translation of code
C717S152000
Reexamination Certificate
active
06289502
ABSTRACT:
BACKGROUND
The invention relates to software design and validation.
An important aspect of software development involves validating that an implementation of a design will function correctly and have desired operating properties. Over time, software systems have become increasingly complex and validation of these systems has become increasingly difficult. This is particularly true of distributed systems that are formed from multiple interacting and asynchronously operating components. Distributed systems include not only physically distributed architectures in which components execute on physically separated computers coupled by communication paths, for example, over data networks, but also include architectures in which multiple components execute on a single computer and are controlled as distinct tasks (e.g., processes or threads). In order to validate such software systems, ad hoc approaches to testing cannot in general be relied on due to the complexity of the overall system.
Formal specifications for abstracted designs of software systems have been used to validate properties of the abstracted designs. One approach to specifying such designs uses the formalism of Input/Output (I/O) Automata, as described in Chapter 8 of the textbook,
Distributed Algorithms,
by Nancy Lynch (Morgan Kaufmann Publishers, 1996, ISBN 1-55860-348-4), which is incorporated herein by reference. An I/O automaton is a labeled transition system model (i.e., a state machine with labeled state transitions) for one or more components of a system, and can be used to model components of an asynchronous concurrent system.
One method of validating properties of a system design, in particular of system designs specified using I/O automata, uses a theorem proving approach. In such an approach, properties of the system design that are to be validated are expressed as logical assertions (predicates), and underlying statements about the system design are expressed as logical axioms. The axioms generally relate to the detailed operation of the system, while the assertions relate to the overall aspects of its desired behavior. A user then verifies by hand that the properties are necessarily true given the axioms, or may possibly use a user-assisted program, such as a theorem proving program, to aid in this verification.
Other methods for validating system properties can also be used. One approach, known as “model checking,” is based on exhaustive checking of all states in an instance of a system design in which the size of the system (i.e., the number of states) is restricted. Another approach is based on simulation of the operation of the system, in which a typically more complex (e.g., larger number of states) instance of the system is checked by examining a sample sequence of states or of transition labels (“actions”) resulting from execution of the system.
SUMMARY
The present invention uses a new computer language which is based on a formal, mathematical state-machine model, and which is used both to validate and to generate code for a distributed system. In general, use of this new language enables developing a system using multiple related system specifications (i.e., precise descriptions), for instance, using system specifications at multiple levels of abstraction or using multiple system decompositions into parallel combinations of interacting systems, and allows use of validation tools to verify properties of these systems and their relationships. The language includes constructs for specifying non-deterministic actions, and for specifying constraints on those non-deterministic choices. Several well-defined sub-languages of the full computer language are also defined. These sub-languages are used to specify the input of some tools, in particular, of some code generators.
In one aspect, in general, the invention is a method for developing a software implementation of a distributed system. The method includes accepting a design specification for the distributed system, including accepting specifications of multiple state machines, and accepting a specification of desired properties of the state machines. The method also includes applying a validation procedure to the design specification to verify that the state machines have the desired properties, including applying a theorem proving procedure to the design specification, and also includes applying a code generating procedure to the specifications of the state machines to generate multiple software implementations for components of the distributed system.
The invention can include one or more of the following features.
The state machines can include node state machines and channel state machines, and applying the code generating procedure to the specifications of the state machines can include, for each of the node state machines, applying a translation procedure to the specification of the node state machine to generate a software implementation of that node state machine.
The specification of each state machine can include a specification of a multiple state variables, the values of which determine the state of the state machine, and also include a specification of multiple state transitions. Each specification of a state transition includes a specification of values of the state variables in a state in which the transition can be taken, and a specification of an effect on the values of the state variables when that transition is taken. Furthermore, the specification of the effect on the values of the state variables can include an instruction to set one of the state variables to a non-deterministic choice of values, as well as a logical constraint on the values of the state variables resulting from taking the transition.
The specifications of the properties of the state machines can include a logical assertion involving states of the state machines.
The step of applying the theorem proving procedure to the design specification can include translating the design specification into a logical language of a theorem prover and providing the translated design specification to a theorem prover, such as a software based theorem proving program. The theorem prover can be an equational theorem prover.
Applying the validation procedure can include applying a simulation procedure to one of the state machines, including determining a sequence of states of the state machine, and verifying one of the desired properties in each of the sequence of states. Applying the validation procedure can further include applying a model checking procedure to one of the plurality of state machines, including enumerating the states of the state machine, and verifying one of the desired properties in each of the enumerated states. Applying the validation procedure can also include deriving a second design specification from the accepted design specification, wherein the derived design specification has a property, such as deterministic behavior or specification using a single state machine, that the accepted design specification does not have, and then applying a second validation procedure to the derived design specification.
In another aspect, in general, the invention is a method for developing a software implementation of a distributed system. The method includes accepting a first design specification including accepting specifications of a first set of state machines, and accepting a specification of a first set of desired properties of the first set of state machines. The method also includes applying a first validation procedure to the first design specification to verify that the first set of state machines has the first desired properties, including applying a theorem proving procedure to the first design specification. The method also includes accepting a second design specification, including accepting specifications of a second set of state machines, and accepting a specification of a desired relationship between the first set of state machines and the second set of state machines. The method further includes applying a second validation procedure to the second design
Garland Stephen J.
Lynch Nancy A.
Fish & Richardson P.C.
Massachusetts Institute of Technology
Powell Mark
Zhen Wei
LandOfFree
Model-based software design and validation does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Model-based software design and validation, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Model-based software design and validation will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2442604