HLL, un langage de modélisation

Les modélisations visées

HLL (High Level Language) est un langage permettant de décrire des modèles de systèmes à temps discret.

Il a été conçu pour exprimer des propriétés de sécurité sur ce type de système.

Son cas d’emploi industriel le plus large à ce jour concerne les analyses formelles de second regard sur des systèmes ou logiciels (dossiers de sécurité, avis d’expert).

Mais les usages peuvent aller plus loin : résolutions de contraintes, génération automatique de cas de tests…

Une technologie de niveau industriel

L’industrie ferroviaire est un moteur de cette technologie et en a fait un usage au-delà de la R&D depuis plusieurs années :

HLL

HLL en quelques mots

HLL est un langage formel de modélisation.

L’élément de base du langage est le stream, une variable typée ayant une valeur à chaque cycle. Les streams d’entrée prennent une valeur au début d’un cycle, puis les différents streams sont évalués dans l’ordre du flot de données (dataflow) à partir des valeurs des inputs et de celles des mémoires au cycle précédent (variables d’état du système), jusqu’à la production des outputs.

C’est donc un langage synchrone et à flot de données (dataflow).

Ce langage possède une syntaxe et une sémantique bien définies.

Ce langage destiné au model checking a été conçu pour être :

  • simple et clair afin d’être efficace et non ambigü lors des activités de :
    • formalisation des propriétés et du modèle d’environnement contraignant l’espace d’état sur lequel faire la preuve,
    • revues de ces propriétés et contraintes,
  • riche et expressif pour simplifier le développement de traducteurs permettant d’obtenir automatiquement le modèle d’un système critique à partir de son code,
  • déclaratif et structuré ce qui le rend extrêmement pratique et puissant pour séparer un cœur générique et son instanciation et ainsi construire des solutions automatiques performantes et certifiables.

Maturité technologique

Comme illustré par les références industrielles citées plus haut, le langage et la technologie existent depuis une dizaine d’années.

Cette antériorité donne à HLL les moyens d’évoluer pour continuer d’améliorer :

  • les coûts et délais de développement de traducteurs spécifiques
  • les efforts de modélisation des propriétés / environnement
  • les performances d’analyse afin de permettre aux utilisateurs d’intégrer ces solutions dans des délais de projets industriels toujours plus contraints.

Systerel et le HLL

L’heure du choix

L’utilisation des méthodes formelles dans le développement et la validation des systèmes critiques fait partie de l’ADN de Systerel.

Pour répondre aux demandes croissantes de ses clients d’appuyer la vérification de la sécurité de leurs systèmes sur l’utilisation de méthodes de “Model Checking”, Systerel a développé sa propre solution de vérification formelle : Systerel Smart Solver (S3) est ainsi né en 2013.

La création d’une solution de vérification impose le choix d’un langage de modélisation. Les caractéristiques précédemment exposées de HLL en faisait un candidat de choix :

  • simple et clair pour formaliser les propriétés de sécurité que l’on cherche à prouver,
  • riche et expressif pour simplifier le développement de traducteurs,
  • disposant d’une syntaxe et d’une sémantique bien définies.

C’est ainsi que tout naturellement HLL a été retenu en tant que langage de modélisation de S3.

Systerel, acteur majeur de la technologie HLL

Systerel utilise le langage HLL depuis de nombreuses années maintenant dans le cadre de vérifications formelles de logiciels ou systèmes critiques comme des CBTC, des postes de signalisation mais également des circuits logiques de contrôle-commande et autres usages nécessitant l’expression de contraintes à vérifier.

Dans le cadre d’un processus d’amélioration continue, Systerel est ainsi devenue un acteur majeur dans l’évolution de la technologie.

Elle a conduit :

  • des travaux sur les dernières évolutions du langage HLL
    • expressivité des propriétés
    • amélioration de la généricité
    • bonne définition des modèles
  • des travaux à la périphérie du langage
    • traducteurs
    • bibliothèques (e.g. pour une prise en compte plus performante des flottants)
  • des améliorations et industrialisation des moyens de la preuve
    • ergonomie des moyens d’analyse de contre-exemples
    • pertinence métier des contre-exemples
    • performance d’analyse
  • des travaux d’études de nouveaux cas d’emplois

