HLL2021-07-02T10:18:30+01:00

HLL – 高级语言

形式化验证安全性的语言

关于 HLL

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

HLL可以帮您实现:

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

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

使用 HLL 解决数独谜题

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

点击阅读全文

HLL的由来

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

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

自 2008 年发布 1.0 版本以来,HLL 一直在不断发展。除了布尔逻辑和整数算术的基本核心之外,它现在还包括枚举、数组、结构、递归函数、量词、多态性、命名空间和块等特性。 HLL 的命令式方言(“sHLL”)还支持赋值、if-then-else、循环和过程等语句。

下表显示了关于 RATP 如何使用 HLL 的示例。

联锁

线路/系统 使用情况
1.    Maillot-la-Défense – Château de Vincennes 2009 – 2010 安全例证
12.  Mairie d’lssy – Front-Populaire 2011 – 2012 安全例证
8.    Créteil Préfecture – Pointe du lac 2011 安全例证
4.    Mairie de Montrouge 2013 安全例证

CBTC

线路/系统 使用情况
3.          CBTC Zone Ctrl 2010 安全例证
5 & 9.   CBTC Onboard Ctrl 2013 安全评估
13.        CBTC (GOA2) 2014 安全评估

目前HLL如何被使用

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

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

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

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

Prover 每天都将 HLL 用于:

  • CBTC系统的形式化验证
  • 联锁系统的形式化验证(基于计算机和基于继电器)
  • 软件源代码和二进制代码等价的形式化验证
  • 表达安全特性

Prover 为许多不同的应用程序提供了 HLL 的翻译器:

通用编程语言

  • SCADE
  • ADA
  • C

供应商特定的编程语言

  • Microlok
  • Westrace
  • iVPI
  • 等等

继电器原理图

世界各地使用 HLL 的项目

未来

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

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

更多关于HLL的内容

为什么进行形式验证-验证问题的解决方案

By |四月 14th, 2020|

如果您已经阅读了本系列的前两部分,那么您将知道,验证联锁满足安全要求并不是一件容易的事。由于联锁的状态空间很大,因此手动方法和测试都无法助您一臂之力。

形式化验证Why系列之一:铁路系统的安全需求

By |三月 31st, 2020|

我将尝试解释为什么形式化验证是更好的选择。尤其是为什么在验证铁路系统的安全需求时使用形式化验证是一种好的做法。 为了做出令人信服的论证,我需要从头开始。

信号设计自动化论坛2019年会总结

By |十一月 19th, 2019|

11月6日,Prover在上海主办了2019年信号设计自动化论坛。 我们的主旨是召集铁路信号行业以及相关安全关键行业的专业人士,共享和讨论设计自动化的最新进展,使用软件技术实现铁路信号系统的自动化设计和验证,并特别地关注了通过形式验证保证安全。

保存日期 – SDA论坛将于2019年11月6日在北京举行

By |七月 8th, 2019|

2017年,Prover Technology公司萌生了技术论坛的想法,我们希望创建一个分享经验和最佳实践以及相互沟通的论坛。 我们的目的是聚集来自世界各地领先的信号管理同行,并讨论自动化铁路信号系统的设计和验证中设计自动化和形式验证软件技术的最新发展,所以SDA论坛诞生了。 第一次会议由Prover公司于2017年5月15日在斯德哥尔摩主办。

Go to Top