HLL – High Level Language2019-07-11T09:07:12+01:00

HLL – High Level Language

A Language for Formal Verification of Safety-Critical Systems

About 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, 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.

Read full article here

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.

Interlocking

Line/system Year Usage
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

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 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
    • SCADE
    • ADA
    • C
  • Vendor-specific programming languages
    • Microlok
    • Westrace
    • iVPI
    • etc
  • Relay schematics

Projects using HLL over the world

Future

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. 

MORE ABOUT HLL

Using HLL to solve Sudoku puzzles

By |July 10th, 2019|

In a recent post we celebrated the 10th anniversary of the declarative, formal language HLL. The language is used extensively in the railway signaling domain for the formal verification of interlocking [...]

A new version of HLL emerging

By |April 10th, 2019|

The HLL Forum meeting we had in December decided to let a subgroup work on a new language definition meeting emerging needs in the market. Some of us in this [...]

HLL formal language celebrates 10 years

By |June 30th, 2018|

The formal language HLL (High Level Language) has emerged in recent years as a quite popular language for formal verification of safety-critical systems, especially in the railway signaling domain. This year marks the [...]