PARAGON: A Tool for Visual Specification and Verification of Real-Time Systems
PARAGON is the following acronym:
Process-Algebraic
Analysis of
Real-time
Applications with
Graphics-
Oriented
Notation
PARAGON provides a visual design environment for distributed real-time systems.
The toolset contains:
- A graphical editor for the
GCSR
specification language.
- A visual simulator for GCSR specifications (under construction).
- XVERSA, a graphical user interface to
VERSA,
a verification tool for
ACSR
specifications.
- Translators between GCSR and ACSR.
The GCSR language consists of a set of primitives that allow one to
capture in an intuivite way both behavioral and structural aspects of
a design.
PARAGON is implemented in C++ and X/Motif, with the help of Lex and Yacc
compiler construction tools and the LEDA class library
to enhance portability. All major components: editor, simulator and the
analysis toolkit are implemented as separate UNIX processes and can be used as
stand-alone tools. The use of a low-level programming language and the
most current algorithms state machine construction and bisimulation testing
has resulted in performance that compares very favorably with existing
process algebra analysis toolkits.
PARAGON Extensions
Several formalisms and analysis tools are not part of PARAGON, but are designed
to interoperate with paragon tools, or use compatible languages and share
"look-and-feel." These tools and formalisms include
- PACSR (Probabilistic ACSR), a formalism that
associates a probability of failure with every resource.
-
LCSR tool is a model checker based on a graphical
version of modal mu-calculus extended with resource modalities. LCSR
uses ACSR specifications as input and can be used as an alternative
back-end verification tool for PARAGON.
Obtaining PARAGON
PARAGON is not yet available for public release. The code is maintained and
supported by