Architecture and functionality of a specification environment for distributed software

A description is given of Graspin, a workstation-based prototype environment that aids in the incremental construction, verification, and prototyping of specifications for concurrent and distributed software systems. It includes a Petri net-based specification formalism, an editor generator with graphical capabilities, and tools for static semantics checking, automated verification of static and dynamic properties of specifications, and specification-based prototyping. The Graspin architecture and kernel environment have shown their flexibility in the development of a prototype environment supporting the formal specification language SEGRAS. It was necessary to extend the kernel by semantic tools such as type checker and net simulator and to integrate separately developed tools such as the rewrite rule subsystem into a coherent environment. New Graspin features include a graphical refinement method and a multi-level net animation technique