From September 2014 to December 2016, the INGEQUIP project was conducted at the IRT Saint Exupéry in Toulouse thanks to the contribution of six industrial companies, five technology providers, and four academic institutions. The common objective was to propose and exploit innovative technologies for the design, the verification, and the validation of aeronautical, automotive, and space equipments.
During this period, a team composed of engineers, post-doctoral researchers, and trainees, selected, analysed, experimented, and evaluated various virtual prototyping environments, modelling formalisms, and formal verification methods and tools.
INGEQUIP Project team wrote a book presenting some of the results of this work. It gives an overview of the methods and tools studied during the project. It shows how they have been applied on small – but representative – examples, and illustrates how they could be implemented on actual industrial projects.
To get more information about INGEQUIP Book, contacts us
Methods and tools for collaborative system engineering (system-hardware-software co-design, component-based development methods, formal verification methods).
Zoom on formal verification methods and tools
A process combining formal refinement and formal software verification using Event-B, S3 and Frama-C technologies has been devised to ensure formal verification from system level requirements up to source code through high and low-level requirements.
Taking into account certification recommendations, this process was tested on the automatic rover protection function of the Twirtee demonstrator (Three Wheeled Integrated Rover Test bench for Engineering Evaluation).
Zoom on virtual prototyping environments and modelling formalisms
A co-development approach including system, electronic and software engineering has been created. The approach ensures the continuity and consistency of all artefacts across the complete chain of engineering activities. It is based on industrial standards such as Capella for system activities, AADL for software refinement and IP-XACT for hardware description. The continuity of the design and verification flow is ensured through model transformations that fill any gaps between the different modelling environments.
Virtual platform technologies like those developed by IRT partners Space Codesign and ASTC Design Partners are compatible with the proposed approach. The scalability of the whole development chain has been demonstrated on the Twirtee demonstrator, a smart rover whose HW-SW architecture is representative of avionics-like systems. This methodology has been awarded at the ERTS2 International Conference
G. Bois, F. Montero, E. Jenn and K. Duplantier:“Architectural Exploration and Implementation of an Image Processing Chain with SpaceStudio”.FPL 2016 (26th International Conference on Field-Programmable Logic and Applications), Lausanne (Switzerland). 2016
M. Clabaut, N. Ge and N. Breton:“Industrial Grade Model Checking: Use Cases, Constraints, Tools and Applications”.ERTS2 2016 (Embedded Real Time Software and Systems), Toulouse, France. 2016
P. Cuenot, E. Jenn, E. Faure, N. Broueilh and E. Rouland:“An Experiment on Exploiting Virtual Platforms for the Development of Embedded Equipments”.ERTS2 2016 (Embedded Real Time Software and Systems), Toulouse (France). 2016
N. Ge, E. Jenn, N. Breton and Y. Fontenneau:“Formal Verification of a Rover Anti-collision System”.FMICS-AVoCS 2016 (International Workshop on Formal Methods for Industrial Critical Systems and Automated Verification of Critical Systems), Pisa (Italy). 2016
B. Ouni, P. Gaufillet, E. Jenn and J. Hugues:“Model Driven Engineering with Capella and AADL”.ERTS2 2016 (Embedded Real Time Software and Systems), Toulouse (France). 2016
E. Jenn:“The INGEQUIP Project and the TwIRTee demonstrator”.Convecs, Charavines (France). 2015
P.-A. Bourdil, E. Jenn and S. Dal Zilio: “Building Confidence on Formal Verification Models”. SafeComp 2016 ( International conference on Computer Safety, Reliability and security), Trondheim (Norway). 2016B. Ouni, P. Gaufillet and P. Cuenot:“TwIRTee design exploration with Capella and IP-XACT”.DVCon Europe (Design and Verification Conference Exhibition), Munich (Germany). 2016