- Verify the semantic consistency of systems described using safe subsets of heterogeneous modeling languages, ranging from behavioural to architectural languages and presenting a synchronous and asynchronous semantics (Simulink/Matlab, Scicos, Xcos, SysML, MARTE, UML).
- Generate optimized source code for multiple programming (Ada, C/C++) and syntesis (VHDL, SystemC) languages.
- Support a multi-domain (avionics, space, and automotive) certification process by providing open qualification material.
The following presentations summarizes the main goals and results of Project P. It was first presented in June 16th, 2015, during the final Project P Open Workshop.
The intermediate metamodel at the heart of the P Toolset - the P formalism - is available under an Apache license here.
Down below, you can find some videos showing the main products and technologies developed during Project P.
Code generation from Simulink models (AdaCore)
In this video, we show how to use QGen to generate code from Simulink models using different code generation strategies.
Real-time schedulability analysis and distributed code generation with SynDEx (Inria)
In this video, we show how to use QGen and SynDEx to perform real-time schedulability analysis and generate a self-contained distributed kernel for a specific application.
Code generation from XCos models (Scilab Enterprises)
In this video, we show how to use QGen to generate code from XCos models.
VHDL generation (LabSticc)
In this video, we show how to use QGen to generate VHDL code.
Code generation from Scicos Pro (Altair / ENPC)
In this video, we show how to use QGen to generate code from Scicos Pro models.
Bug finding in Simulink models (AdaCore)
In this video, we show how to use QGen to look for bugs, in particular potential divisions by zero, in Simulink models.
Redundant modeling elements in Simulink models (AdaCore)
In this video, we show how to use QGen to detect redundant modeling elements, i.e. redundant calculations that are "hidden" by other calculations.
Formal Verification of Simulink models (AdaCore)
In this video, we show how to use QGen to formally prove properties on Simulink models using Simulink assertion blocks.