HLL, a modeling language

Targeted Modelings

HLL (High Level Language) is a language used to describe discrete-time systems models.

It has been designed to formally express both the model of a system, operational environment constraints, and safety properties on this system.

As of today, its main industrial usage is for the independent formal safety analysis of critical systems and software (safety case, expert safety assessment, …).

However it can also be used for advanced problem resolution such as constraint satisfactions, combinational optimization, or automatic test case generation.

A mature industrial technology

The railway industry is the main driver of this technology, using it in full-scale operational projects since many years:

HLL

HLL in a few words

HLL is a formal modeling language.

The basic element of the language are streams, typed variables having values at each time-cycle. The input streams take any value of their (bounded) range at a given cycle, and the various defined streams are then evaluated in the dataflow order using the values of these inputs at this cycle, and the values of the memory streams at the previous cycle. This evaluation is performed up to the valuation of the output streams.

HLL is thus a synchronous dataflow language with formally defined syntax and semantic. Targeted for the Model Checking of safety critical systems, this language has been designed to be:

  • rich and expressive to ease the development of automatic
    translators of a system or software to its model
  • simple, clear, efficient, and non-ambiguous to enable both:
    • the formalization of the safety properties that the system
      shall respect
    • the formalization of the operational constraints assumed on
      the environment of the system
    • the independent reviews performed on the properties and
      constraints
  • declarative and structured to enable the separation of the
    generic core, from the instantiation of this core on a specific
    track layout giving rise to efficient and certifiable automatic
    safety verification solutions.

Technological maturity

As seen from its industrial references, the language and technology exist since ten years.

This long track of successes in the use of Model Checking for the safety verification of critical systems has always been driven by the evolution of the language and solution to improve:

  • the costs and time for the development of specialized translators
  • the ease of modeling of the safety properties and environment constraints
  • the analysis power of the safety verification solutions

These improvements enable the users to easily integrate these solutions in their development processes despite the evermore constrained time-to-market schedules.

Systerel and HLL

Time for choice

The use of formal methods for the development and validation of critical system is part of the DNA of Systerel.

To answer the increasing demands of its customers to strengthen the safety verification of their critical systems by the use of Model Checking, Systerel has developed its own formal verification solution: Systerel Smart Solver (S3), started in 2013.

The creation of such a solution implies the choice of a modeling language. Thanks to its unique characteristics, HLL has been a highly priced candidate, and has thus been chosen as the S3 modeling language.

Systerel, a major player in the HLL technology

Systerel has now been using HLL for many years in the formal safety verification of critical systems such as CBTCs, interlockings, logical control-command circuits, but also for the optimization of constrained systems.

In the framework of a continuous improvement process, Systerel is now a main actor in this technology’s evolution. In particular, we have worked on:

  • the evolution of the latest version of the HLL language
    • expressiveness of the language
    • increase in the genericity
    • checking of the correctness of models
  • the development and improvement of specialized translators
  • the development of an IEEE-compliant library for the handling of
    floating points
  • the improvement and industrialization of analysis tools
    • usability of counter-example exploration tools
    • relevancy of counter-examples with respect to the user domain
    • analysis performance
  • the use of the technology for innovative applications

Systerel tools around HLL

Systerel has a complete offering of tools around HLL and SAT-based Model Checking technology. These high-performance tools are designed both to work at the HLL level, but also to translate normalized languages such as SCADE, C’99 or Ada to HLL.

The tools are also certifiable to bring the justification and qualification artifacts to an overall solution safety-case.

The Systerel Smart Solver offering

Systerel offers a range of industrially proven solutions built upon its Systerel Smart Solver product:

  • Term-Based Licenses
  • Tool-Based Services
    • safety proofs
    • resolution/optimization of constrained systems
  • Design and development of personalized solutions
  • Training

They trust us

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

As well as other major players in the aeronautics industry.

Bibliographical references

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

Contact us Learn more about Systerel Smart Solver