Langages pour la programmation des systèmes hybrides temps discret/temps continu

Cependant, le développement d'un système embarqué réel demande aussi de savoir modéliser ces comportements discrets (logiciel, circuit) en interaction avec des modèles des composants physiques (par exemple : hydraulique, électrique, mécanique). D'où le développement indépendant de langages issus de la simulation numérique comme Simulink, LabView ou Modelica, normes industrielles de fait. Parce qu'ils permettent de combiner temps discret et temps continu, ces langages de modélisation de systèmes hybrides sont apparemment  bien plus expressifs que les langages synchrones. Mais, en n y regardant de plus près, on se rend compte que le temps discret n'y est pas un temps logique, indépendant de l'implémentation, mais peut dépendre des instants où le solveur numérique décide de rendre le contrôle. Cette absence de frontière étanche induit des comportements difficilement prévisibles, et rend délicate la définition d'une sémantique de référence nécessaire pour garantir que les simulations et les implémentations sur différentes plateformes sont équivalentes.

Dans cet exposé, nous montrerons comment bâtir un langage de modélisation de systèmes hybrides au-dessus d’un noyau synchrone en lui ajoutant des équations différentielles ordinaires (ODEs). Cette extension est conservatrice vis-à-vis d'un langage synchrone existant (par exemple : SCADE), c'est-à-dire que tout programme synchrone y conserve sa sémantique, sa compilation restant inchangée. Mais la partie discrète synchrone permet aussi de modéliser les transitions entre des modes continus. Nous nous appuyons sur l'analyse non-standard pour donner une sémantique synchrone en présence d'un solveur idéal en se ramenant à un système à temps discret. Cette abstraction nous aide à répondre à des questions clefs : quelle discipline imposer dans la combinaison des composants à temps discret et des composants à temps continu ? Que signifie qu'un programme combinant des signaux mixtes discrets/continus est causal ? Sous quelles conditions peut-on produire du code ordonné statiquement nécessaire pour obtenir du code embarqué et des simulations efficaces ? Comment s'assurer que les signaux donnés au solveur numériques sont continus durant l'intégration ? Notre réponse à ces questions est incarnée dans un langage prototype, appelé Zélus, qui utilise plusieurs systèmes de types dédiés, qui généralise la compilation traçable des langages synchrones et qui interagit avec un solveur numérique efficace.