TEA

Head of team
Jean-Pierre TALPIN (Chercheur Inria)

Tim, Events and Architectures

An embedded architecture is an artifact of heterogeneous constituents and at the crossing of several design viewpoints: software, embedded in hardware, interfaced with the physical world. Time takes different forms when observed from each of these viewpoints: continuous or discrete, event-based or time-triggered. Unfortunately, modeling and programming formalisms that represent software, hardware and physics significantly alter this perception of time. Moreover, time reasoning in system design is usually isolated to a specific design problem: simulation, profiling, performance, scheduling, parallelization, simulation. The aim of project-team TEA is to define conceptually unifying frameworks for reasoning on the composition and integration of cyber-physical systems. Tea aims at putting such reasoning to practice by revisiting analysis, verification and synthesis issues in real-time system design with soundness and compositionality gained from formalization.

 Research themes

Time in system design

  • Logic and calculi to model time(s) and concurrency
  • Abstractions and refinements to formally relate time domains
  • Verification of timed quantitative properties
  • Conformance checking and synthesis of adapters
  • Logical and quantitative reasoning for analysis and verification
  • Type inference, abstract interpretation, SAT/SMT verification, proof
  • Control and scheduler synthesis, abstract affine scheduling
  • Proof theory, type theory, module systems, contract algebra

Artifacts for system design

  • ADFG: A versatile scheduler analysis and synthesis tool for SDF/CSDF implementing abstraction-refinement: ADFG
  • Polychrony on Polarsys: an Eclipse IWG Polarsys project for polychronous modeling, analysis and code generation
  • Tactics for the Keymaera X prover to automate the proof of contracts for the composition of hybrid system models
Creation date
01/01/2014
Reporting institution
Inria, CNRS
Location
Campus de Beaulieu, RENNES
Activity reports
Attachment Size
tea2019.pdf 432.39 KB
tea2018.pdf 434.61 KB
tea2017.pdf 626.65 KB