Accueil > Archives > DCS (Archive) > Outils > Outils
Outils
- Time-Critical Applications on Multicore Platforms
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 (...)
- BIP Compiler
The BIP compiler and execution engines for simulation, execution, exploration and debug of BIP models.
- BIP-SMC : A Statistical Model Checking Engine for the BIP framework
A statistical model checking engine prototype for the BIP framework.
- DFinder A Compositional Deadlock Detection and Verification Tool for BIP Models
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
FLATA is a tool for the analysis of non-deterministic linear integer programs (also known as counter automata).
- FLATA-C
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 Invariants Verification System
InVeSt is a tool for verification of invariance properties of infinite state systems.
- L2CA a tool for the analysis of pointer programs
Lists to Counter Automata : a tool for the analysis of pointer programs
- RTD-Finder A COMPOSITIONAL VERIFICATION TOOL FOR Real-time BIP MODELS
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.
- SMI Symbolic Model Interface
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.
