HLL – High-Level Language
A Language for Formal Verification of Safety-Critical Systems
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 the absence of overflows and divisions by zero. You can also create CENELEC EN50128 SIL4-compliant safety evidence using Prover Certifier.