Model-based software design and validation
First Claim
1. A method for developing a software implementation of a distributed system, comprising:
- accepting a design specification for the distributed system, including accepting specifications of a plurality of interacting asynchronous state machines, wherein at least some of the state machines exhibit non-deterministic behavior, and accepting a specification of desired properties of the distributed system, including accepting a logical property that is desired to be satisfied in any state of the state machines that can be reached during execution of the distributed system;
applying a validation procedure to the design specification to verify that the distributed system has the desired properties, including applying a theorem proving procedure to the design specification, including proving that the logical property is satisfied; and
applying a code generating procedure to the specifications of one or more of the state machines to generate software implementations for components of the distributed system.
1 Assignment
0 Petitions
Accused Products
Abstract
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, enables developing a system using multiple related system specifications, 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. One method for developing a software implementation of a distributed system using the present invention includes accepting a design specification for the distributed system, and applying a validation procedure to the design specification to verify that the system has desired properties. This validation includes applying a theorem proving procedure to the design specification. The method also includes applying a code generating procedure to the specification to generate multiple software implementations for components of the distributed system.
172 Citations
29 Claims
-
1. A method for developing a software implementation of a distributed system, comprising:
-
accepting a design specification for the distributed system, including accepting specifications of a plurality of interacting asynchronous state machines, wherein at least some of the state machines exhibit non-deterministic behavior, and accepting a specification of desired properties of the distributed system, including accepting a logical property that is desired to be satisfied in any state of the state machines that can be reached during execution of the distributed system;
applying a validation procedure to the design specification to verify that the distributed system has the desired properties, including applying a theorem proving procedure to the design specification, including proving that the logical property is satisfied; and
applying a code generating procedure to the specifications of one or more of the state machines to generate software implementations for components of the distributed system. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10)
a specification of a plurality of state variables, wherein values of the state variables determine the state of the state machine; and
a specification of a plurality of state transitions, each specification of a state transition including 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.
-
-
4. The method of claim 3 wherein the specification of the effect on the values of the state variables includes an instruction to set one of the state variables to a non-deterministic choice of values.
-
5. The method of claim 4 wherein the specification of the effect on the values of the state variables includes a logical constraint on the values of the state variables resulting from taking the transition.
-
6. The method of claim 1 wherein applying the theorem proving procedure to the design specification includes:
-
automatically translating the design specification into a logical language of a theorem prover; and
providing the translated design specification to a theorem prover.
-
-
7. The method of claim 6 wherein the theorem prover is an equational theorem prover, and each of the specifications of the state machines includes a specification of a plurality of state variables, each state variable having a data type, and values of the state variables determine the state of the state machine, wherein
applying the theorem prover includes accepting axiomatic definitions of the data types of the state variables. -
8. The method of claim 1 wherein applying the validation procedure further includes applying a simulation procedure to one of the plurality of state machines, including determining a sequence of states of the state machine, and verifying that the logical property is satisfied in each of the sequence of states.
-
9. The method of claim 1 wherein applying the validation procedure further includes applying a model checking procedure to one of the plurality of state machines, including enumerating the states of the state machine, and verifying that the logical property is satisfied in each of the enumerated states.
-
10. The method of claim 1 wherein accepting specification of a plurality of interacting asynchronous state machines includes accepting a specification of an infinite-state state machine.
-
11. A method for developing a software implementation of a distributed system, comprising:
-
accepting a first design specification for the distributed system, including accepting specifications of a first plurality of state machines, and accepting a specification of desired properties of the first plurality of state machines;
applying a validation procedure to the first design specification to verify that the first plurality of state machines has the desired properties, including applying a theorem proving procedure to the first design specification, determining a second design specification from the accepted design specification, wherein the second design specification has a property that the first design specification does not have, and applying a second validation procedure to the second design specification; and
applying a code generating procedure to the specifications of one or more of the first plurality of state machines to generate software implementations for components of the distributed system. - View Dependent Claims (12, 13, 14, 15, 16, 17, 18)
-
-
19. A method for developing a software implementation of a distributed system, comprising:
-
accepting a first design specification including accepting specifications of a first plurality of state machines, and accepting a specification of a first plurality of desired properties of the first plurality of state machines;
applying a first validation procedure to the first design specification to verify that the first plurality of state machines has the first desired properties, including applying a theorem proving procedure to the first design specification;
accepting a second design specification, includingaccepting specifications of a second plurality of state machines, and accepting a specification of a desired relationship between the first plurality of state machines and the second plurality of state machines;
applying a second validation procedure to the second design specification to verify that the first plurality of state machines and the second plurality of state machines have the desired relationship; and
for one or more of the second plurality of state machines, applying a code generating procedure to the specification of the state machine to generate a software implementation of that state machine. - View Dependent Claims (20, 21, 22, 23, 24, 25, 26)
refining the first design specification to yield the second design specification.
-
-
21. The method of claim 20 wherein refining the first design specification includes expressing the specification of the second plurality of state machines using a restricted sublanguage of the language used to express the specification of the first plurality of state machines.
-
22. The method of claim 21 wherein the specification of the first plurality of state machines includes a specification of non-deterministic behavior of the state machines, and the restricted sublanguage does not permit specification of non-deterministic behavior.
-
23. The method of claim 19 wherein accepting a specification of a desired relationship between the first plurality of state machines and the second plurality of state machines includes:
-
accepting a desired relationship between a first one of the first plurality of state machines and a second one of the second plurality of state machines, including accepting an association of the states of the first state machine and states of the second state machine, and accepting an association of state transitions of the first state machine and sequences of one or more state transitions of the second state machine.
-
-
24. The method of claim 19 further comprising accepting a software implementation of one of the second plurality of state machines wherein the software implementation was determined prior to accepting the design specification for the distributed system.
-
25. The method of claim 19 further comprising implementing one of the second plurality of state machines using a communication channel.
-
26. The method of claim 19 further comprising applying a third validation procedure to the second design specification to verify that the second plurality of state machines has second desired properties.
-
27. Software stored on a computer readable medium comprising instructions for causing a computer to perform the functions of:
-
accepting a design specification for a distributed system, including accepting specifications of a plurality of interacting asynchronous state machines, wherein at least some of the state machines exhibit non-deterministic behavior, and accepting a specification of desired properties of the distributed system, including accepting a logical property that is desired to be satisfied in any state of the state machines that can be reached during execution of the distributed system;
applying a validation procedure to the design specification to verify that the distributed system has the desired property, including applying a theorem proving procedure to the design specification; and
applying a code generating procedure to the specifications of the state machines to generate a plurality of software implementations for distributed components of the distributed system.
-
-
28. Software stored on a computer readable medium comprising instructions for causing a computer to perform the functions of:
-
accepting a first design specification for a distributed system, including accepting specifications of a first plurality of state machines, and accepting a specification of a first plurality of desired properties of the first plurality of state machines;
applying a first validation procedure to the first design specification to verify that the first plurality of state machines has the first desired properties, including applying a theorem proving procedure to the first design specification;
accepting a second design specification, including accepting specifications of a second plurality of state machines, and accepting a specification of a desired relationship between the first plurality of state machines and the second plurality of state machines;
applying a second validation procedure to the second design specification to verify that the first plurality of state machines and the second plurality of state machines have the desired relationship; and
for one or more of the second plurality of state machines, applying a code generating procedure to the specification of the state machine to generate a software implementation of that state machine.
-
-
29. A system for iterative development of a software implementation of a distributed system, comprising:
-
a means for accepting a first design specification for the distributed system, wherein the first design specification includes specifications of a first plurality of state machines, and includes a specification of desired properties of the plurality of first state machines;
a means for verifying that the first state machines have the desired properties;
a means for accepting a second design specification, wherein the second design specification includes specifications of a second plurality of state machines, and includes a specification of a desired relationship between the first plurality of state machines and the second plurality of state machines;
a means for verifying that the first plurality of state machines and the second plurality of state machines have the desired relationship;
a code generator for producing a plurality of software implementations of components of the distributed system from the specifications of the second plurality of state machines.
-
Specification