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

Documents et médias

Télécharger le support

pdf (1.61 Mo)

Résumé

Les langages synchrones rencontrent un succès important dans la programmation de systèmes embarqués tels que les avions, les trains ou les centrales électriques (voir les cours de Gérard Berry en 2013 et 2014). Le temps y est vu de manière logique comme la suite de réactions instantanées du système aux entrées d'un environnement extérieur. Cette abstraction discrète permet d'écrire des programmes dans un langage mathématique, de garantir statiquement leur déterminisme et de les compiler vers du code s'exécutant en mémoire et temps bornés. La sémantique et la compilation des langages synchrones sont aujourd'hui suffisamment précises et bien comprises pour satisfaire aux exigences imposées par les autorités de certification de l'avionique civile pour le développement des parties les plus critiques (voir le séminaire de Bruno Pagano sur le logiciel SCADE 6 en 2013).

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.