HLL, a modeling language
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 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
- the formalization of the operational constraints assumed on
the environment of the system
- the independent reviews performed on the properties and
- the formalization of the safety properties that the system
- 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.
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
- 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
They trust us
- General Electric
As well as other major players in the aeronautics industry.
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_1Contact us Learn more about Systerel Smart Solver