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.

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.

  • Formally express safety requirements and lemmas.

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 absense of overflows and divisions by zero.

You can also create CENELEC EN50128 SIL4-complient safety evidence using Prover Certifier.

For privacy reasons YouTube needs your permission to be loaded. For more details, please see our Privacy Policy.
I Accept

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.

Guide digital twins

Learn more about Signaling Design Automation

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.


1.    Maillot-la-Défense – Château de Vincennes2009 – 2010Safety case
12.  Mairie d’lssy – Front-Populaire2011 – 2012Safety case
8.    Créteil Préfecture – Pointe du lac2011Safety case
4.    Mairie de Montrouge2013Safety case


3.          CBTC Zone Ctrl2010Safety case
5 & 9.   CBTC Onboard Ctrl2013Safety assessment
13.        CBTC (GOA2)2014Safety assessment

Want to learn how your project can benefit with Signaling Design Automation?

How HLL is used today

H.LL 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. 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

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.

HLL Forum

Projects use HLL all over the world


Latest news, stories and upcoming events from the railway industry.