Les outils Systerel autour de la technologie HLL

Systerel propose une palette d’outils autour de la technologie HLL basée sur une approche SAT.

Cette gamme d’outils performants est conçue pour permettre de travailler au niveau HLL mais aussi de traduire des langages normalisés tels que SCADE, C’99, Ada vers HLL.

Elle est également certifiable pour amener les éléments de justification et de qualification à un dossier de sécurité.

L’offre Systerel Smart Solver

Systerel propose une gamme de solutions éprouvées industriellement s’appuyant sur la technologie de son produit Systerel Smart Solver :

  • Location annuelle de licence
  • Services outillés
    • preuve
    • résolution / optimisation de contraintes
  • Etude et développement de solutions personnalisées
  • Formation

Ils nous font confiance :

  • HITACHI
  • ALSTOM
  • General Electric
  • ONERA
  • RATP
  • SNCF

Ainsi que d’autres acteurs majeurs de l’aéronautique.

Références bibliographiques

Julien Ordioni, Nicolas Breton, Jean-Louis Colaço. HLL v.2.7 Modelling Language Specification. STF-16-01805, RATP. 2018. <hal-01799749> URL : https://hal.archives-ouvertes.fr/view/index/docid/1799749/lang/fr/

Nico­las Bre­ton and Yoann Fonte­neau. S3: prov­ing the safe­­ty of crit­i­­cal sys­tem­s. In Re­li­a­bil­i­ty, Safe­ty, and Se­cu­ri­ty of Rail­way Sys­tem­s. Mod­elling, Anal­y­sis, Ver­i­fi­ca­tion, and Cer­ti­fi­ca­tion – First In­ter­na­tion­al Con­fer­ence, RSS­Rail 2016, Paris, France, June 28-30, 2016, Pro­ceed­ings, 231–242. 2016. URL : https://link.springer.com/chapter/10.1007%2F978-3-319-33951-1_17

Ning Ge, Ar­naud Dieumegard, Er­ic Jen­n, and Lau­rent Voisin. From even­t-b to ver­i­fied c via hll. URL : https://hal.archives-ouvertes.fr/hal-01387137

Ning Ge, Er­ic Jen­n, Nico­las Bre­ton, and Yoann Fonte­neau. For­mal ver­i­fi­ca­tion of a rover an­ti-­col­li­sion sys­tem. In Crit­i­cal Sys­tem­s: For­mal Meth­ods and Au­to­mat­ed Ver­i­fi­ca­tion – Joint 21st In­ter­na­tion­al Work­shop on For­mal Meth­ods for In­dus­tri­al Crit­i­cal Sys­tems and 16th In­ter­na­tion­al Work­shop on Au­to­mat­ed Ver­i­fi­ca­tion of Crit­i­cal Sys­tem­s, FMIC­S-AV­oCS 2016, Pisa, Italy, Sep­tem­ber 26-28, 2016, Pro­ceed­ings, 171–188. 2016. URL : https://link.springer.com/chapter/10.1007%2F978-3-319-45943-1_12

Marielle Pe­tit-Doche, Nico­las Bre­­ton, Roméo Cour­bis, Yoann Fonte­neau, and Matthias Güde­­man­n. For­mal ver­i­fi­ca­tion of in­dus­tri­al crit­i­cal soft­ware. In For­mal Meth­ods for In­dus­tri­al Crit­i­cal Sys­tems – 20th In­ter­na­tion­al Work­shop, FMICS 2015, Oslo, Nor­way, June 22-23, 2015 Pro­ceed­ings, 1–11. 2015. URL : https://link.springer.com/chapter/10.1007%2F978-3-319-19458-5_1

Contactez-nous En savoir plus sur Systerel Smart Solver