HLL – 高级语言

HLL 是一种声明式、基于流的语言，具有大量的类型和运算符。它适用于对离散时间序列行为进行建模，并表达这些行为的时间特性。

HLL可以帮您实现：

• 模型软件作为形式化验证或仿真的数学模型，
• 为软件环境建模，以研究软件在其中的行为，以及
• 形式化表达安全要求和引理。

HLL 是一种为工业系统的形式化验证量身定制的形式化高级语言。您可以自动将计算机程序或中继系统转换为 HLL，以便在数学上研究它们，并使用模型检查器（如 PSL）证明有关它们的属性。常见用例是证明安全属性、不变性检查、顺序等价性检查、测试用例生成和静态代码分析，例如没有溢出和除以零。您还可以使用 Prover 认证器创建符合 CENELEC EN50128 SIL4 标准的安全证据。

数独问题对于现代证明引擎（例如 SAT 求解器）来说是一个非常简单的问题，但它可以很好地帮助我们向读者介绍 HLL。可以肯定的是，我们只能说明 HLL 的一个相对较小的子集，HLL 是一种多年来发展相当多的语言。为了形式化和解决数独问题，我们主要需要整数、数组和量词。

2008 年，Prover 和 RATP 之间的合作促成了 HLL 语言第一个版本的发布，它是 Prover 语言 Tecla 的继任者。 HLL 的主要目标是添加必要的功能，以实现 CBTC 系统（基于通信的列车自动控制系统）的形式化验证。

HLL 起源于 Prover开发的证明引擎技术，它由Prover不断发展演进，从 1980 年代的Stålmarck 方法，到1990 年代的时间归纳，再到 21世纪初期更高层次的理论。

HLL 是我们的工具 Prover的输入语言。您可以使用 Prover 认证器获取系统的安全证据，这一过程包括通过将您的系统转换为 HLL ，并在 HLL 中定义您的安全要求。形式化验证可确保您的系统在 100% 的可能场景中满足要求，这是一般测试永远无法实现的覆盖范围。

自 2008 年以来，我们的许多客户已使用 HLL 获得了 CENELEC EN50128 SIL4 级别的形式化安全证明。

HLL 的成功也许要归功于它的易用性（灵活和直观），能处理大型工业系统的形式化验证工具的支持，以及提供可认证的结果。

HLL 2.7 版本于 2018 年发布。 HLL 不断改进和扩展，以支持更多种类的系统，让表达更多种类的属性成为可能。已发布的版本不再用于最先进的形式化验证项目。更新版本最终将在 HLL 论坛倡议下发布。

HLL 不断改进和扩展，以支持更多种类的系统，使表达更多种类的属性成为可能。 Prover 始终关注 HLL 的向向下兼容。 我们可以自豪地表示，我们的新工具经过新的改进，仍然能够处理旧系统。

为了确保 HLL 语言的发展并避免分叉成方言，我们成立了 HLL 论坛。 这是一个工作小组，邀请工具供应商和用户讨论 HLL 的新功能。 我们都同意 HLL 是一种很棒的语言，它需要以可控的方式进行开发以满足未来的需求。