HLL, un langage de modélisation

Langage HLL

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

Initialement créé pour exprimer des propriétés de sécurité sur ce type de systèmes, son utilisation s’étend aujourd’hui à des analyses formelles formelles de second regard sur des systèmes ou logiciels

Toutefois, ses usages peuvent aller plus loin : résolutions de contraintes, génération automatique de cas de tests, etc.

Performance industrielle

L’industrie ferroviaire a été le moteur de cette technologie et l’a utilisée au-delà de la R&D depuis plusieurs années :Vérification formelle HLL de systèmes ferroviaires

Les principes du langage HLL

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 formellement définies.

HLL : ses avantages

Ce langage, destiné au Model Checking, a été conçu pour être :

  • simple et clair afin d’être efficace et non ambigu 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
    • revue 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

Le langage et la technologie sont exploités industriellement depuis 2010. Cette antériorité donne à HLL et à Systerel Smart Solver, 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

Systerel, acteur majeur de la technologie HLL

Systerel utilise le langage HLL depuis de nombreuses années 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 contexte 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
  • 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

Systerel Smart Solver : solution de vérification formelle

Systerel Smart Solver : solution de vérification formelle

Systerel intègre les méthodes formelles dans le développement et la validation des systèmes critiques. Face à une demande croissante 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 lancé sa solution, Systerel Smart Solver, en 2013, choisissant naturellement le langage HLL pour la modélisation.

Découvrez dès à présent tous les avantages de notre solution de vérification formelle : Systerel Smart Solver.

Ils ont fait confiance à Systerel

CONACTEZ NOUS En savoir plus sur Systerel Smart Solver

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