Apparatus for defining properties in finite-state machines

An apparatus for defining a system design specification for any system the behavioral attributes of which can be expressed in terms a succession of transitions from one system model state to a succeeding model state, the apparatus comprising:

• means for selecting a template from a fixed predetermined library comprising a finite set of templates, said selected template having a set of qualifiers and a set of a fixed number of entry spaces, each qualifier being associated with an entry space, the totality of templates in the library defining a set of behavioral attribute types of any such system;
• and
• means for inputting at least one system expression into said set of entry spaces of said selected template, one expression per entry space, said at least one system expression and said associated qualifiers, in combination, defining a specific behavioral attribute of a particular such system.

An apparatus for defining a design specification of any system the behaviors of which can be expressed in terms of a succession of transitions from one system model state to a succeeding model state, the apparatus comprising a fixed finite set of templates, the totality of templates defining a set of behavior types of any such system, each template having one or more than one fixed number of entry spaces for accepting one system expression per entry space comprising at least a selected one of fulfilling conditions which define events required by a system behavior, enabling conditions, and discharging conditions which signify conditions after which said fulfilling conditions are no longer required such that said template, when filled with said system expression, defines a specific behavior of a particular such system.

A method of defining a design specification for any system the behaviors of which can be expressed in terms of a succession of transitions from one model state to a succeeding model state, the method comprising the steps of:

• receiving a set of inputs, each input representing a parameter that describes a system attribute;
• and
• filling a set of templates, selected from a fixed predetermined finite template set, with information based on said set of inputs, each template having one or more than one fixed number of entry spaces, the totality of templates in the template set defining a set of behavior types of any such system, each template of said finite template set having a format for accepting a fixed number of said parameters that describe said system attributes, one parameter per entry space, such that each said filled template defines a specific behavioral attribute of a particular system.

A method comprising the steps of:

• retrieving a template from a fixed predetermined library comprising a finite set of templates, each template having one or more than one fixed number of entry spaces, the totality of templates in the library defining a set of behavioral attribute types of any system for which the set of behavioral attribute types can be expressed in terms of a succession of transitions from one model state to a succeeding model state;
• and
• filling said one or more than one fixed number of entry spaces of the retrieved template with at least one expression, one expression per entry space, to form a filled template that defines a specific behavioral attribute of a particular such system, said at least one expression comprising a fulfilling condition which defines at least one event required by said behavioral attribute of said system.