Model-based software design and validation

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.

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, 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.

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.

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.

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.