HLL formal language celebrates 10 years

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 10th anniversary of its conception.

The history of HLL

The language has its roots in the proof engine technologies developed by Prover in the 1980s (Stålmarck’s method), 1990s (temporal induction) and early 2000s (higher level theories) and its development was prompted by a need for trusted (or certifiable) formal verification.

HLL is a declarative language with a broad panel of types and operators and is suitable for modelling discrete-time sequential behaviors and expressing properties of these behaviors.

Or to put it differently: if you have a reactive system (such as an interlocking or a CBTC subsystem) with some inputs, outputs and internal state (memory), and you want to formally prove that some present or future conditions on the outputs shall follow from some past or present conditions on the inputs, then HLL may be the right language for you. The language, with its associated tools, can be used for applications such as invariant checking, sequential equivalence checking, test case generation or static code analysis (detection of runtime errors such as overflows or divisions by zero).

Version 1.0 of HLL was released in 2008 and the language is being continually developed. The latest version includes, in addition to the basic core of Boolean logic and integer arithmetic, features such as enums, arrays, tuples, structs, recursive functions, quantifiers, polymorphism, namespaces and blocks. The imperative dialect of HLL also supports statements such as assignments, if-then-else, loops and procedures.

The HLL formal language success

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 both scale up in practice for a wide variety of systems, and provide certifiable results based on diversification and proof logging/checking.

Find out more about HLL here.
You can also check out our HLL Forum – The community for those who use HLL