POLYCORE associate team

Polychronous models

International partner

  • Area : North America
  • Country : United States
  • Institution : Fermat Laboratory
  • Laboratory : Virginia Tech
  • Principal investigator : Sandeep Shukla

Presentation of the associate team

Anyone experienced with multi-threaded programming would recognize the difficulty of designing and implementing such software. Resolving concurrency, synchronization, and coordination issues, and tackling the non-determinism germane in multi-threaded software is extremely difficult. Ensuring  correctness  with respect to the specification and deterministic behavior  is necessary for safe execution of such code. It is therefore desirable to synthesize  multi-threaded code from formal specifications using a provably `correct-by-construction' approach.  In Europe, it has been widely claimed that the embedded software for 'fly-by-wire' was mostly automatically generated using French tools based on the synchronous programming models. Unfortunately, software generated in those contexts usually operate in a  time-triggered execution model. Such models are simpler but less efficient than multi-threaded software on multi-core processors. Normally they run on multiple processors communicating over a time-triggered bus. Hence the execution is less  efficient than it could be.  While time-triggered programming model simplifies code generation, we feel that multi-rate event driven execution model is much more efficient.  Code synthesis  for such execution model must be thoroughly investigated.  The multi-threaded software generation is  inspired by a recent shift in the hardware design paradigms from single-core to multi-core processors. This shift has brought parallel and concurrent programming to the desktop and embedded arena. In the desktop market, most processors now being sold are multi-core, and very soon this trend might  conquer the embedded world as well. We plan to develop formal models, methods, algorithms and techniques for generating provably correct multi-threaded reactive real-time embedded software for mission-critical applications. For scalable modeling of larger embedded software systems,  the specification formalism has to be  compositional and hierarchical. Our proposed formalism entails a model of computation (MoC) based  on a multi-rate synchronous data-flow paradigm: Polychrony.

Keywords: Associate teams INRIA Rennes - Bretagne Atlantique North America United States

Inria research teams of the same theme

Inria Headquarters and research centres

Direct links

Social