HLL – High Level Language
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.
With HLL you can:
- model software as a mathematical model for formal verification or simulation,
- model a software environment to investigate how the software behaves in it, and
- formally express safety requirements and lemmas.
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 absense 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 be 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.
|1. Mailot-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|
|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 several of our clients 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.
Version 2.7 of HLL was published in 2018. HLL is continuously improved and extended to support more kinds of systems and to make it possible to express more kinds of properties. The published version is not the one used anymore in state-of-the-art formal verification projects. An updated version will eventually be published under 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
- Vendor-specific programming languages
- Relay schematics
Projects using HLL over the world
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 are invited to 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.