Formal languages

Prover provides three different languages that are used to create and represent formal requirement specifications and configuration data: PiSPEC, HLL and LCF. PiSPEC is the language used for Generic Applications (for design, test and safety requirements) in the Prover Trident process and the Prover iLock tool, HLL is a more general-purpose modelling and verification language and is the input language of PSL and Prover Certifier, while LCF is used for configuration data.

In addition to having a precisely defined syntax and semantics, these languages have been carefully designed to make it easy to express signalling requirements and configuration data, but also to simplify manual review tasks. The latter is particularly important for the LCF language, as review of configuration data, especially safety critical data, is an important and common task in many rail control projects. LCF data can be imported and exported by Prover iLock and translated into HLL for use in CENELEC EN50128 compliant verification processes.