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.

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.

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).

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.

There is a proposal for version 4.0 of HLL. A version 4.0 will eventually be published within the HLL Forum initiative.

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.