Software
The Vertics team develops two main software tools: Tina, a toolbox for the analysis of Time Petri Nets, and Frac, the Fiacre compiler.
Tina
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 modelcheckers 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.
FIACRE
FIACRE is an Intermediate Formal language
for the description of concurrent activities with realtime constraints. It is
a formally defined language for representing compositionaly both the behavioural
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 realtime
verification patterns, that is
a possibility to define timed temporal properties directly within a
specification.
Miscellaneous
We also distribute several prototypes:

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.

SMPT (Satisfiability Modulo Petri Net): is an SMTbased modelchecker for checking reachability properties on generalized Petri nets.

Kong (Koncurrent places Grinder): is a tool to accelerate the computation of concurrent places in Petri nets using structural reductions.

MCC: a tool to unfold highlevel (colored) Petri Nets that can be applied on models used in the ModelChecking Contest.

Ramona: a tool for analyzing realtime 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.

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

Fiacre Simulator: an Eclipse plugin providing support for editing, syntaxhighlighting, debugging and simulation of Fiacre programs.

SimSo (Simulation of Multiprocessor Scheduling with Overheads): is a scheduling simulator for realtime multiprocessor architectures that takes into account some scheduling overheads (scheduling decisions, context switches) and the impact of caches through statistical models. The easiest way to evaluate the simulator is to use SimSo Web, a full browser interface of SimSo.

Tina2IPN: a singlepage application that generates an Interpreted Petri net file (rdp) from a net file and a table associating labels with actions.