EXSPECT

The EXecutable SPECification Tool is a framework for executable formal specifications of distributed systems based on a functional language.

Environment:

SunOS or SOLARIS on SPARC or Intel x86

Origin:

Bakkenist Management Consultants, Amsterdam, The Netherlands

Kind of Nets supported:

Hierarchical Coloured Petri Nets with time, time delays associated with tokens.
Every token has a value and a time stamp: system time at his production and time delay (determined by the transition) denoting the earliest time it may be consumed.

Functionalities:

Graphical EDITOR and TYPE CHECKER
interactive SIMULATION: interpreter for executing
IAT (Interval Timed Petri Net Analysis Tool): calculates S- and T-Invariants and other structural and timing properties

Availability:

POLICY: single user license
CONTACT Dr. W. Hengeveld

References:

K. M. van Hee, L. J. Somers, M. Voorhoeve: Executable Specifications for Distributed Information Systems [hsv89]
K. M. van Hee, L. J. Somers, M. Voorhoeve: The EXSpect Tool [hsv91]
Tool description at DAIMI