A diagram of the tool chain for code generation is shown in the figure above. The top-part represents a high-level design, serving as input to the tool chain. Currently we support high level designs from the DOL Critical framework. The framework should provide the model of the application (task graph) and the model of deployment (mapping). The application model includes both the task communication structure (here: the DOL-Cr XML) and the task functions (here: the C files). The mapping file (...)
The BIP compiler and execution engines for simulation, execution, exploration and debug of BIP models.
A statistical model checking engine prototype for the BIP framework.
D-Finder tool implements a compositional and incremental method for the verification of component-based systems described in BIP language encompassing multi-party interaction.
For deadlock detection, D-Finder applies proof strategies to eliminate potential deadlocks by computing increasingly stronger invariants.
Finally, the use of abstraction in invariant computation may introduce false positives. D-Finder proposes a refinement procedure to remove those cases for BIP programs with Boolean variables.
FLATA is a tool for the analysis of non-deterministic linear integer programs (also known as counter automata).
FLATA-C is static-analysis front-end, implemented as a FRAMA-C plugin, that aims at extracting Numerical Transition System models from C programs with low-level pointer updates such as e.g.: allocation, deletion, pointer arithmetic, etc. The generated NTS models can be used with off-the-shelf verifiers such as FLATA or ELDARICA. We target the following types of errors in the C code: null or dangling pointer dereferencing unaligned memory accesses memory leaks double free out-of-bound (...)
InVeSt is a tool for verification of invariance properties of infinite state systems.
Lists to Counter Automata: a tool for the analysis of pointer programs
RTD-Finder tool implements a compositional method for the verification of component-based Real-time systems modeled in RT-BIP language. RTD-Finder verifies safety properties.
The Symbolic Model Interface (SMI) is a library which provides for the efficient construction and manipulation of symbolic representations for finite state systems, in particular for communication protocols.