HLL
HLL – High Level Language
HLL – High Level Language
A Language for Formal Verification of Safety-Critical Systems.
A Language for Formal Verification of Safety-Critical Systems.
What is HLL?
HLL is a declarative, stream-based language with a large panel of types and operators. It is suitable for modelling discrete-time sequential behaviours and expressing temporal properties of these behaviours.
Try HLL and our model checker Prover PSL in our free Prover Station Playground.
There is an online specification. An old version was published on HAL. There is also a proposal for a new version 4.0.
With HLL you can:
HLL enables formal verification of industrial systems
HLL is a formal high level language tailored for formal verification of industrial systems.
You can automatically translate computer programs or relay systems to HLL in order to investigate them mathematically and prove properties about them with a model checker such as PSL. Common use cases are proving safety properties, invariant checking, sequential equivalence checking, test case generation and static code analysis such as absence of overflows and divisions by zero.
You can also create CENELEC EN50128 SIL4-complient safety evidence using Prover Certifier.
Using HLL to solve Sudoku puzzles
The Sudoku problem is a very easy problem for modern proof engines (such as SAT solvers), but it will serve us well in introducing the reader to HLL. To be sure, we will only be able to illustrate a relatively small subset of HLL, a language which has grown quite a bit over the years. To formalize and solve Sudoku problems we will mainly need integers, arrays and quantifiers.
The origin of HLL
In 2008, a collaboration between Prover and RATP resulted in the release of the first version of the language HLL, a successor of Prover’s language Tecla. The main goal of HLL was to add the necessary features to enable formal verification of CBTC systems (Communication-Based Train Control).
HLL has its roots in the proof engine technologies developed by Prover in the 1980’s (Stålmarck’s method), 1990’s (temporal induction) and early 2000’s (higher level theories).
Since the release of version 1.0 in 2008, HLL is being constantly developed. It now includes, in addition to the basic core of Boolean logic and integer arithmetic, features such as enums, arrays, structs, recursive functions, quantifiers, polymorphism, namespaces and blocks. The imperative dialect of HLL (“sHLL”) also supports statements such as assignments, if-then-else, loops and procedures.
The tables below show some examples of how RATP used HLL.
Interlocking
| Line/system | Year | Usage |
|---|---|---|
| 1. Maillot-la-Défense – Château de Vincennes | 2009 – 2010 | Safety case |
| 12. Mairie d’lssy – Front-Populaire | 2011 – 2012 | Safety case |
| 8. Créteil Préfecture – Pointe du lac | 2011 | Safety case |
| 4. Mairie de Montrouge | 2013 | Safety case |
CBTC
| Line/system | Year | Usage |
|---|---|---|
| 3. CBTC Zone Ctrl | 2010 | Safety case |
| 5 & 9. CBTC Onboard Ctrl | 2013 | Safety assessment |
| 13. CBTC (GOA2) | 2014 | Safety assessment |
How HLL is used today
HLL is the input language of our tool Prover Certifier. By translating your system to HLL and defining your safety requirements in HLL, you can use Prover Certifier to get safety evidence for the system. Formal verification ensures that your system fulfills the requirements in 100% of the possible scenarios, a coverage that can never be achieved by testing.
Since 2008, HLL has been used by many of our customers to obtain formal safety proofs on a level of CENELEC EN50128 SIL4.
The success of HLL can possibly be attributed to its ease of use (flexible and intuitive) coupled with the support by formal verification tools that are able to handle large industrial systems, and provide certifiable results.
There is a proposal for version 4.0 of HLL available on HAL. A version 4.0 will eventually be published within the HLL Forum initiative.
Prover uses HLL on a daily basis for:
- Formal Verification of CBTC systems
- Formal Verification of interlocking systems (computer-based and relay-based)
- Formal Verification of equivalence of software source code and binary code
- Expressing safety properties
Prover provides translators to HLL for many different applications:
- General-purpose programming languages
- SCADE
- ADA
- C
- Vendor-specific programming languages
- Microlok
- Westrace
- iVPI
- etc
- Relay schematics
Future
HLL Forum
HLL is continuously improved and extended to support more kinds of systems and to make it possible to express more kinds of properties. Prover always takes care of the backward compatibility of HLL. We can proudly declare that our new tools, with new improvements, are still able to treat old systems.
To ensure a flourishing HLL language and avoid forking into dialects we have formed HLL Forum. It is a working group where tool suppliers and users such as signalling suppliers discuss new features of HLL. We all agree that HLL is a great language and that it needs to develop in a controlled way to meet the demands of the future.
Projects use HLL all over the world
News
Latest news, stories and upcoming events from the railway industry.
In the realm of railway software development, adhering to industrial standards is not just a matter of compliance; it’s a cornerstone of ensuring safe, reliable, and efficient railway systems. The latest milestone along this journey is the introduction of the CENELEC standard EN 50716:2023.
+46 (0)8 617 68 00