APPARATUS FOR DEFINING PROPERTIES IN FINITE-STATE MACHINES

摘要

A method and apparatus for defining a system design specification by using a finite set of templates that have a format for accepting a set of system express ion such that a selected template, when filled with the system expressions, defines an ex pected behavioral attribute of the system. In one illustrative embodiment, each templat e has a set of qualifiers and a set of entry blanks, wherein each qualifier is associate d with a entry blank. In such an embodiment, the set of entry spaces may comprise a fulfi lling condition entry space for accepting a system expression that defines a required or assumed event of the system model, an enabling condition entry space for accepti ng a system expression that defines a precondition for starting a check of the requir ed or assumed event, and a discharging condition entry space for accepting a system expression that defines a condition after which said fulfilling condition is no longer required or assumed by the system model. Filling the entry spaces of a selected template with the appropriate system expression can form an expression that defi nes an expected behavior of the system model. Thus, a set of filled templates can defin e a set of expected behaviors of the system model (i.e. a system design specification). The system design specification can then be used to generate computer-executable cod e (e.g. automata) for testing the expected behavioral attributes of the system. For exam ple, each filled template of the system design specification can be converted to an a utomaton by a given subroutine.