Inria
Inria.fr
Inria Channel
Demos showroom
Demo showroom
Astrée: Proof of Absence of Runtime Errors
Astrée is a static analyzer making it possible to prove the absence of runtime errors in embedded critical C programs. This proof is fully automatic and is carried out at the source code level, with regard to the semantics of the language. Astrée has successfully analyzed industrial-size applications in the aerospace field. The Astrée analyzer was designed and developed within the Abstraction team. It is currently distributed by the company Absint Angewandte Informatik.
Keywords:
Demo showroom
Architecture exploration in the aerospace field through synchronous technology
Application for management of energy distribution modes for a satellite in orbit with optimization of its load in survival mode. Performance assessment of embedded systems distributed through synchronous technology.
Keywords:
Demo showroom
The SynDEX tool for optimized distributed implementation of critical embedded applications under real-time constraints
Critical embedded applications are generally modeled and simulated with tools using block diagrams. A presentation will be given on the SynDEx tool, which makes it possible to read such application models, specify constraints and temporal characteristics, specify heterogeneous distributed hardware architectures, then, after automatically performing a real-time schedulability analysis and optimizations, generate correct code through construction for these embedded architectures. A gateway between the Scicos modeling and simulation tool for instrumentation and control systems and the SynDEx tool will also be presented.
Keywords:
Demo showroom
Alt-Ergo, automatic proof for critical code certification Project team
Alt-Ergo is software for automatic theorem proving. It is dedicated to the deductive proof of programs, which reduces the correction of a program in relation to its specification with the validity of a logical formula. In particular, Alt-Ergo is at the end of the chain of proof platforms used in avionics. Depending on the complexity of the analyzed codes, there are thousands of formulas that must be proved. Because it is not possible to produce all of these proofs by hand, the use of a tool like Alt-Ergo is crucial for the scaling of this approach.
Keywords:
Demo showroom
TimeSquare: Functional Specifications based on Logical Time in Model Engineering
TimeSquare is based on the CCSL (Clock Constraint Specification Language) formalism, part of the OMG UML MARTE profile (modeling and analysis of embedded real-time systems). The tool makes it possible to specify logical clocks and associate them with behavioral activations and rates within an embedded system (for example, modeled in UML or SysML). TimeSquare permits the analysis and unification of logical clocks and their heterogeneous times for placement/scheduling of applications on execution platforms.
Keywords:
Demo showroom
A sustainable development process: the ATL experience
Model Driven Engineering involves the definition of software elements with precise models. Model transformation can then automate their exploitation. It is particularly used for software development, reverse engineering, and even as an element of the software system (runtime models). The AtlanMod team is working in collaboration with Obeo on ATL: a model transformation tool.
Keywords:
Innovation - Embedded systems
Cappucino: exploiting ambient intelligence from design to implementation of software
The project shows how online sales software is built, deployed, then run on a phone. The software production line and the execution platform have the distinction of being sensitive to context. In addition, the CAPPUCINO platform is capable of adapting the software on the spot based on changes in the user's environment.
Keywords:
Innovation - Embedded systems
Colivad: modeling and optimization of the logistics chain
The global logistics chain involves the optimization of flows at all stages of the Supplier/Customer chain: production, procurement, storage, distribution. Our team focuses on the optimization methods applied to the logistics chain at both the operational and strategic level. In the COLIVAD project, we have developed an optimization tool for package delivery that takes into account the resources specific to the company and its subcontractors.
Keywords:
Sector contact
Are you an entrepreneur? An industry stakeholder? Do you want to collaborate with one of our research teams? Contact our Technology Transfer Associate for Software Publishing and Embedded Systems.
Thierry Vareine
Tel.: +33 (0)1 39 63 51 77
