Abstract:
A visual environment for specifying graphical user interfaces has been developed. The PUIST (Petri net based graphical User Interface Specification Tool) environment integrates formal specification, prototyping and formal analysis. The PUIST model permits an EPT net (PUIST Extended Place/Transition) node to be associated with a GUI object. The GUI object semantics are mapped to EPT net semantics. This permits the EPT nets specification and the prototypes of the GUI under the specification to be created concurrently. Nets and interfaces can be tested concurrently at any stage of the specification. The PUIST subnet type formalism provides a novel and useful form of parametric abstraction permitting straightforward reuse of specifications. The visual formalism allows both hierarchical and recursive composition of GUI components to be specified. While the language has a simple notation, it is capable of defining complex EPT nets. It is particularly good for EPT nets with complex and repeated pattern structures, where abstractions can be applied. Reachability trees, a method of Petri net analysis, are used to evaluate designs in PUIST. A modification to Peterson's reachability tree algorithm (Peterson,81) is given and implemented in PUIST. The modified algorithm preserves more firing sequence information of a net than Peterson's algorithm. The correctness of the modification is proved. The modified algorithm takes the three special components (emptying arcs, autofiring transitions, and inhibitor arcs) into consideration and the correctness of the extension is proved. From the reachability tree of a net given by the modified algorithm, the following Petri net properties of the net can be tested: boundedness, liveness (including deadlock detection), reversibility and controllability.