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
Reporting institution
Inria, CNRS
Campus de Beaulieu, RENNES
Activity reports
Attachment Size
tea2019.pdf 432.39 KB
tea2018.pdf 434.61 KB
tea2017.pdf 626.65 KB