ONE
ONE (OBJSA Nets Environment) consists of different modules, each one supporting a different step in the incremental development of the net specification.
- Environment:
- Sun4 (DesignML and OBJ3 Interpreter required)
- Origin:
- Dipartimento di Scienze dell'informazione, Università di Milano, Italy
- Kind of Nets supported:
- OBJSA Nets
- Functionalities:
- Modules of the tool:
- ONESyst permits the user to give a top-down specification of a system.
- ONEGen supports the production of executable OBJSA specifications providing a graphical net editor and a support for the development of the algebraic token specifications.
- ONERed supports the NET TRANSFORMATION Red, which transfers the information contained in an OBJSA component (N, SPEC) from the net N to the associated algegraic specificaion SPEC, preserving its semantics.
- ONEComp handles the OBJSA COMPOSITION mechanism.
- ONESim SIMULATES the specification using OBJ equations as rewriting rules.
- ONEUnf realizes the UNFOLDING of an OBJSA net in a 1-safe SA net.
- ONEInv calculates S-/T- INVARIANTS of the unfolding.
- ONEVer generates the CASE GRAPH of the unfolding and supports the user in the verification of properties using the ACTL model checker AMC developed at IEI of Pisa.
- ONEGSPN convertes OBJSA Nets in Generalized Stochastic Petri Nets
- Availability:
-
- References:
-
