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 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/
Nicolas Breton and Yoann Fonteneau. S3: proving the safety of critical systems. In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification – First International Conference, RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings, 231–242. 2016. URL : https://link.springer.com/chapter/10.1007%2F978-3-319-33951-1_17
Ning Ge, Arnaud Dieumegard, Eric Jenn, and Laurent Voisin. From event-b to verified c via hll. URL : https://hal.archives-ouvertes.fr/hal-01387137
Ning Ge, Eric Jenn, Nicolas Breton, and Yoann Fonteneau. Formal verification of a rover anti-collision system. In Critical Systems: Formal Methods and Automated Verification – Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2016, Pisa, Italy, September 26-28, 2016, Proceedings, 171–188. 2016. URL : https://link.springer.com/chapter/10.1007%2F978-3-319-45943-1_12
Marielle Petit-Doche, Nicolas Breton, Roméo Courbis, Yoann Fonteneau, and Matthias Güdemann. Formal verification of industrial critical software. In Formal Methods for Industrial Critical Systems – 20th International Workshop, FMICS 2015, Oslo, Norway, June 22-23, 2015 Proceedings, 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