Software

main architect: Bernard Berthomieu

The TINA toolbox is a set of tools for the edition and analysis of time Petri Nets and their extensions. In particular it can handle Time Petri Nets (TPN), priorities, inhibitor arcs, and an extension of TPN with data handling called TTS.

Tina includes an editor and GUI (nd) for Time Petri Nets and Automata; stepper simulators and state space generation tools (tina and sift); structural analysis tools (struct); and model-checkers for state/event LTL (selt), and for CTL* and an existential fragment of μ calculus (muse).

sift is a specialized version of tina supporting in addition on the fly verification of reachability properties. If offers less options than tina but is typically faster and requires considerably less space.

main architect: Bernard Berthomieu

FIACRE is an Intermediate Formal language for the description of concurrent activities with real-time constraints.

It is a formally defined language for representing compositionaly both the behavioral and timing aspects of embedded and distributed systems for formal verification and simulation purposes. We provide a compiler (frac) that is able to generate a TTS model from a given Fiacre specification. This TTS model can then be used with Tina.

We have recently extended the language with: native functions and real-time verification patterns, that is a possibility to define timed temporal properties directly within a specification.

main architect: Silvano Dal Zilio

Twina a tool for analyzing the “product” of two Time Petri Nets (TPN), with possibly inhibitor and read arcs. Its main objective is to compute a usable representation of the intersection of two net languages; meaning the intersection of the (timed) languages obtained from the executions of two TPN, in which transitions with the same labels are fired at the same date

main architect: Silvano Dal Zilio

MCC is a tool to unfold high-level (colored) Petri Nets that can be applied on models used in the Model-Checking Contest.

main architect: Silvano Dal Zilio

Ramona is a tool for analyzing real-time properties of systems of RAte MONotonic tAsks. Its main objective is to check the schedulabity of a set of periodic tasks using some hypothesis on the behavior; more specifically the use of fixed priority scheduling and a Logical Execution Time (LET) model

main architect: Nicolas Amat

SMPT (Satisfiability Modulo Petri Net): is an SMT-based model-checker for checking reachability properties on generalized Petri nets.

main architect: Faiez Zalila

An OSATE compliant Eclipse plugin for generating Fiacre (behavioral) specifications from an AADL model using the Behavioral Annex.

main architect: Silvano Dal Zilio

Tina2IPN is a single-page application that generates an Interpreted Petri net file (rdp) from a net file and a table associating labels with actions.