计算机系统被应用于各种重要领域, 这些系统的失效可能会带来重大灾难.不同应用领域的系统对于可信性具有不同的要求, 如何建立高质量的可信计算机系统, 是这些领域共同面临的巨大挑战.近年来, 具有严格数学基础的形式化方法已经被公认为开发高可靠软硬件系统的有效方法.目标是对形式化方法在不同系统的应用进行不同维度的分类, 以更好地支撑可信软硬件系统的设计.首先从系统的特征出发, 考虑6种系统特征: 顺序系统、反应式系统、并发与通信系统、实时系统、概率随机系统以及混成系统.同时, 这些系统又运行在众多应用场景, 分别具有各自的需求.考虑4种应用场景: 硬件系统、通信协议、信息流以及人工智能系统.对于以上的每个类别, 介绍和总结其形式建模、性质描述以及验证方法与工具.这将允许形式化方法的使用者对不同的系统和应用场景, 能够更准确地选择恰当的建模、验证技术与工具, 帮助设计人员开发更加可靠的系统.
Computer systems have been applied in many different areas, and the failure of these systems may bring catastrophic results. Systems in different areas have different requirements, and how to build trustworthy computer systems with high quality is the challenge faced by all these areas. Recently, formal methods with rigorous mathematical foundation have been widely recognized as effective methods for developing trustworthy software and hardware systems. Based on formal methods, this paper presents a classification of requirements of systems and their formalization, to support the design of trustworthy systems. First of all, six types of system characteristics are considered, namely, sequential systems, reactive systems, parallel and communicating systems, real-time systems, probabilistic and stochastic systems, and continuous and hybrid systems. All these systems may run in different application scenarios, with their respective requirements. Four classes of scenarios are considered, i.e., hardware systems, security protocols, information flow, and AI systems. For each class of systems and application scenarios above, the related formal methods are introduced and summarized, including formal modeling, property specification, verification methods and tools. This will allow users of formal methods to choose, based on different system characteristics and application scenarios, the appropriate formal models, verification methods and tools, which ultimately helps the design of more trustworthy systems.
随着计算机科学和技术的飞速发展, 大量计算机系统被应用于人们生活的各个方面, 计算机系统的可信保障[
近年来, 形式化建模与验证广泛应用于软硬件系统的正确性保障, 并被认为是开发高可信软硬件系统的有效方法[
针对不同类型的系统和性质, 采用什么样的数学语言去描述, 使用什么样的方法和工具去验证, 存在共通之处, 但同时也存在较大差异. 对各类系统和性质所采用的形式化方法进行整理, 一方面能够更准确地为不同的系统和应用场景选择恰当的验证技术与工具, 另一方面也有助于更完整地描述不同系统的可信性需求. 这对于可信系统的设计与开发具有重要的理论和实际指导意义. 本文的目标是对可信系统的需求和形式化方法在不同系统中的应用进行不同维度的分类, 以更好地支撑基于形式化方法的可信软硬件系统的分析与验证.
我们首先从不同的系统特征出发, 考虑6种系统特征: 顺序系统、反应式系统、并发与通信系统、实时系统、概率随机系统以及混成系统. 同时, 我们考虑4种应用场景: 硬件系统、通信协议、信息流以及人工智能系统. 这些系统特征和应用场景并非互不相容, 而是有很多交叉之处. 针对每种系统特征和应用场景, 我们对相关的形式化方法研究进行概述, 主要关注以下3个问题.
(1) 系统描述语言, 即可以使用哪些形式化模型对系统的行为进行建模. 常见的建模语言包括迁移系统、自动机、进程代数、重写系统等. 根据不同的系统特征, 需要对这些基本建模语言进行相应的拓展. 例如, 实时系统需要建模语言包含时钟的描述, 混成系统需要建模语言使用微分方程描述连续行为, 通信协议的建模语言需要刻画攻击者模型, 等等.
(2) 性质规约语言, 即可以使用哪些形式语言描述系统需要满足的性质. 常见的性质规约语言包括命题逻辑和谓词逻辑、时序逻辑、动态逻辑、霍尔逻辑、区间演算等. 性质规约语言的选择需要考虑性质是否只关注输入输出关系还是整个运行过程, 以及是否需要考虑实时和概率因素等.
(3) 验证方法与工具, 即在给定系统描述和性质规约后, 采用哪些方法验证系统满足规约, 以及现有哪些验证工具. 验证方法可以分为两大类: 模型检验[
形式化方法领域已有多篇综述文章[
本文第1−6节分别介绍6种系统特征. 第7−10节分别介绍4种应用场景. 第11节对本文进行总结.
在本文中, 我们将串行执行的程序称为顺序系统. 这种程序在给定输入后, 经过计算返回输出结果. 我们关心的性质包括: 程序的功能正确性(functional correctness), 即给定合法的输入, 返回的输出结果应该满足一定的性质; 终止性, 即程序针对合法的输入是终止的. 相对于后面章节描述的系统, 顺序系统的形式和性质都比较单一. 然而, 顺序系统的正确性属于形式化方法最初研究的范畴, 仍然有非常丰富的理论, 是研究更复杂系统的基础. 本节将先后介绍顺序系统的形式语义、验证逻辑、终止性和不变式生成、软件模型检验以及验证工具.
顺序系统一般使用程序语言来表示. 最简单的程序语言包含赋值、顺序语句、条件语句和循环语句. 更复杂的程序语言添加函数调用(包括递归调用)、指针以及类、对象、方法调用、动态绑定等面向对象语言的元素. 程序语言的形式语义为程序的行为给出数学的定义, 可以分为3种类型: 操作语义、指称语义和公理语义. 操作语义由Plotkin提出[
最初研究的程序验证方法使用逻辑推导的方式, 其主要思想是在程序中插入断言, 表达到达每个程序语句时系统状态应当满足的性质. Floyd首先提出使用断言描述程序正确性的思想[
以上介绍的霍尔逻辑为程序验证提供了一个理论框架, 而不是完全自动的方法, 其主要原因是, 基于霍尔逻辑的正确性验证需要提供每个循环和递归调用的不变式. 如果还要证明程序的终止性, 则需要提供循环和递归调用的秩函数(ranking function). 不变式和秩函数的自动生成存在相当多的研究[
模型检验技术也可用于顺序系统的验证. 针对一般应用程序进行模型检验的研究称为软件模型检验[
目前有许多程序验证工具以霍尔逻辑及其扩展为基础, 这里仅列出几个代表. VeriFast[
软件模型检验最初的一个成功案例是SLAM[
顺序系统的正确性只关注系统的输入和输出, 然而对于一些系统, 我们不仅关注输入和输出, 还关注系统的整个运行过程. 我们称这类系统为反应式系统(reactive system), 它在运行过程中持续与环境进行交互, 而不是生成某个计算结果. 反应式系统的运行过程可以表示为由状态(state)和事件(event)构成的序列, 时序性质则是描述这些序列的性质. 本节将介绍反应式系统的行为模型、性质规约语言、时序性质的分类, 以及时序性质的验证工具.
反应式系统可以使用迁移系统建模. 迁移系统[
反应式系统所关注的性质是时序性质, 即对迁移系统的执行路径的要求. 我们可以用自动机[
如果一个时序性质可以被有穷状态自动机表示, 则这个性质是正则性质. 正则安全性质可以用非确定性有穷自动机(NFA)来表示其“坏前缀”; 其他正则性质可以用非确定性Büchi自动机(NBA)[
非确定性有穷自动机是用来接受有穷输入序列的自动机, 可被形式化地表示为元组〈
非确定性Büchi自动机可用于接受无穷输入序列, 其语法与NFA相同, 不同之处在于其接受语言的定义. 对于非确定性Büchi自动机
线性时序逻辑从线性的角度考虑性质, 即每一时刻只考虑一个后继的状态. 因此, LTL公式定义在系统的单条路径上. LTL的语法如下:
其中,
LTL可以使用基于自动机的方法进行模型检验[
计算树逻辑从分支的角度考虑性质. 在迁移系统中, 一个状态可以对应多个后继状态, 因此, 从一个状态出发可以有多条路径, 形成一个树状结构. 在这种树状结构上定义性质, 即分支时序逻辑[
其中, ∃
验证迁移系统
CTL*[
LTL与CTL的表达能力无法比较, 即有些性质可以用LTL表达但不能用CTL表达, 而有些性质可以用CTL表达但无法用LTL表达. CTL*的表达能力强于CTL和LTL, 且CTL*还能表达LTL和CTL无法表达的性质.
关于
时序性质中有两类特殊的性质特别受到关注: 安全性(safety)[
● 一个性质是安全性质, 如果性质的违反总能在有限步内发现. 也就是说, 对于任何违反安全性质
● 一个性质是活性性质, 如果性质的违反永远无法在有限步内发现. 也就是说, 对于任何路径的前缀
除了理论意义之外, 安全性和活性的分类在现实应用中也有指导作用. 一般来说, 安全性和活性的验证方法不同. 安全性的验证一般通过寻找系统的不变式, 而活性的验证则需要寻找秩函数. 由于安全性的违反总能在有限步内察觉, 系统的公平性假设对安全性的验证没有帮助. 然而, 在很多情况下, 活性的验证需要对系统做出公平性假设.
安全性和活性的定义还被扩展到分支时间(计算树)的场景[
对于线性时间性质, 任意性质
除了安全性与活性的分类之外, 还有其他的线性时间性质的分类方法. Manna等人[
时序性质间的包含关系[
目前, 常用的反应式系统的时序性质验证工具有NuSMV[
NuSMV用于LTL模型检验、CTL模型检验和限界模型检验, 是对SMV工具的再实现和改进. NuSMV整合了基于BDD的符号模型检验和基于SAT的限界模型检验, 接受自动机模型作为输入, 验证该模型是否满足由LTL、CTL描述的性质, 在不满足时给出反例. NuSMV可用于验证通信协议[
SPIN (simple promela interpreter)是用于验证并发系统和分布式系统的开源工具, 起源于贝尔实验室形式化方法与验证小组开发的PAN. 在SPIN中, 使用Promela (process meta language)语言对需要验证的系统进行建模. SPIN支持验证安全性和活性、是否存在死锁、是否违反给定断言等性质. SPIN可用于验证分布式算法[
Murphi是一种描述语言, 也是用于验证有限状态并发系统的验证工具. 使用者需先用Murphi语言对协议建模, 进而使用Murphi工具验证该协议是否满足性质. 性质一般表示为不变式. Murphi已被成功应用于许多实际问题的验证, 特别是微处理器缓存一致性问题[
基于动作的时序逻辑(temporal logic of actions, TLA)[
当多个系统并发执行时, 它们通过共享数据或者通道通信的方式来相互沟通信息. 对于共享数据, 需要关注的性质是不发生数据竞争, 即一个线程在使用某个共享数据时, 另一个线程不能对这个数据进行修改. 避免数据竞争的一个常见方法是在共享的数据上加锁, 通过获取锁和释放锁来控制共享数据的访问和修改. 另一个性质是公平性. 当线程的执行顺序通过一个调度器决定时, 调度策略需要保证每个线程都能分配到一定的执行时间, 没有线程出现饿死的情况, 这称为调度策略的公平性. 公平性还体现在锁和信号量分配的策略中, 保证每个线程都有机会获得这些资源.
基于通道通信的并发具有多种实现方式.
● 同步通信, 即发送方和接收方必须同时准备好执行时, 同步通信才能发生.
● 异步通信, 即发送方不需要等待总是立刻发生, 而只要发送的数据集合不为空, 接收方随时从发送的数据中接收数据. 当发送的数据为空时, 接收方需要等待.
● 广播通信, 即发送方总是立刻发生, 同时, 所有同通道上可行的接收方都与发送方同步发生.
对于基于通道通信的并行系统, 关注的性质有无死锁、无活锁.
(1) 无死锁: 在并发程序中, 2个或多个线程为了获取信号量或其他资源相互等待其他进程, 造成所有进程都无法继续执行, 这称为死锁. 系统设计的问题, 例如线程忘记释放锁, 或不合理的获取锁的顺序, 都可能造成死锁情况.
(2) 无活锁: 当2个或多个线程之间无限次地重复通信, 而无法在实际任务中取得进展, 这称为活锁. 不合理的线程间通信的协议可能造成活锁现象.
对于不同的并发与通信的建模机制, 相应的性质规约和验证方法差别很大. 进程代数是一种常用的系统建模的方法. 它使用代数公式来描述系统模型, 非常适合描述系统的并发和通信特征. 目前, 研究最多的进程代数语言包括通信系统演算CCS和通信顺序进程CSP. 我们下面将首先介绍以进程代数为基础的并发通信系统, 然后介绍Petri网以及并发系统的验证工具.
通信系统演算(calculus of communicating systems, CCS)由Robin Milner在20世纪70年代提出[
● 一类是外部动作, 用于描述进程间通信的同步和交互. 外部动作发生在一个系统的两个进程之间, 因此通常成对出现, 其中一个进程产生发送信号的动作, 相应地, 另一个进程产生接收信号的动作, 我们通常用
● 另一类动作是内部动作, 即非交互动作, 由单独一个进程产生, 与环境无关, 通常用
外部动作和内部动作构成了CCS的动作集. CCS进程由并发系统中比较直观的语法操作构成, 包括动作前缀、选择操作、并发操作、限制操作和重命名操作等.
CCS通过定义结构操作语义来定义其语义, 表示为一个标号迁移系统. 每个迁移关系形式为
在CCS中, 互模拟等价关系是一个非常重要的概念, 是CCS系统验证的基础. 下面介绍相关的概念.
我们用〈
1. 若存在动作
2. 若存在动作
若〈
基于强互摸拟关系的性质规约可以使用Hennessy-Milner逻辑(HML)[
前面4个公式的定义和传统逻辑一致. 对于最后两个公式: [
HML与上述强互摸拟性质的关系为: 系统
例如, 对于系统
除了上述定义的互模拟关系以外, 在CCS中还通常使用观测等价性, 它忽略内部动作的行为. 首先定义几个概念. 给定
1. 若存在动作
2. 若存在动作
从直观上看, 由于内部动作是环境中不可观测的, 故这个弱等价关系也被称为观测等价性. 它是一种更加宽泛的互模拟关系.
MWB是一个基于CCS和π-演算的并发系统分析与验证工具[
通信顺序进程(communicating sequential processes, CSP)由C.A.R Hoare提出[
CSP的语法规则可以定义如下:
其中,
● STOP表示死锁的系统.
● SKIP表示系统成功完成了执行.
●
●
选择由环境动作直接决定. 例如, 一个自动贩卖机进行找零, 找零1块钱时, 返回一个1块钱的硬币还是两个5角的硬币由系统内部直接决定, 而贩卖机弹出哪个商品是由顾客的选择决定的.
●
●
●
CSP具有多种不同的指称语义[
对于系统(
在失败迹语义的基础上, 失败-发散迹语义(failure-divergence semantics)对其进一步进行了扩充, 即除了失败迹以外, 还刻画进程可以执行无穷
这3种语义的表达能力依次增强, 在确定语义模型之后, 可以定义精化的概念. 给定两个进程
首先, 性质本身定义为一个CSP规范, 记为进程
FDR (failures divergence refinement)[
FDR已经成功验证了很多通信协议, 若协议满足所需要验证的安全性质, 则FDR正常退出; 否则, FDR会给出一种不满足给定安全性质的攻击. 在实际的应用中, Donovan等人[
Petri网是对离散并行系统的数学表示, 由Carl Adam Petri于1962年提出, 是针对复杂系统进行模型分析、验证、仿真以及性能分析的重要工具[
在一个Petri网中, 定义格局(configuration)
Petri网具有很强的表达能力, 可以验证系统的多种性质, 其主要的验证问题如下.
1. 可达性(reachability)问题: 判断一个系统是否能够达到一个特定的状态, 或者表现出某种特定功能.
2. 可覆盖性问题[
在使用Petri网进行性质验证时, 主要包含两种方法.
● 一种是覆盖树(the coverability tree)[
● 第二, 关联矩阵与状态方程法(incidence matrix and state equation)[
目前, 基于Petri网的验证和分析工具主要有Travis[
PAT (process analysis toolkit)[
对于CSP模块, PAT扩展了以上介绍的标准CSP语法, 加入共享变量、赋值以及选择、循环等控制流结构, 语言描述更加丰富. CSP的语义被定义成一个标号迁移系统. PAT支持CSP模型之间的精化关系检查, 因此可以用于CSP的验证.
PAT在实际中具有广泛的应用. 2PC (two phase commit)协议是许多分布式关系型数据库用来完成分布式事务的重要协议. 该协议包含协调者和参与者两个进程, 对保证数据的一致性具有重要作用. PAT通过对该协议的两个阶段进行建模, 可以验证2PC协议的无死锁性质, 并可以根据需要定义相关LTL性质来进行验证. 此外, Fernando等人[
实时系统是指对于时间有严格要求的系统, 系统的状态、动作或运行轨迹需要满足一定的时间约束条件, 例如, 必须在一定时间期限内做出响应等. 汽车的控制系统、网络实时监控系统都有这些要求, 因此可以称为实时系统. 下面将从实时系统的行为规约、性质规约和验证、验证工具进行展开, 最后还对实时系统的鲁棒性进行介绍.
时间自动机(timed automata, TA)是一个常用的实时系统建模语言, 这一模型最初由Alur等人提出[
两档声控灯时间自动机
我们称TA的一个格局(configuration)是由当前位置
一个带时间戳的动作是二元组(
对于TA本身和TA之间的关系, 我们关注3类性质: 可达性、包含性和互模拟性. 其中, 可达性判定的复杂度是PSPACE的, 借助于region等价类划分的概念, 将TA的无限状态空间划分成有穷个区域(region), 从而将TA的可达性转化为有穷迁移系统上的可达性[
在文献[
和CTL一样, TCTL语法的定义分为状态公式
其中,
TPTL语法定义如下:
其中,
目前已有多种用于时间自动机验证的工具, 如Uppaal、KRONOS、RED等.
Uppaal是目前最常用的基于TA的实时系统建模、仿真、验证工具, 目前仍在维护[
KRONOS的特点在于支持多种形式的建模, 并且除了基本的TCTL性质以外, 还允许通过定义一个TA从行为的方式描述性质, 将特定性质的验证归结为忽略时钟变元后两个自动机的互模拟问题[
鲁棒性是实时系统的重要性质. 在实时系统中, 时间扮演着重要的角色, 而时间的测量、时钟的实现以及控制导致的误差会干扰系统的正常运行. 对于实时系统而言, 系统执行过程可以看成一个带时间戳的执行序列. 我们可以在所有执行构成的空间中定义一个度量, 借助度量空间的相关理论, 研究实时系统的鲁棒性[
概率系统指行为具有随机性的系统. 随机性可能来自于随机算法, 也可能来自于真实环境下系统组件失效或外界干扰等. 此外, 也可以选择将系统描述的一些不确定性使用随机性刻画. Katoen为概率模型检验的现状做了较为完整的综述[
概率系统的行为模型可以从多个维度分类: 离散时间/连续时间、确定性/非确定性、是否涉及奖励等. 由此可以延伸出多种概率模型. 下面我们介绍3种主要模型: 离散时间马尔可夫链、马尔可夫决策过程以及连续时间马尔可夫链.
离散时间马尔可夫链(discrete-time Markov chain, DTMC)是最基础的概率系统模型[
IPv4协议对应的离散时间马尔可夫链(
与DTMC对应, 刻画连续时间概率系统的基础模型是连续时间马尔可夫链(continuous-time Markov chain, CTMC), 而对连续时间下概率行为更早期的研究可以追溯到泊松过程[
工作任务队列对应的连续时间马尔可夫链
DTMC中的线性时间性质可以分为定性性质(qualitative properties)与定量性质(quantitative properties), 使用LTL公式描述. 在DTMC的线性时间性质验证中, 4种基础的LTL定性性质(可达性、约束可达性、重复性和持续性)可以通过忽略DTMC中迁移概率的具体数值, 仅区分迁移概率大于0 (存在一条边)和等于0 (不存在边), 并分析图的结构验证[
DTMC和CTMC的分支时间性质可以分别由概率计算树逻辑(probabilistic CTL, PCTL)和连续随机逻辑(continuous stochastic logic, CSL)描述, 这两种逻辑都是在CTL中引入概率.
PCTL的语法定义如下, 同样分为状态公式
PCTL移除了CTL状态公式中的全称量词和特称量词, 补充了概率算子
例如,
CSL的语法定义如下, 同样分为状态公式
CSL在CTL的基础上引入了概率算子
Katoen等人将安全-活性的分类方式拓展到概率模型中[
PRISM模型检验工具支持对概率系统的建模、仿真和验证[
STORM是2017年发布的一款功能强大的概率模型检验工具[
EPMC (原iscasMC)是由中国科学院软件研究所开发的一款基于网页的模型检验工具[
类似的验证工具还有MRMC[
以上工作都是从自动机的角度出发描述系统的概率行为, 使用模型检验方法验证系统的概率性质. 近年来, 在程序模型中加入概率, 并以概率霍尔逻辑或最弱前期望(weakest pre-expectation)语义为基础验证概率性质, 是另一种基于逻辑推理的形式化验证方法. 目前主要集中于离散程序, 在命令式程序中加入概率选择或概率赋值. 例如,
概率性质验证的一个主要应用方向是可靠性和可用性验证: 系统的可靠性(reliability)指的是在给定条件、给定时间区间下, 系统能够无失效地执行要求的能力; 而可用性(availability)指的是系统处于按要求执行状态的能力. 在一个系统中, 可靠性和可用性是密切相关的. 从概率的角度来看, 系统可靠性指的是在给定的时间区间
在本节内容中, 我们将介绍系统可靠性和可用性常用的方法——故障树(fault tree, FT)分析以及可靠性框图(reliability block diagram, RBD), 并对相关的可靠性可用性验证工具进行介绍.
标准故障树(也称静态故障树)是最基本的故障树, 由Bell实验室在20世纪60年代提出, 并用于分析导弹[
● 事件分成基本事件和中间事件(包括未展开事件、条件事件等等): 基本事件为在系统中要分析的基本元组件, 在故障树模型中用一个圆圈表示; 出现在故障树最顶部的事件称为顶事件, 一般为所分析的系统的需求事件, 用矩形表示. 例如, 研究一台计算机是否正常运行时, 基本事件包含这台计算机的CPU、内存、磁盘等等, 顶事件就是这台计算机没有正常运行, 非基本事件包含这台计算机是否在使用等.
● 故障树中所使用的门和数字逻辑中的门电路类似, 包含了与门、或门、表决门(在
一个基本的故障树示例
在Codetta-Raiteri等人的研究[
接着, 可以在树结构中进行性质的分析. 从定性性质上, 可以找到树中的最小割集(minimal cut sets, MCS)和最小路径集(minimal path sets, MPS), 从而确定整个系统正常运行的条件. 最小割集是一个系统的最少组件集合, 这个集合中的组件全部出故障, 则整个系统出故障. 上图中的{
给定一个故障树, 经典的求最小割集和最小路径集的算法是自顶向下和自底向上的方法[
从定量性质上, 首先考虑单一时刻, 一个系统的可靠性是系统在该时刻下不出现错误的概率[
标准故障树还能进行一系列的扩展, 例如, 使用动态故障树(dynamic fault tree, DFT)来处理包含序列的组件[
● PAND门: 当输入按顺序从左到右依次为1时, 门的输出才为1. 例如, 一个设备有一个备份, 只有当备用触发开关激活后, 若此备份失效, 这部分组件才会失效. 我们用PAND门表示了这种组件序列依赖的关系.
● FDEP(function dependency)门: FDEP的输出是一个伪输出(即恒等于0), FDEP门有一个触发器, 当触发器触发时, FDEP门会使所有的门输入进行激活(即输入等于1), 当然, 其输入不一定需要触发器进行触发. 例如, 电源的失效可以导致所有CPU的失效, 我们可以把电源看作一个触发器, 用FDEP门来表示电源与CPU之间的关系.
● SPARE门: 表示可由一个徽章多个备件替换的组件. 当主设备发生故障时, 从左到右激活第1个可用的备件, 一个备件可以连接到多个SPARE门, 但只能被一个SPARE门使用. 例如, 一个计算机系统中可以有内存备份, 当一个内存失效时, 可以用备份内存替换进行工作.
动态故障树的实例[
这个故障树实例加入了两个动态故障树的门结构FDEP门和SPARE门, 对于FDEP门而言, 当PS触发时,
此外, 研究者还考虑了一些其他方面的拓展. 例如, 由于实际的故障分布难以获取, 研究者考虑用模糊数代替组件的故障分布[
有很多基于故障树的工具用于进行系统的可靠性和可用性分析. 例如, CORAL[
可靠性框图[
同样地, 类似于标准故障树到动态故障树的拓展, RBD可以考虑动态依赖因素, 拓展成为DRBD. Distefano等人[
基于RBD和DRBD也存在一些形式化验证的工具. 例如, Object-Z[
动力系统指的是随着时间连续演化的系统, 其连续行为通常使用微分方程等数学模型来描述. 混成系统是既包含离散行为也包含连续行为的系统, 典型的例子是受离散程序控制的动力系统: 每个时间周期(或每个事件发生时)离散程序执行一次, 改变系统的离散状态或参数; 然后, 系统以微分方程刻画的规律随时间演化. 混成系统广泛存在于航空航天、自动驾驶等安全攸关领域, 这些系统的失效会带来人员伤亡等灾难性后果. 因此, 对这些系统的安全设计及验证变得极为重要. 基于严格数学基础的形式化方法是确保这些系统安全的重要支撑.
混成系统可以使用多种形式化建模语言表达, 其中, 由Henzinger提出的混成自动机模型[
混成自动机的实例
混成自动机的优点是语言相对简单. 然而和有限状态自动机一样, 混成自动机的可组合性较弱, 对于复杂的系统, 很难体现系统的模块化结构. 除了混成自动机以外, 其他混成系统建模语言包括微分动态逻辑(differential dynamic logic, dL)[
除了形式化模型之外, 工业界普遍使用的嵌入式系统建模语言可用于描述混成系统, 例如Simulink[
Modelica则定义了一个能够表达微分方程和微分代数方程(differential algebraic equation)的程序语言.
对于混成系统, 我们最关注的性质依然是安全性, 也就是系统不会进入危险状态, 例如自动驾驶的车辆不会与其他车辆相撞. 除了安全性外, 我们也可以考虑活性性质, 例如自动驾驶的车辆最终能够到达目的地.
混成系统的任何时序性质可以使用LTL的扩展MTL和STL表达. MTL (metric temporal logic)[
其中, 主要添加的语法构造是
STL (signal temporal logic)[
目前讨论的MTL和STL的语义都是布尔语义, 也就是说, 每条轨迹或者满足性质或者不满足性质. 对于连续和混成系统, 这类语义在很多场景下并不恰当. 例如, 如果需要的STL安全性性质是□[0, ∞]
关于STL的模型检验已有一些研究[
可达集计算是混成系统安全设计及验证的主要技术手段, 其中, 系统连续行为可达集计算是主要技术发展瓶颈. 可达集一般不可准确计算, 因此文献中主要研究可达集上、下近似的计算.
可达集上近似是包含准确可达集的集合, 一般用于安全性验证. 如果可达集上近似与危险状态不相交, 则准确可达集与危险状态不相交, 从而系统是安全的. 可达集上近似是近30年混成系统安全验证的研究热点之一, 其理论及计算方法得到了较好的研究, 如泰勒模型方法[
可达集下近似是准确可达集的子集, 一般用于安全设计. 以可达-规避集合为例来说明可达集下近似如何用于系统安全设计, 如通过计算向后可达集的下近似, 可以确定使系统进入目标区域且在进入目标区域前规避危险状态的初始状态集合(也称为可达-规避集合). 可达集下近似计算近8年来才开始研究, 理论及方法相对匮乏. 但经过近几年的研究, 涌现出了一些理论方法, 如区间计算方法[
混成系统的模型检验工具包括SpaceEx[
SpaceEx[
C2E2在实际应用中对很多信息物理融合系统进行了验证分析, 如Duggirala等人[
KeYmaera在混成系统的验证中具有广泛应用: 在文献[
硬件验证是模型检验最早也最成功的工业应用案例. 很多模型检验技术的发展最初用于硬件模型检验, 例如符号模型检验[
硬件模块的设计可以建模为一个迁移系统, 其状态空间由
描述一个初始值为〈
在硬件系统的验证中, 最关注的性质依然是安全性. 给定一个由谓词
例如, 以上给出的系统满足任何时候
由于硬件模型检验普遍应用, 已经产生了标准的行为和性质描述语言和文件格式. 在行为描述方面, 一般采用基于网表的格式, 例如AIGER[
硬件模型行为和性质的描述本身相对简单, 可以使用一般的LTL模型检验方法验证. 因此, 硬件验证的主要挑战来自待验证的模型规模非常庞大, 可能涉及上万个布尔变量, 而状态空间则是变量个数的指数. 硬件模型检验的研究主要关注如何通过符号化的方法, 结合基于不变式生成的定理证明技术来处理庞大的状态空间.
第1个在显式状态空间基础上的突破是符号模型检验[
为了能够验证模型的正确性, 也就是说在任意多步内都不会出错, 主要使用的想法是寻找模型的归纳不变式. 一个表达式
如果存在这样一个归纳不变式, 则可证明模型的确满足安全性性质
继插值法之后的下一个主要进展是IC3算法[
硬件模型检验的算法在近期依然是一个研究热点. 除了IC3之外, 其他一些方法, 包括CAR (complementary approximate reachability)[
硬件模型检验竞赛(hardware model checking competition, HWMCC)是每1年或2年举行一次的模型检验工具之间的竞赛, 在工业界提供的实例上比较工具的性能. 目前, 性能处于前列的工具包括AVR[
通信协议是现代计算机网络连接的约定标准, 是保障计算机之间信息传递的安全性的重要基础. 通信协议可以用于用户之间或用户和服务之间进行认证, 并产生双方共享的密钥, 保证双方通信的安全性. 然而, 如果通信协议的设计或实现存在漏洞, 则可能允许入侵者监听通道上发送的私密信息, 也可能允许入侵者伪装成其中一方与另一方进行通信, 造成信息泄露等通信安全问题. 因此, 保障通信协议的安全性对于计算机网络是十分重要的. 基于模型检验的方法在验证通信协议方面已经有了很多研究. 我们在本节将主要阐述验证使用的协议和攻击者的模型、性质描述, 以及验证方法和工具.
在描述通信协议时, 我们首先需要确定以下概念[
● 通信方(agent): 表示能够执行通信操作的实体/用户.
● 角色(role): 表示通信方在一次协议运行中所扮演的角色(例如发起方(initiator)、响应方(responder)以及中间的服务器方(server)).
● 协议(protocol): 表示多个角色之间发送消息的规则和顺序.
● 会话(session): 表示协议的一次执行.
需要注意的是, 每个通信方可以参与同一个协议的多个会话(session), 并在其中扮演不同的角色. 例如, 用户
在通信协议的分析中, 最普遍使用的攻击者模型是Dolev-Yao模型[
我们使用Needham-Schroeder协议[
然而, 这个协议在Dolev-Yao攻击者模型下是不安全的. 设
1.
2.
3.
4.
5.
当这个攻击过程完成时,
除了Dolev-Yao模型之外, 最近也有对更强的攻击者模型的研究, 例如eCK[
在本节, 我们列举通信协议的一些安全性性质. 对于通信协议, 一类非常重要的性质是保证某些信息不会被攻击者截获. 这类性质称为私密性(secrecy): 对于通信方
Lowe的文章[
1. 存活性(aliveness): 当通信方
2. 弱一致性(weak agreement): 当通信方
3. 非单射一致性(non-injective agreement): 当通信方
4. 单射一致性(injective agreement): 当通信方
在以上性质中, 我们也可以加入近期性(recentness)的要求, 即定义一个验证时间
根据以上的定义, 我们可以看出, Needham-Schroeder满足存活性, 但不满足弱一致性: 通过中间人攻击,
Lowe最早基于FDR开发了通信协议验证工具Casper[
Tamarin将通信协议和攻击者建模为一个迁移系统. 系统的状态表示攻击方所知的信息、网络上的信息、新产生的值和协议方的状态, 表达为一个由已知事实(fact)组成的多重集. 系统的迁移由多重集的重写规则表达, 描述协议的规则和攻击者的能力. 加密、解密等函数的代数性质使用一个等式理论(equational theory)表达. 安全性质表达为关于迁移系统的路径的一阶逻辑公式. Tamarin使用约束求解算法对性质进行验证, 通过反向搜索的方式, 试图找到一个违反性质的路径: 如果找到了这个路径, 则说明性质不成立, 并在用户界面上展示这个反例; 如果不能找到路径, Tamarin可以生成一个该性质的证明. 由于所涉及的验证问题是不可判定的, Tamarin的自动验证不能保证终止. 但是在很多实际例子中, Tamarin能够在很短的时间内完成验证或找到反例. 除了安全性质, Tamarin也能验证协议中的一些隐私性质及观察等价性(observational equivalence). Tamarin在很多安全通信协议上取得了非常成功的应用, 例如, Schmidt等人使用Tamarin验证了NAXOS协议在eCK攻击者模型下的安全性[
ProVerif和AKiSs基于Applied pi演算对协议建模. Applied pi演算[
基于Applied pi演算验证的基础是进程之间的等价性概念, 其中, 静态等价性(static equivalence)表达两套替换之间的不可区分性. 观察等价性和带标注的互模拟关系(labeled bisimilarity)表达了进程之间行为的不可区分性, 其中, 观察等价性的定义需要考虑所有可能与进程交互的环境, 因此直接验证非常复杂. 相比之下, 带标注的互模拟关系更易于直接验证. Applied pi演算理论的一个核心定理是, 观察等价性和带标注的互模拟关系是等价的.
ProVerif工具实现了Applied pi演算模型的可达性(reachability)、一致性(correspondence)和观察等价性的验证算法, 其中, 一致性[
AKiSs可用于验证有限会话假设下通信协议的观察等价性, 输入语法与Applied pi演算语法相似, 输出结果为所查询的两个进程是否满足观察等价性. 由于AKiSs只考虑有限会话的场景, 并使用了不同的算法, 可以用于验证一些ProVerif无法验证的协议, 例如Okamoto电子投票协议[
另一种完全不同的验证方式是使用逻辑推理来证明协议的安全性, 称为可证明的安全性(provable security). 其主要步骤是: 首先, 定义协议模型和攻击者模型; 然后, 定义对密码系统的安全假设; 最后, 通过归约(reduction)将攻击者针对协议安全性质的攻击行为最终转化为密码系统安全假设的违反, 从而说明协议的安全性质(在密码系统安全假设成立的情况下)不会被违反. Barthe等人使用概率程序对协议和攻击者行为进行建模, 并使用概率关系霍尔逻辑(probabilistic relational Hoare logic)证明协议的安全性, 实现了工具EasyCrypt[
信息流性质一般指信息不会在未经授权的情况下被访问、修改和泄露, 同时保证被授权的一方在给定的权限内, 合理地访问和使用信息. 我们这里主要介绍3类信息流性质: 无干扰性(noninterference), 即高机密级别的操作不能影响低机密级别的状态和输出; 不透明性(opacity), 即系统的秘密对外界的入侵者来说不透明; 以及隐私性, 即用户和用户的数据之间的对应关系一定程度地被隐藏起来, 使得攻击者无法推导. 我们针对这3类性质, 分别从模型、性质描述和验证这些方面进行展开.
无干扰性的定义依赖一个安全模型(security model), 描述哪些用户/进程可以访问或修改哪些资源, 或者哪些用户/进程之间可以发送信息. Rushby基于不同迹之间的unwinding关系等价性, 首次给出了具有非传递性的无干扰性的形式定义[
在给出定理之前, 先介绍几个定义. 系统
即如果
后来, von Oheimb对这个定义进行了扩展, 能够处理非确定系统的情况, 并且能够描述更多的性质, 例如无泄露性质(nonleakage)和无影响性质(noninfluence)[
以上的工作都是基于状态机, 除此之外, 还有基于进程代数的无干扰性的建模和验证[
以上的工作都是针对静态政策, 无干扰性还被推广到动态政策, 即系统的信息流政策可以在执行过程中改变, Eggert等人给出了形式定义[
对于无干扰性的验证, Hadj-Alouane等人[
不透明性(opacity)可以用来描述系统的安全与隐私性质. 有的研究者认为, 不透明性可以归类到关于系统秘密行为的隐私问题. 另外, 匿名(anonymity)和保密(secrecy)性质也都可以用不透明性来阐释. 不透明性的目标是保护系统的秘密, 使其对外界的入侵者来说不透明. 具体来说, 外界入侵者掌握系统的模型构造的全部内容, 但是在观测系统的行为时, 信息流的局部不能被观测到, 或者不能被准确地观测到. 外界入侵者将基于上述信息, 对系统的秘密进行推断. 如果在系统的任何一种运行下, 外界入侵者都不能准确发现系统的秘密, 则称系统对该入侵者而言是不透明的. 由上面的描述可知, 不透明性的研究中带有两个参数: 系统的秘密, 记作
基于秘密的类型, 不透明性可以分为两大类: 当系统的秘密是一个语言, 即一个“秘密的行为序列”的集合时, 称为基于语言的不透明性(language-based opacity, LBO); 当系统的秘密是系统的一个状态集合, 即一个“秘密的状态”的集合时, 称为基于语言的不透明性(state-based opacity, SBO). 在系统为离散动态系统的背景下, 共有两种系统模型: 自动机和Petri网. 另外, 在考虑物理时间的条件下, 系统模型为时间自动机. 不透明性的验证问题一般情况下是不可判定的. 对于自动机模型, Saboori和Hadjicostis以有限状态机为模型, 分别研究了初始状态不透明性(Initial state opacity)、
Petri网模型是一种用来研究离散事件系统的基本数学工具. Petri网模型不仅像自动机模型一样具备直观的图表达与严格的数学表达, 而且在某种程度上还能扩展自动机模型的建模能力. 文献[
对于时间自动机模型, 问题的复杂程度将大幅度上升, 甚至出现不可判定的情况. 解决不可判定的问题有以下方式: (1) 找到时间自动机的子集, 使得不透明性在该子集上变成可判定问题; (2) 缩小不透明性的范围, 使问题变得可解[
一个系统满足隐私性, 如果它能够将用户和用户的系统数据之间的对应关系(correspondence)一定程度地隐藏起来, 而攻击者无法由已知信息推导出这个对应关系. 按照隐藏的程度不同, 系统将提供不同强度的隐私性. 最常见的隐私性质有[
Bohli等人[
前面所介绍的功能性质、时序性质、通信性质、协议的鉴权性质等, 都是单个轨迹的性质, 即描述系统的每个运行轨迹都满足某个性质. 但是, 很多信息安全性质不能如此表示, 因为它们需要表达系统的两个或多个运行轨迹之间的关系, 例如上面介绍的无干扰性. Clarkson等人提出了超性质(hyperproperties)[
Clarkson等人后来又将时序逻辑扩展到超性质中[
最后, 对于安全-活性的分类, 已经证明, 任何一个超性质都可以表示为某一个超安全性和某一个超活性的合取[
近些年来, 基于深度神经网络的人工智能系统得到了飞快的发展以及越来越广泛的应用, 智能系统的正确性也因此受到越来越多的关注. 关于深度神经网络的可信性和安全性已经有了很多研究, 文献[
人工神经网络, 简称神经网络, 是一种模仿生物神经网络(动物中的中枢神经系统, 特别是大脑)的结构和功能的数学模型或计算模型, 用于对函数进行估计或近似. 经过几十年的发展, 神经网络理论在模式识别、自动控制、信号处理、辅助决策、人工智能等众多研究领域取得了广泛的成功. 深度神经网络是深度学习的一种框架, 它是具备至少1个隐藏层的神经网络. 与浅层神经网络类似, 深度神经网络也能够为复杂非线性系统提供建模, 但多出的隐藏层为模型提供了更多抽象层次, 因此提高了模型的抽象能力. 神经网络的基本结构可以分为3层: 输入层、隐藏层、输出层, 各层由神经元和神经元之间的权值组成.
在深度神经网络中, 信号从一个神经元传入到下一个神经元之前是通过线性加权和来计算的, 而进入下一层神经元需要非线性的激活函数, 继续往下传递, 如此循环下去. 由于这些非线性函数的反复叠加, 才使得神经网络有足够的能力来抓取复杂的特征.
如果不使用(非线性)激活函数, 每一层输出都是输入的线性函数. 因此, 无论神经网络有多少层, 输出都是输入的线性函数, 这样就和只有一个隐藏层的效果是一样的, 无法逼近复杂的非线性函数. 这就是为什么激活函数都是非线性的. 比较常用的激活函数包括Sigmoid、tanh和ReLU函数.
● Sigmoid函数:
● tanh函数:
● ReLU函数:
深度神经网络具有以下特点.
(1) 神经网络与传统的参数模型最大不同之处在于, 它是数据驱动的自适应技术, 不需要对问题模型做任何先验假设. 在解决问题的内部规律未知或难以描述的情况下, 神经元可以通过对样本的学习训练, 获取数据之前隐藏的函数关系. 适用于解决一些利用假设和现存理论难以解释, 却具备足够多数据和观察变量的问题.
(2) 神经元具备泛化能力. 神经网络可以通过对输入样本数据的学习训练, 获得隐藏在数据内部的规律, 并利用学习到的规律来预测未来的数据.
(3) 神经网络是一种具有普遍适用性的函数逼近器. 它能以任意精度逼近任何非线性函数. 传统的预测模型由于存在各种限制, 不能对复杂的变量函数进行有效的估计. 神经网络的内部函数形式比传统的统计方法更为灵活、有效.
(4) 神经网络算法是非线性的方法. 神经元之间相互制约和相互影响, 使得整个网络从输入空间到输出空间形成了非线性映射, 可用于处理一些环境信息十分复杂、知识背景不清楚和推理规则不明确的问题.
我们对神经网络的可能攻击方式和期望满足的性质进行分类.
首先, 神经网络可能遇到的攻击有以下几类.
● 训练时攻击(training-time attack): 攻击者试图通过在训练集里掺入恶意的数据, 从而影响训练出来的神经网络.
● 测试时攻击(test-time attack): 攻击者试图构造对抗性的测试案例(adversarial example), 使得神经网络做出错误的判断. 这是最常见也是研究最广泛的攻击方式.
● 模型提取攻击(model extraction attack): 攻击者通过对一个模型询问, 试图获取同样的模型. 这可能会造成商业数据或个人隐私数据的泄露.
深度神经网络的性质可以分为以下几类[
● 输入-输出的鲁棒性. 这种正确性性质强调: 如果输入没有很大的改变, 输出也不应有很大的改变. 这个定义对应着大多数对抗性攻击, 通过对输入微小的扰动来误导神经网络得出错误的判断. 此外, 我们还可以把鲁棒性定义为: 如果输入相似, 则神经网络的输出相似.
● 输入-输出关系. 这种正确性性质规定: 当神经网络的输入满足条件
● 系统正确性. 这种定义方式的主要思想是: 一个神经网络应该考虑为一个更大系统的一部分. 例如, 神经网络可以作为这个系统的感知部件. 因此, 神经网络的正确性应当从整个系统的正确性考虑. 例如, 整个系统的正确性可以通过STL等时序逻辑公式描述. 在这个定义下, 神经网络的对抗样本是一个可以造成整个系统违反STL公式的样本. 同样地, 在对抗样本上进行重新训练的目标是, 使得系统在更多情况下能够满足设置的STL公式. 这种对抗和重新训练的概念被称为语义对抗深度学习(semantic adversarial deep learning)[
● 语义不变性. 对于一些应用, 输入空间
● 单调性. 在一些应用里, 输入空间
● 公平性. 近期神经网络的公平性越来越受到关注. 我们期望神经网络在做出判断时不会受到某些因素(例如年龄、种族等)的影响. 这种公平性的定义有多种方式, 例如, 可以要求神经网络给出某个输出的概率与某些敏感的特征在统计意义下是独立的; 而另一种描述方式则依赖因果模型, 定义为神经网络对于某个输入是公平的, 如果对这个输入修改某些敏感特征后, 神经网络的输出保持不变.
深度神经网络的输入/输出常常受到环境、设备及安全等因素的限制, 并且在实际应用中, 也面临着实际任务需求的限制. 因此, 如果在一些安全攸关应用领域使用深度神经网络, 例如商用飞机防撞、大规模发电厂、化工厂控制等, 我们必须对部署的神经网络进行形式验证, 以确保其能够安全运行. 深度神经网络形式验证主要涉及验证网络的输出是否满足给定的安全性质规约. 考虑到实际应用中深度神经网络的非线性、高度复杂等特性, 对其进行形式验证极具挑战性.
目前已有的神经网络验证工具包括Reluplex[
ERAN (ETH robustness analyzer for neural networks)是苏黎世联邦理工大学开发的神经网络鲁棒性的验证工具, 针对多种扰动实现了多个验证算法, 例如基于zonotopes抽象域的DeepZono[
此外, 还有许多工作从不同的角度和方向对神经网络的验证进行了探索. Seshia等人[
Dutta等人借助于局部搜索及混合整数线性规划, 提出了计算网络输出集合上近似的迭代算法[
Ruan等人证明了大多数已知的DNN层都是Lipschitz连续的, 无论其层深、激活功能和神经元数量, 且提出一种基于全局优化的自适应嵌套优化算法来进行可达性分析, 解决神经网络的安全性和鲁棒性验证[
利用抽象解释来验证深度神经网络的基本思想是: 利用合适的抽象域(比如boxes、zonotopes和polyhedra)来上近似神经网络的输入集及其计算过程, 得到神经网络输出集的上近似, 并验证其是否满足给定性质. Li等人[
对基于精确可达性分析的方法, 如何高效计算出神经网络的输出集, 则是验证问题的核心, 比如利用面-顶点关联矩阵(FVIM)来表示凸集组合结构的完整编码[
针对一个黑盒神经网络, Xue等人基于可能近似正确学习的理论(PAC learning)以及场景优化(scenario optimization), 提出了计算“黑盒”系统(包括大规模非线性深度神经网络)安全特征输入集下近似的线性规划方法[
当神经网络仅作为系统中的一部分时, 例如一个信息物理融合系统包含了复杂的机器学习组件, 整个系统的安全性验证问题则更加复杂. Dreossi等人提出一个复合框架[
ReachNN[
如何设计安全可靠的计算机系统, 是计算机科学的重大挑战. 尤其近年来智能系统在计算机领域的广泛应用, 给系统的可靠性带来更大的挑战. 具有严格数学基础的形式化方法已被公认为设计可信系统的有效方法, 在工业领域中得到越来越广泛地应用. 然而, 与传统的仿真和测试相比, 形式化方法对使用者的要求依然较高; 另一方面, 智能系统的广泛应用也带来新的形式化问题. 本文从系统的可信需求出发, 对系统进行不同维度的分类, 并调研系统设计中所用的主要形式化方法. 我们分别根据系统的特征和应用场景, 将系统进行分类. 针对每一类系统和场景, 从行为建模、性质描述、验证方法和工具等方面分别介绍有关的形式化方法. 本文最终的目的是对系统的行为和性质建立一个形式化的分类和技术框架, 以支撑包括智能系统在内的可信系统的设计.
本文由“智能系统的分析和验证”专题特约编辑明仲教授、张立军教授和秦胜潮教授推荐.
感谢成文过程中, 詹乃军研究员的指导.
Becker S, Boskovic M, Dhama A, Giesecke S, Happe J, Hasselbring W, Koziolek H, Lipskoch H, Meyer R, Muhle M, Paul A, Ploski J, Rohr M, Swaminathan M, Warns T, Winteler D. Trustworthy software systems: A discussion of basic concepts and terminology. ACM SIGSOFT Software Engineering Notes, 2006, 31(6): 1-18.
Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J. Formal methods: Practice and experience. ACM Computing Surveys, 2009, 41(4): Article No. 19.
Gleirshcer M, Foster S, Woodcock J. New opportunities for integrated formal methods. ACM Computing Surveys, 2020, 52(6): Article No. 117.
Baier C, Katoen J. Principles of Model Checking. MIT Press, 2008.
Clarke EM, Henzinger TA, Veith H. Handbook of Model Checking. Springer, 2018.
Clarke EM, Grumberg O, Kroening D,
Robinson A, Voronkov A. Handbook of Automated Reasoning. Elsevier, 2001.
Harrison J. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.
Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ. Symbolic model checking: 1020 states and beyond. Information and Computation, 1992, 98(2): 142-170.
Biere A, Cimatti A, Clarke EM, Zhu Y. Symbolic model checking without BDDs. In: Proc. of the TACAS. 1999. 193-207.
Clarke EM, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM (JACM), 2003, 50(5): 752-794.
Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019, 30(1): 33-61(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm [doi:10.13328/j.cnki.jos.005652]
王戟, 詹乃军, 冯新宇, 刘志明. 形式化方法概貌. 软件学报, 2019, 30(1): 33-61. http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
Bu L, Chen LQ, Chen Z,
卜磊, 陈立前, 陈哲, 等. 形式化方法的研究进展与趋势. 见: 中国计算机学会文集, 2018. 1-68.
Peled DA. Software Reliability Methods. Springer, 2001.
Nielson F, Nielson HR. Formal Methods, An Appetizer. Springer, 2019.
Zhang J, Zhang C, Xuan JF, Xiong YF, Wang QX, Liang B, Li L, Dou WS, Chen ZB, Chen LQ, Cai Y. Recent progress in program analysis. Ruan Jian Xue Bao/Journal of Software, 2019, 30(1): 80-109(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5651.htm [doi:10.13328/j.cnki.jos.005651]
张健, 张超, 玄跻峰, 熊英飞, 王千祥, 梁彬, 李炼, 窦文生, 陈振邦, 陈立前, 蔡彦. 程序分析研究进展. 软件学报, 2019, 30(1): 80-109. http://www.jos.org.cn/1000-9825/5651.htm [doi:10.13328/j.cnki.jos.005651]
Nielson F, Nielson HR, Hankin C. Principles of Program Analysis. Springer, 1999.
Plotkin G. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 1981, 60: 17-139.
https://www.researchgate.net/publication/242406560]]>
Floyd RW. Assigning meanings to programs. Proc. of Symposia in Applied Mathematics, 1967, 19: 19-32.
Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10): 576-580.
Dijkstra EW. A Discipline of Programming. Prentice Hall, 1976.
Apt KR, Olderog ER. Fifty years of Hoare's logic. Formal Aspects of Computing, 2019, 31: 751-807.
Reynolds JC. Separation logic: A logic for shared mutable data structures. In: Proc. of the LICS. 2002. 55-74.
Chin WN, David C, Nguyen H, Qin S. Enhancing modular OO verification with separation logic. In: Proc. of the POPL. 2008. 87-99.
Parkinson M, Bierman GM. Separation logic, abstraction and inheritance. In: Proc. of the POPL. 2008. 75-86.
Bjorner N, Browne A, Manna Z. Automatic generation of invariants and intermediate assertions. Theoretical Computer Science, 1997, 173(1): 49-87.
Cook B, Podelski A, Rybalchenko A. Proving program termination. Communications of the ACM, 2011, 54(5): 88-98.
Yang L, Zhou CC, Zhan NJ,
McMillan KL. Interpolation and SAT-based model checking. In: Proc. of the CAV. 2003. 1-13.
Garg P, Loding C, Madhusudan P, Neider D. ICE: A robust framework for learning invariants. In: Proc. of the CAV. 2014. 69-87.
Si X, Dai H, Raghothaman M, Naik M, Song L. Learning loop invariants for program verification. In: Advances in Neural Information Processing Systems. 2018. 7751-7762.
Yao J, Ryan G, Wong J, Jana S, Gu R. Learning nonlinear loop invariants with gated continuous logic networks. In: Proc. of the PLDI. 2020. 106-120.
Podelski A, Rybalchenko A. A complete method for the synthesis of linear ranking functions. In: Proc. of the VMCAI. 2004. 239-251.
Heizmann M, Hoenicke J, Podelski A. Termination analysis by learning terminating programs. In: Proc. of the CAV. 2014. 797-813.
Chen Y, Heizmann M, Lengál O, Li Y, Tsai M, Turrini A, Zhang L. Advanced automata-based algorithms for program termination checking. In: Proc. of the PLDI. 2018. 135-150.
Jhala R, Majumdar R. Software model checking. ACM Computing Surveys, 2009, 41(4): Article No. 21.
Alur R, Benedikt M, Etessami K, Godefroid P, Reps TW, Yannakakis M. Analysis of recursive state machines. ACM Trans. on Programming Languages and Systems, 2005, 27(4): 786-818.
Bouajjani A, Esparza J, Maler O. Reachability analysis of pushdown automata: Application to model checking. In: Proc. of the CONCUR. 1997. 135-150.
Esparza J, Hansel D, Rossmanith P, Schwoon S. Efficient algorithms for model checking pushdown systems. In: Proc. of the CAV. 2000. 232-247.
Alur R, Madhusudan P. Adding nesting structure to words. Journal of the ACM (JACM), 2009, 56(3): Article No. 16.
Jacobs B, Smans J, Philippaerts P, Vogels F, Penninckx W, Piessens F. VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Proc. of the NASA Formal Methods. 2011. 41-55.
Rustan K, Leino M. Dafny: An automatic program verifier for functional correctness. In: Proc. of the LPAR. 2010. 348-370.
Filliatre JC, Paskevich A. Why3-Where programs meet provers. In: Proc. of the ESOP. 2013. 125-128.
Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B. Frama-C: A software analysis perspective. Formal Aspects of Computing, 2015, 27(3): 573-609.
Ball T, Levin V, Rajamani SK. A decade of software model checking with SLAM. Communications of the ACM, 2011, 54(7): 68-76.
O'Hearn PW. Continuous reasoning: Scaling the impact of formal methods. In: Proc. of the LICS. 2018. 13-25.
Keller R. Formal verification of parallel programs. Communications of the ACM, 1976, 19(7): 371-384.
Kropf T. Introduction to Formal Hardware Verification. Springer, 1999.
Büchi, JR. On a decision method in restricted second order arithmetic. In: Proc. of the Int'l Congress on Logic, Method, and Philosophy of Science. 1962. 1-12.
McNaughton R. Testing and generating infinite sequences by a finite automaton. Information and Control, 1966, 9: 521-530.
Rabin MO. Decidability of second order theories and automata on infinite trees. Trans. of the American Mathematical Society, 1969, 141: 1-35.
Vardi MY, Wolper P. An automata-theoretic approach to automatic program verification (preliminary report). In: Proc. of the LICS. 1986. 332-344.
Pnueli A. The temporal logic of programs. In: Proc. of the FOCS. 1977. 46-57.
Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching-time temporal logic. Logics of Programs, 1981, 131: 52-71.
Kupferman O, Vardi MY. Model checking of safety properties. Formal Methods in System Design, 2001, 19(3): 291-314.
Courcoubetis C, Vardi MY, Wolper P, Yannakakis M. Memory-efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1992, 1(2-3): 275-288.
Ben-Ari M, Pnueli A, Manna Z. The temporal logic of branching time. Acta Informatica, 1983, 20: 207-226.
Queille JP, Sifakis J. Specification and verification of concurrent systems in CESAR. In: Proc. of the Int'l Symp. on Programming, Vol. 137. 1982. 337-351.
Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. on Programming Languages and Systems, 1986, 8(2): 244-263.
Iwashita H, Nakata T, Hirose F. CTL model checking based on forward state traversal. In: Proc. of the ICCAD. 1996. 82-87.
Emerson EA, Halpern JY. "Sometimes" and "not never" revisited: On branching versus linear-time temporal logic. Journal of the ACM (JACM), 1986, 33(1): 151-178.
Janin D, Walukiewicz I. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In: Proc. of the Int'l Conf. on Concurrency Theory. 1996. 263-277.
Thomas W. Infinite games and verification. In: Proc. of the Int'l Conf. on Computer Aided Verification. 2002. 58-65.
Kozen D. Results on the propositional mu-calculus. Theoretical Computer Science, 1983, 27(3): 333-354.
Kozen D. A finite model theorem for the propositional mu-calculus. Studia Logica, 1988, 47(3): 233-241.
Berwanger D, Gradel E, Lenzi G. The variable hierarchy of the mu-calculus is strict. Theory of Computing Systems, 2007, 40(4): 437-466.
McNaughton R. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 1993, 65(2): 149-184.
Jurdziński M. Small progress measures for solving parity games. In: Proc. of the Annual Symp. on Theoretical Aspects of Computer Science. 2000. 290-301.
Schewe S. Solving parity games in big steps. In: Proc. of the Int'l Conf. on Foundations of Software Technology and Theoretical Computer Science. 2007. 449-460.
Lamport L. Proving the correctness of multiprocess programs. IEEE Trans. on Software Engineering, 1977, 3(2): 125-143.
Alpern B, Schneider FB. Defining liveness. Information Processing Letters, 1985, 21(4): 181-185.
Manolios P, Trefler RJ. Safety and liveness in branching time. In: Proc. of the LICS. 2001. 366-374.
Manna Z, Pnueli A. A hierarchy of temporal properties. In: Proc. of the ACM Symp. on Principles of Distributed Computing. 1990. 377-410.
Cimatti A, Clarke EM, Giunchiglia F, Roveri M. NuSMV: A new symbolic model checker. Int'l Journal on Software Tools for Technology Transfer, 2000, 2(4): 410-425.
Holzmann G. The model checker SPIN. IEEE Trans. on Software Engineering, 1997, 23(5): 279-295.
Dill D. The Murphi verification system. In: Proc. of the CAV. 1996. 390-393.
Lamport L. Specifying Systems. Boston: Addison-Wesley, 2002.
Havelund K, Shankar N. Experiments in theorem proving and model checking for protocol verification. In: Proc. of the IBAFM. 1996. 662-681.
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.31.7109&rep=rep1&type=pdf]]>
McMillan KL, Schwalbe J. Formal verification of the encore Gigamaxcache consistency protocol. In: Proc. of the Int'l Symp. on Shared Memory Multiprocessors. 1991. 242-251.
Clarke EM, Grumberg O, Hiraishi H, Jha S, Long DE, McMillan KL, Ness LA. Verification of the futurebus+cache coherence protocol. Formal Methods in System Design, 1995, 6(2): 217-232.
Moon I. Modeling programmable logic controllers for logic verification. IEEE Control Systems, 1994, 14(2): 53-59.
Barrett G. Model checking in practice: The T9000 virtual channel processor. IEEE Trans. on Software Engineering, 1995, 21(2): 69-78.
Anderson RJ, Beame P, Burns S, Chan W, Modugno F, Notkin D, Reese JD. Model checking large software specifications. In: Proc. of the SIGSOFT FSE. 1996. 156-166.
Holzmann GJ. Protocol design: Redefining the state of the art. IEEE Software, 1992, 9(1): 17-22.
Ruane LM. Process synchronization in the UTS kernel. Computer Systems, 1990, 3(3): 387-421.
D'Argenio PR, Katoen JP, Ruys T, Tretmans J. Modeling and verifying a bounded retransmission protocol. In: Proc. of the Workshop Applied Formal Methods in System Design. 1996. 114-127.
Jensen HE, Larsen KG, Skou A. Modelling and analysis of a collision avoidance protocol using SPIN and UPPAAL. In: Proc. of the Spin Verification System. 1996. 261-277.
Ruys T, Langerak R. Validation of Bosch'mobile communication network architecture with SPIN. In: Proc. of the 3rd SPIN Workshop. 1997. 75-89.
Dill DL, Park S, Nowatzyk AG. Formal specification of abstract memory models. In: Proc. of the Symp. on Research on Integrated Systems. 1993. 38-52.
Dill DL, Drexler AJ, Hu AJ, Yang CH. Protocol verification as a hardware design aid. In: Proc. of the IEEE Int'l Conf. on Computer Design. 1992. 522-525.
Lenoski D, Laudon J, Gharachorloo K, Weber WD, Gupta A, Hennessy J, Horowitz M, Lam M. The Stanford DASH multiprocessor. Computer, 1992, 25(3): 63-79.
Mitchell JC, Mitchell M, Stern U. Automated analysis of cryptographic protocols using Mur/spl phi/. In: Proc. of the IEEE Symp. on Security and Privacy. 1997. 141-151.
Needham RM, Schroeder MD. Using encryption for authentication in large networks of computers. Communications of the ACM, 1978, 21(12): 993-999.
Tatebayashi M, Matsuaaki N, Newman D. Key distribution protocol for digital mobile communication systems. In: Proc. of the CRYPTO. 1990. 324-333.
Lamport L. The temporal logic of actions. ACM Trans. on Programming Languages and Systems (TOPLAS), 1994, 16(3): 872-923.
Beers R. Pre-RTL formal verification: An Intel experience. In: Proc. of the DAC. 2008. 806-811.
Newcombe C, Rath T, Zhang F, Munteamu B, Brooker M, Deardeuff M. How Amazon web services uses formal methods. Communications of the ACM, 2015, 58(4): 66-73.
Milner R. A Calculus of Communicating Systems. New York: Springer, 1980.
Hennessy MCB, Milner R. Algebraic laws for nondeterminism and concurrency. Journal of the ACM (JACM), 1985, 32(1): 137-161.
https://www.it.uu.se/profundis/mwb-dist/guide-3.122.pdf]]>
Victor B. A verification tool for the polyadic pi-calculus[MS. Thesis]. Department of Computer Systems, Uppsala University, 1994.
Hoare CAR. Communicating Sequential Processes. Englewood: Prentice-Hall, 1985.
Brookes SD. On the relationship of CCS and CSP. In: Proc. of the ICALP. 1983. 83-96.
Bundgaard M, Milner R. Unfolding CSP. In: Proc. of the Reflections on the Work of C.A.R. Hoare. 2010. 213-228.
Roscoe AW. Understanding concurrent systems. New York: Springer, 2010.
Schneider SA, Davies J. Timed CSP: Theory and practice. In: Proc. of the REX Workshop. 1991. 640-675.
Gibson-Robinson T. FDR3-A modern refinement checker for CSP. In: Proc. of the TACAS. 2014. 187-201.
Armstrong P, Lowe G, Ouaknine J, Roscoe AW. Model Checking Timed CSP. In: HOWARD-60. A Festschrift on the Occasion of Howard Barringer's 60th Birthday, Vol. 42. 2014. 2014. 13-33.
https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.365293]]>
https://www.cs.ox.ac.uk/publications/publication676-abstract.html]]>
doi: 10.1109/CSFW.1998.683164]]]>
Peterson JL. Petri Net Theory and the Modeling of Systems. Englewood: Prentice-Hall, 1981.
Murata T. Petri nets: Properties, analysis and applications. In: Proc. of the IEEE. 1989. 541-580.
Abdulla PA. General decidability theorems for infinite-state systems. In: Proc. of the LICS. 1996. 313-321.
Reisig W, Rozenberg G. Lectures on Petri Nets I: Basic Models: Advances in Petri Nets. New York: Springer, 1998.
Kostin A. Using Transition Invariants for Reachability Analysis of Petri Nets. INTECH Open Access Publisher, 2008.
Benjamin M, Bergenthum R. Travis-An online tool for the synthesis and analysis of Petri nets with final states. In: Proc. of the Int'l Conf. on Application and Theory of Petri Nets and Concurrency. 2017. 101-111.
Hillah LM, Kordon F. Petri nets repository: A tool to benchmark and debug Petri net tools. In: Proc. of the Int'l Conf. on Application and Theory of Petri Nets and Concurrency. 2017. 125-135.
Hu X, Li J, Li ZJ. Modelling and performance analysis of IEEE 802.11 DCF using coloured Petri nets. The Computer Journal, 2016, 59(10): 1563-1580.
Berthelot G, Terrat R. Petri nets theory for the correctness of protocols. IEEE Trans. on Communications, 1982, 30(12): 2497-2505.
https://pat.comp.nus.edu.sg]]>
Sun J, Liu Y, Dong JS, Pang J. PAT: Towards flexible verification under fairness. In: Proc. of the CAV. 2009. 709-714.
Liu Y, Sun J, Dong JS. PAT 3: An extensible architecture for building multi-domain model checkers. In: Proc. of the ISSRE. 2011. 190-199.
Fernando D, Dong N, Jégourel C, Dong JS. Verification of strong Nash-equilibrium for probabilistic BAR systems. In: Proc. of the Formal Engineering Methods. 2018. 106-123.
Fernando D, Dong N, Jégourel C, Dong JS. Verification of Nash-equilibrium for probabilistic BAR systems. In: Proc. of the ICECCS. 2016. 53-62.
Thin WYMM, Dong NP, Bai GD, Dong JS. Formal analysis of a proof-of-stake blockchain. In: Proc. of the 23rd Int'l Conf. on Engineering of Complex Computer Systems (ICECCS). 2018. 197-200.
Li L, Sun J, Liu Y. A formal specification and verification framework for timed security protocols. IEEE Trans. on Software Engineering, 2017, 44(8): 725-746.
Ling S, Liu S, Hao J. Towards solving decision making problems using probabilistic model checking. In: Proc. of the ICECCS. 2017. 150-153.
Alur R, Dill D. Automata for modeling real-time systems. In: Proc. of the ICALP. 1990. 322-335.
Alur R, Dill D. A theory of timed automata. Theoretical Computer Science, 1994, 126(2): 183-235.
Cerans K. Decidability of bisimulation equivalences for parallel timer processes. In: Proc. of the CAV. 1992. 302-315.
Konrad S, Cheng BHC. Real-time specification patterns. In: Proc. of the ICSE. 2005. 372-381.
Bouyer P, Laroussinie F, Markey N,
Alur R, Courcoubetis C, Dill D. Model-checking for real-time systems. In: Proc. of the LICS. 1990. 414-425.
Alur R, Courcoubetis C, Dill D. Model-checking in dense real-time. Information and Computation, 1993, 104(1): 2-34.
Bouyer P, Chevalier F, Markey N. On the expressiveness of TPTL and MTL. In: Proc. of the FSTTCS. 2005. 432-443.
Alur R, Henzinger TA. A really temporal logic. Journal of the ACM (JACM), 1994, 41(1): 181-203.
Larsen KG, Pettersson P, Yi W. UPPAAL in a nutshell. Int'l Journal on Software Tools for Technology Transfer, 1997, 1(1): 134-152.
Bengtsson J, Yi W. Timed automata: Semantics, algorithms and tools. In: Lectures on Concurrency and Petri Nets. 2003. 87-124.
Havelund K, Larsen KG, Skou A. Formal verification of a power controller using the real-time model checker Uppaal. In: Proc. of the Int'l AMAST Workshop on Aspects of Real-time Systems and Concurrent and Distributed Software. Berlin, Heidelberg: Springer, 1999. 277-298.
Larsen K G, Mikucionis M, Nielsen B,
Larsen KG, Lorber F, Nielsen B. 20 years of UPPAAL enabled industrial model-based validation and beyond. In: Proc. of the Int'l Symp. on Leveraging Applications of Formal Methods. Cham: Springer, 2018. 212-229.
Yovine S. Kronos: A verification tool for real-time systems. Int'l Journal on Software Tools for Technology Transfer, 1997, 1(1-2): 123-133.
Bozga M, Daws C, Maler O,
Wang F, Yao LW, Yang YL. Efficient verification of distributed real-time systems with broadcasting behaviors. Real-time Systems, 2011, 47(4): 285-318.
Gupta V, Henzinger TA, Jagadeesan R. Robust timed automata. In: Proc. of the HART. 1997. 331-345.
Bouyer P, Markey N, Sankur O. Robustness in timed automata. In: Proc. of the RP. 2013. 1-18.
Katoen JP. The probabilistic model checking landscape. In: Proc. of the 31st Annual ACM/IEEE Symp. on Logic in Computer Science. 2016. 31-45.
Kemeny JG, Snell JL. Finite Markov Chains. Princeton: D. Van Nostrand, 1960.
Kulkarni VG. Modeling and Analysis of Stochastic Systems. New York: Chapman & Hall, 1995.
Bellman R. A Markovian decision process. Journal of Mathematics and Mechanics, 1957, 6(5): 679-684.
Vardi MY. Automatic verification of probabilistic concurrent finite state programs. In: Proc. of the 26th Annual Symp. on Foundations of Computer Science. 1985. 327-338.
Anderson WJ. Continuous-time Markov Chains: An Applications-oriented Approach. New York: Springer Science & Business Media, 2012.
Hart S, Sharir M, Pnueli A. Termination of probabilistic concurrent program. ACM Trans. on Programming Languages and Systems (TOPLAS), 1983, 5(3): 356-380.
Vardi MY, Wolper P. Reasoning about infinite computations. Information and Computation, 1994, 115(1): 1-37.
Klein J, Baier C. Experiments with deterministic
Hansson H, Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994, 6(5): 512-535.
Aziz A, Singhal V, Balarin F, Brayton RK, Sangiovanni-Vincentelli AL. It usually works: The temporal logic of stochastic systems. In: Proc. of the Int'l Conf. on Computer Aided Verification. 1995. 155-165.
Baier C, Katoen JP, Hermanns H, Wolf V. Comparative branching-time semantics for Markov chains. Information and Computation, 2005, 200(2): 149-214.
Aziz A, Sanwal K, Singhal V, Brayton R. Model-checking continuous-time Markov chains. ACM Trans. on Computational Logic (TOCL), 2000, 1(1): 162-170.
Baier C, Haverkort B, Hermanns H, Katoen JP. Model-checking algorithms for continuous-time Markov chains. IEEE Trans. on Software Engineering, 2003, 29(6): 524-541.
Katoen JP, Song L, Zhang L. Probably safe or live. In: Proc. of the Joint Meeting of the 23rd EACSL Annual Conf. on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symp. on Logic in Computer Science (LICS). 2014. 1-10.
Kwiatkowska M, Norman G, Parker D. PRISM 4.0: Verification of probabilistic real-time systems. In: Proc. of the Int'l Conf. on Computer Aided Verification. 2011. 585-591.
Baier C, Clarke EM, Hartonas-Garmhausen V, Kwiatkowska M, Ryan M. Symbolic model checking for probabilistic processes. In: Proc. of the Int'l Colloquium on Automata, Languages, and Programming. 1997. 430-440.
Fruth M. Probabilistic model checking of contention resolution in the IEEE 802.15. 4 low-rate wireless personal area network protocol. In: Proc. of the 2nd Int'l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006). IEEE, 2006. 290-297.
Kwiatkowska M, Norman G, Parker D. Probabilistic verification of Herman's self-stabilisation algorithm. Formal Aspects of Computing, 2012, 24(4): 661-670.
Barbot B, Kwiatkowska M. On quantitative modelling and verification of DNA walker circuits using stochastic Petri nets. In: Proc. of the Int'l Conf. on Applications and Theory of Petri Nets and Concurrency. Cham: Springer, 2015. 1-32.
Dehnert C, Junges S, Katoen JP,
Hahn EM, Li Y, Schewe S,
Katoen JP, Khattri M, Zapreevt IS. A Markov reward model checker. In: Proc. of the 2nd Int'l Conf. on the Quantitative Evaluation of Systems (QEST 2005). 2005. 243-244.
Baier C, Ciesinski F. Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: Proc. of the 3rd Int'l Conf. on the Quantitative Evaluation of Systems (QEST 2006). 2006. 131-132.
Bozzano M, Cimatti A, Katoen JP,
Esteve MA, Katoen JP, Nguyen VY,
Kaminski BL, Katoen JP, Matheja C, Olmedo F. Weakest precondition reasoning for expected run-times of probabilistic programs. In: Proc. of the European Symp. on Programming. 2016. 364-389.
McIver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure termination. In: Proc. of the Symp. on Principles of Programming Languages (POPL 2018). 2018. 33: 1-33: 28.
Gretz F, Katoen JP, McIver A. PRINSYS-On a quest for probabilistic loop invariants. In: Proc. of the 10th Int'l Conf. on Quantitative Evaluation of Systems (QEST 2013). 2013. 172-187.
Ericson CA. Fault tree analysis-A history. In: Proc. of the 17th Int'l System Safety Conf. 1999. 1-9.
Vesely WE, Goldberg FF, Roberts NH, Haasl DF. FaultTree Handbook. Washington: Nuclear Regulatory Commission, 1981.
Raiteri DC, Franceschinis G, Iacono M, Vittorini V. Repairable fault tree for the automatic evaluation of repair policies. In: Proc. of the Dependable Systems and Networks. 2004. 659-668.
Coudert O, Madre JC. Fault tree analysis: 1020 prime implicants and beyond. In: Proc. of the Reliability and Maintainability Symp. 1993. 240-245.
Rauzy AB. New algorithms for fault tree analysis. Reliability Engineering and System Safety, 1993, 40(3): 203-211.
Remenyte-Prescott R, Andrews J. An enhanced component connection method for conversion of fault trees to binary decision diagrams. Reliability Engineering and System Safety, 2008, 93(10): 1543-1550.
Barlow RE, Proschan F. Statistical Theory of Reliability and Life Testing. New York: Holt, Rinehartand Winston, 1975.
Rao KD, Gopika V. Dynamic fault tree analysis using Monte Carlo simulation in probabilistic safety assessment. Reliability Engineering & System Safety, 2009, 94(4): 872-883.
https://www.di.unipmn.it/en/publications-en/technical-reports-en.html]]>
Dugan JB, Bavuso SJ, Boyd MA. Fault trees and sequence dependencies. In: Proc. of the Annual Reliability and Maintainability Symp. IEEE, 1990. 286-293.
Ruijters E, Stoelinga M. Fault tree analysis: A survey of the state-of-the-art in modeling, analysis and tools. Computer Science Review, 2015, 15-16: 29-62.
Tanaka H, Fan L, Lai F, Toguchi K. Fault-tree analysis by fuzzy probability. IEEE Trans. on Reliability, 1983, 32(5): 453-457.
Bobbio A, Codetta-Raiteri D. Parametric fault trees with dynamic gates and repair boxes. In: Proc. of the Reliability and Maintainability Symp. (RAMS). IEEE, 2004. 459-465.
Boudali H, Crouzen P, Stoelinga M. CORAL-A tool for compositional reliability and availability analysis. In: Proc. of the Workshop on the CAV. 2007.
Codetta-Raiteri D. The conversion of dynamic fault trees to stochastic Petri nets, as a case of graph transformation. In: Proc. of the PNGT. 2005. 45-60.
Boudali H, Nijmeijer AP, Stoelinga MIA. DFTSim: A simulation tool for extended dynamic fault trees. In: Proc. of the Spring Simulation Multiconference. 2009. 1-8.
Hasan O, Ahmed W, Tahar S, Hamdi MS. Reliability block diagrams based analysis: A survey. AIP Conf. Proc., 2015, 1648(1). [doi:10.1063/1.4913184]
Distefano S, Puliafito A. Dynamic reliability block diagrams: Overview of a methodology. In: Proc. of the European Safety and Reliability. 2007. 1059-1068.
Smith G. The Object-Z Specification Language. New York: Springer. 2012.
Ahmed W, Hasan O, Tahar S. Formalization of reliability block diagrams in higher-order logic. Journal of Applied Logic, 2016, 18: 19-41.
Yassmeen E, Osman H. A formally verified algebraic approach for dynamic reliability block diagrams. In: Proc. of the ICFEM. 2019. 253-269.
https://hol-theorem-prover.org/]]>
Henzinger TA. The theory of hybrid automata. In: Proc. of the Logic in Computer Science. 1996. 278-292.
Platzer A. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 2008, 41(2): 143-189.
He J. From CSP to hybrid systems. In: Proc. of the a Classical Mind: Essays in Honour of C.A.R. Hoare. 1994. 171-189.
Zhou C, Wang J, Ravn A. A formal description of hybrid systems. In: Proc. of the Hybrid Systems. 1995. 511-530.
http://www.mathworks.com/help/pdf_doc/simulink/sl_using.pdf]]>
Modelica Association. Modelica-A Unified Object-oriented Language for Systems Modeling-Version 3.3 Revision 1. Standard Specification, 2014.
Koymans R. Specifying real-time properties with metric temporal logic. Real Time System, 1990, 2(4): 255-299.
Alur R, Feder T, Henzinger T. The benefits of relaxing punctuality. Journal of the ACM (JACM), 1996, 43(1): 116-146.
Maler O, Dickovic D. Monitoring temporal properties of continuous signals. In: Proc. of the FORMATS. 2004. 152-166.
Maler O, Dickovic D, Pnueli A. Checking temporal properties of discrete, timed and continuous behaviors. Pillars of Computer Science, 2008. 475-505.
Fainekos GE, Pappas GJ. Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science, 2009, 410(42): 4262-4291.
Donzé A, Maler O. Robust satisfaction of temporal logic over real-valued signals. In: Proc. of the FORMATS. 2010. 92-106.
Roehm H, Oehlerking J, Heinz T, Althoff M. STL model checking of continuous and hybrid systems. In: Proc. of the ATVA. 2016. 412-427.
Donzé A, Ferrère T, Maler O. Efficient robust monitoring for STL. In: Proc. of the CAV. 2013. 264-279.
Deshmukh JV, Donzé A, Ghosh S, Jin X, Juniwal G, Seshia SA. Robust online monitoring of signal temporal logic. Formal Methods System Design, 2017, 51(1): 5-30.
Makino K, Berz M. Rigorous integration of flows and ODEs using Taylor models. In: Proc. of the SNC. 2009. 79-84.
Chen X, Ábrahám E, Sankaranarayanan S. Taylor model flowpipe construction for non-linear hybrid systems. In: Proc. of the RTSS. 2012. 183-192.
Nedialkov NS, Jackson KR, Corliss GF. Validated solutions of initial value problems for ordinary differential equations. Applied Mathematics and Computation, 1999, 105(1): 21-68.
Althoff M, Stursberg O, Buss M. Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. In: Proc. of the CDC. 2008. 4042-4048.
Henrion D, Korda M. Convex computation of the region of attraction of polynomial control systems. IEEE Trans. on Automatic Control, 2014, 59(2): 297-312.
Fan C, Qi B, Mitra S, Viswanathan M. DryVR: Data-driven verification and compositional reasoning for automotive systems. In: Proc. of the CAV. 2017. 441-461.
Xue B, Zhang M, Easwaran A, Li Q. PAC model checking of black-box continuous-time dynamical systems. IEEE Trans. on Computer-aided Design of Integrated Circuits and Systems, 2020. 39(11): 3944-3955.
Goubault E, Mullier O, Putot S, Kieffer M. Inner approximated reachability analysis. In: Proc. of the HSCC. 2014. 163-172.
Goubault E, Putot S. Forward inner-approximated reachability of non-linear continuous systems. In Proc. of the HSCC. 2017. 1-10.
Xue B, She Z, Easwaran A. Under-approximating backward reachable sets by polytopes. In: Proc. of the CAV. 2016. 457-476.
Xue B, Fränzle M, Zhan N. Inner-approximating reachable sets for polynomial systems with time-varying uncertainties. IEEE Trans. on Automatic Control, 2020, 65(4): 1468-1483.
Xue B, Zhan N, Fränzle M. Inner-approximating reach-avoid sets for discrete-time polynomial systems. In: Proc. of the CDC. 2020. 867-873.
Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O. SpaceEx: Scalable verification of hybrid systems. In: Proc. of the CAV. 2011. 379-395.
Chen X, Ábrahám E, Sankaranarayanan S. Flow*: An analyzer for non-linear hybrid systems. In: Proc. of the CAV. 2013. 258-263.
Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. JuliaReach: A toolbox for set-based reachability. In: Proc. of the HSCC. 2019. 39-44.
Althoff M. An introduction to CORA 2015. In: Proc. of the ARCH@CPSWeek. 2015. 120-151.
Bu L, Li Y, Wang L, Chen X, Li X. BACH 2: Bounded reachability checker for compositional linear hybrid systems. In: Proc. of the DATE. 2010. 1512-1517.
Fan C, Qi B, Mitra S, Viswanathan M, Duggirala PS. Automatic reachability analysis for nonlinear hybrid models with C2E2. In: Proc. of the CAV. 2016. 531-538.
Donzé A. Breach, a toolbox for verification andparameter synthesis of hybrid systems. In: Proc. of the CAV. 2010.167-170.
Fulton N, Mitsch S, Quesel J, Völp M, Platzer A. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In: Proc. of the CADE. 2015. 527-538.
Wang S, Zhan N, Zou L. An improved HHL prover: An interactive theorem prover for hybrid systems. In: Proc. of the ICFEM. 2015. 382-399.
http://spaceex.imag.fr/sites/default/files/introduction_to_spaceex_0.pdf]]>
Johnson T, Green J, Mitra S, Dudley R, Erwin RS. Satellite rendezvous and conjunction avoidance: Case studies in verification of nonlinear hybrid systems. In: Proc. of the FM. 2012. 252-266.
Minopoli S, Frehse G. SL2SX translator: From Simulink to SpaceEx models. In: Proc. of the HSCC. 2016. 93-98.
Duggirala PS, Fan C, Mitra S, Viswanathan M. Meeting a powertrain verification challenge. In: Proc. of the CAV. 2015. 536-543.
Platzer A, Quesel JD. Logical verification and systematic parametric analysis in train control. In: Proc. of the HSCC. 2008. 646-649.
Platzer A, Quesel JD. European train control system: A case study in formal verification. In: Proc. of the ICFEM. 2009. 246-265.
Platzer A. Verification of cyberphysical transportation systems. IEEE Intelligent Systems, 2009, 24(4): 10-13.
Loos S, Renshaw DW, Platzer A. Formal verification of distributed aircraft controllers. In: Proc. of the HSCC. 2013. 125-130.
Kouskoulas Y, Renshaw D, Platzer A. Certifying the safe design of a virtual fixture control algorithm for a surgical robot. In: Proc. of the HSCC. 2013. 263-272.
Mitsch S, Ghorbal K, Vogelbacher D. Formal verification of obstacle avoidance and navigation of ground robots. CoRR abs/1605. 00604, 2016.
Herber P, Adelt J, Liebrenz T. Formal verification of intelligent cyber-physical systems with the interactive theorem prover KeYmaera X. In: Proc. of the Software Engineering (Satellite Events). 2021.
Staroletov S. Automatic proving of stability of the cyber-physical systems in the sense of Lyapunov with KeYmaera. In: Proc. of the FRUCT. 2021. 431-438.
Zhao H, Yang M, Zhan N, Gu B, Zou L, Chen Y. Formal verification of a descent guidance control program of a lunar lander. In: Proc. of the FM. 2014. 733-748.
Ahmad E, Dong YW, Larson BR, Lü JD, Tang T, Zhan NJ. Behavior modeling and verification of movement authority scenario of Chinese train control system using AADL. Science China Information Sciences, 2015, 58(11): 1-20.
Bradley A. SAT-based model checking without unrolling. In: Proc. of the VMCAI. 2011. 70-87.
Eén N, Mishchenko A, Brayton R. Efficient implementation of property directed reachability. In: Proc. of the FMCAD. 2011. 125-134.
Biere A, Heule M, van Maaren H, Walsh T. Handbook of Satisfiability. IOS Press, 2009.
Biere A, Heljanko K, Wieringa S. AIGER 1.9 and beyond. Technical Report, 11/2, Institute for Formal Models and Verification, Johannes Kepler University, 2011.
Niemetz A, Preiner M, Wolf C, Biere A. Btor2, BtorMC and Boolector 3.0. In: Proc. of the CAV. 2018. 587-595.
IEEE Standard for Property Specification Language (PSL), Annex B. IEEE Std 1850TM-2010, 2010.
IEEE Standard for SystemVerilog-Unified Hardware Design, Specification, and Verification Language, Annex F. IEEE Std 1800TM-2009, 2009.
Sheeran M, Singh S, Stålmarck G. Checking safety properties using induction and a SAT-solver. In: Proc. of the FMCAD. 2000. 108-125.
Cimatti A, Griggio A. Software model checking via IC3. In: Proc. of the CAV. 2012. 277-293.
Hoder K, Bjørner N. Generalized property directed reachability. In: Proc. of the SAT. 2012. 157-171.
Cimatti A, Griggio A, Mover S, Tonetta S. Infinite-state invariant checking with IC3 and predicate abstraction. Formal Methods in System Design, 2016, 49(3): 190-218.
Goel A, Sakallah K. Model checking of verilog RTL using IC3 with syntax-guided abstraction. In: Proc. of the NFM. 2019. 166-185.
Li J, Zhu S, Zhang Y, Pu G, Vardi M. Safety model checking with complementary approximations. In: Proc. of the ICCAD. 2017. 95-100.
Zhang H, Gupta A, Malik S. Syntax-guided synthesis for lemma generation in hardware model checking. In: Proc. of the VMCAI. 2021. 325-349.
Seger CJ, Bryant R. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 1995, 6(2): 147-189.
Melham T. Higher order logic and hardware verification. Cambridge Tracts in Theoretical Computer Science 31. Cambridge University Press, 1993.
Goel A, Sakallah K. AVR: Abstractly verifying reachability. In: Proc. of the TACAS. 2020. 413-422.
Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S. The nuXmv symbolic model checker. In: Proc. of the CAV. 2014. 334-342.
Mann M, Irfan A, Lonsing F, Yang Y, Zhang H, Brown K, Gupta A, Barrett C. Pono: A flexible and extensible SMT-based model checker. In: Proc. of the CAV. 2021. 461-474.
Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A. NuSMV 2: An open source tool for symbolic model checking. In: Proc. of the CAV. 2002. 359-364.
Brayton R, Mishchenko A. ABC: an academic industrial-strength verification tool. In: Proc. of the CAV. 2010. 24-40.
Seger CJH, Jones RB, O'Leary JW, Melham T, Aagaard MD, Barrett C, Syme D. An industrially effective environment for formal hardware verification. IEEE Trans. on Computer-aided Design of Integrated Circuits and Systems, 2005, 24(9): 1381-1405.
O'Leary JW, Kaivola R, Melham T. Relational STE and theorem proving for formal verification of industrial circuit designs. In: Proc. of the FMCAD. 2013. 97-104.
https://satoss.uni.lu/members/patrick/1stsxxm.pdf]]>
Dolev D, Yao ACC. On the security of public key protocols. In: Proc. of the FOCS. 1981. 350-357.
LaMacchia B, Lauter K, Mityagin A. Stronger security of authenticated key exchange. In: Proc. of the Provable Security. 2007. 1-16.
Lowe G. A hierarchy of authentication specifications. In: Proc. of the CSFW. 1997. 31-44.
Lowe G. Casper: A compiler for the analysis of security protocols. Journal of Computer Security, 1998, 6(1-2): 53-84.
Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software Concepts Tools, 1996, 17(3): 93-102.
Schmidt B, Meier S, Cremers C, Basin D. Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Proc. of the CSF. 2012. 78-94.
Meier S, Schmidt B, Cremers C, Basin D. The TAMARIN prover for the symbolic analysis of security protocols. In: Proc. of the CAV. 2013. 696-701.
Blanchet B. An efficient cryptographic protocol verifier based on Prolog rules. In: Proc. of the CSFW. 2001. 82-96.
Chadha R, Cheval V, Ciobaca S, Kremer S. Automated verification of equivalence properties of cryptographic protocols. Trans. on Computational Logic, 2016, 17(4): Article 23.
Cremers C, Horvat M, Hoyland J, Scott S, Merwe T. A comprehensive symbolic analysis of TLS 1.3. In: Proc. of the CCS. 2017. 1773-1788.
Basin D, Dreier J, Hirschi L, Radomirovic S, Sasse R, Stettler V. A formal analysis of 5G authentication. In: Proc. of the CCS. 2018. 1383-1396.
Kunnemann R, Steel G. YubiSecure?Formal security analysis results for theYubiKey and YubiHSM. In: Proc. of the STM. 2012. 257-272.
Abadi M, Blanchet B, Fournet C. The applied pi calculus: Mobile values, new names, and secure communication. Journal of the ACM (JACM), 2018, 65(1): Article No. 1.
Woo T, Lam S. A semantic model for authentication protocols. In: Proc. of the IEEE Symp. on Security and Privacy. 1993. 178-194.
Bruno B. Automatic verification of correspondences for security protocols. Journal of Computer Security, 2009, 17(4): 363-434.
Bruno B, Martín A, Cédric F. Automated verification of selected equivalences for security protocols. The Journal of Logic and Algebraic Programming, 2008, 75(1): 3-51.
Abadi M, Blanchet B, Fournet C. Just fast keying in the pi calculus. ACM TISSEC, 2007, 10(3): 1-59.
Aiello W, Bellovin SM, Blaze M, Canetti R, Ioannidis J, Keromytis K, Reingold O. Just fast keying: Key agreement in a hostile Internet. ACM TISSEC, 2004, 7(2): 242-273.
Abadi M, Blanchet B. Computer-assisted verification of a protocol for certified email. Science of Computer Programming, 2005, 58(1-2): 3-27.
Delaune S, Kremer S, Ryan M. Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security, 2009, 17(4): 435-487.
Backes M, Hritcu C, Maffei M. Automated verification of remote electronic voting protocols in the applied pi-calculus. In: Proc. of the CSF. 2008. 195-209.
Kremer S, Ryan M. Analysis of an electronic voting protocol in the applied pi calculus. In: Proc. of the ESOP. 2005. 186-200.
Barthe G, Dupressoir F, Grégoire B, Kunz C, Schmidt B, Strub PY. Easycrypt: A tutorial. In: Proc. of the FOSAD. 2013. 146-166.
Barthe G, Grégoire B, Béguelin SZ. Formal certification of code-based cryptographic proofs. In: Proc. of the POPL. 2009. 90-101.
Rushby J. Noninterference, transitivity, and channel-control security policies. Technical Report, CSL-92-02, SRI Int'l, 1992.
Oheimb DV. Information flow control revisited: Noninfluence=Noninterference+nonleakage. In: Proc. of the ESORICS. 2004. 225-243.
Peter Y, Ryan A. Mathematical models of computer security. In: Proc. of the FOSAD. 2000. 1-62.
Focardi R, Gorrieri R. Classification of security properties (part I: Information flow). In: Proc. of the FOSAD. 2000. 331-396.
Roscoe AW, Huang J. Checking noninterference in timed CSP. Formal Aspects of Computing, 2013, 25(1): 3-35.
Volpano DM, Irvine CE, Smith G. A sound type system for secure flow analysis. Journal of Computer Security, 1996, 4(2/3): 167-188.
Zhang DF, Askarov A, Myers AC. Language-based control and mitigation of timing channels. In: Proc. of the PLDI. 2012. 99-110.
Rajani V, Garg D. On the expressiveness and semantics of information flow types. Journal of Computer Security, 2020, 28(1): 129-156.
Zdancewic SA. Programming languages for information security[Ph. D. Thesis]. Cornell University, 2002.
Eggert S, Schnoor H, Wilke T. Dynamic noninterference: Consistent policies, characterizations and verification. CoRR, abs/1208. 5580, 2012.
Eggert S, Schnoor H, Wilke T. Noninterference with local policies. In: Proc. of the MFCS. 2013. 337-348.
Hadj-Alouane NB, Lafrance S, Lin F, Mullins J, Yeddes MM. On the verification of intransitive noninterference in multilevel security. IEEE Trans. on Systems, Man and Cybernetics, Part B, 2005, 35(5): 948-958.
Eggert S, Meyden RVD, Schnoor H, Wilke T. The complexity of intransitive noninterference. In: Proc. of the IEEE Symp. on Security and Privacy. 2011. 196-211.
Murray TC, Matichuk D, Brassil M, Gammie P, Bourke T, Seefried S, Lewis C, Gao X, Klein G. sel4: From general purpose to a proof of information flow enforcement. In: Proc. of the IEEE Symp. on Security and Privacy. 2013. 415-429.
Zhao YW, Sanán D, Zhang FY, Liu Y. Refinement-based specification and security analysis of separation kernels. IEEE Trans. on Dependable and Secure Computing, 209, 16(1): 127-141.
Saboori A, Hadjicostis CN. Verification of infinite-step opacity and complexity considerations. IEEE Trans. on Automatic Control, 2012, 57(5): 1265-1269.
Saboori A, Hadjicostis CN. Verification of initial-state opacity in security applications of discrete event systems. Information Sciences, 2013, 246: 115-132.
Saboori A, Hadjicostis CN. Verification of
Saboori A, Hadjicostis CN. Opacity-enforcing supervisory strategies via state estimator constructions. IEEE Trans. on Automatic Control, 2012, 57(5): 1155-1165.
Keroglou C, Hadjicostis C. Initial state opacity in stochastic DES. In: Proc. of the ETFA. 2013. 1-8.
Berard B, Chatterjee K, Sznajder N. Probabilistic opacity for Markov decision processes. Information Processing Letters, 2015, 115(1): 52-59.
Berard B, Mullins J, Sassolas M. Quantifying opacity. In: Proc. of the QEST. 2010. 263-272.
Bryans J, Kounty M, Ryan P. Modelling opacity using Petri nets. Electronic Notes in Theoretical Computer Science, 2005, 121: 101-115.
Tong Y, Li Z, Seatzu C, Giua A. Verification of state-based opacity using petri nets. IEEE Trans. on Automatic Control, 2017, 62(6): 2823-2837.
Cassez F. The dark side of timed opacity. In: Proc. of the ISA. 2009. 21-30.
Wang LT, Zhan NJ, An J. The opacity of real-time automata. IEEE Trans. on Computer-aided Design of Integrated Circuits and Systems, 2018, 37(11): 2845-2856.
Deng MN, Wuyts K, Scandariato R, Preneel B, Joosen W. A privacy threat analysis framework: Supporting the elicitation and fulfillment of privacy requirements. Requirements Engineering, 2011, 16(1): 3-32.
Bohli JM, Pashalidis A. Relations among privacy notions. ACM Trans. on Information and System Security, 2011, 14(1): Article No. 4.
Dong NP, Jonker H, Pang J. Enforcing privacy in the presence of others: notions, formalisations and relations. In: Proc. of the ESORICS. 2013. 499-516.
Clarkson MR, Schneider F. Hyperproperties. Journal of Computer Security, 2010, 18(6): 1157-1210.
Clarkson MR, Finkbeiner B, Koleini M, Micinski KK, Rabe MN, Sánchez C. Temporal logics for hyperproperties. In: Proc. of the POST. 2014. 265-284.
Finkbeiner B, Hahn C. Deciding hyperproperties. In: Proc. of the CONCUR. 2016. Article No. 13.
Finkbeiner B, Hahn C, Stenger M. EAHyper: Satisfiability, implication, and equivalence checking of hyperproperties. In: Proc. of the CAV. 2017. 564-570.
Huang X, Kroening D, Ruan W, Sharp J, Sun Y, Thamo E, Wu M, Yi X. A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability. Computer Science Review, 2020, 37: Article No. 100270.
Seshia SA, Desai A, Dreossi T, Fremont D, Ghosh S, Kim E, Shivakumar S, Vazquez-Chanlatte M, Yue X. Formal specification for deep neural networks. In: Proc. of the ATVA. 2018. 20-34.
Dreossi T, Jha S, Seshia SA. Semantic adversarial deep learning. In: Proc. of the CAV. 2018. 3-26.
Katz G, Barrett C, Dill DL, Julian K, Kochenderfer MJ. Reluplex: An efficient SMT solver for verifying deep neural networks. In: Proc. of the CAV. 2017. 97-117.
Ehlers R. Formal verification of piece-wise linear feed-forward neural networks. In: Proc. of the ATVA. 2017. 269-286.
Wang S, Pei K, Whitehouse J, Yang J, Jana S. Formal security analysis of neural networks using symbolic intervals. In: Proc. of the USENIX Security Symp. 2018. 1599-1614.
Singh G, Gehr T, Mirman M, Puschel M, Vechev MT. Fast and effective robustness certification. In: Proc. of the NeurIPS. 2018. 10825-10836.
Singh G, Gehr T, Puschel M, Vechev MT. An abstract domain for certifying neural networks. In: Proc. of the ACM Programming Languages (POPL). 2019. Article No. 41.
Weng TW, Zhang H, Chen H, Song Z, Hsieh CJ, Daniel L, Boning DS, Dhillon IS. Towards fast computation of certified robustness for ReLU networks. In: Proc. of the ICML. 2018. 5273-5282.
Zhang H, Weng TW, Chen PY, Hsieh CJ, Daniel L. Efficient neural network robustness certification with general activation functions. In: Proc. of the NeurIPS. 2018. 4944-4953.
Dreossi T, Ghosh S, Sangiovanni-Vincentelli AL, Seshia SA. A formalization of robustness for deep neural networks. In: Proc. of the AAAI Spring Symp. Workshop on Verification of Neural Networks (VNN). 2019.
Dutta S, Jha S, Sankaranarayanan S, Tiwari A. Output range analysis for deep feedforward neural networks. In: Proc. of the NFM. 2018. 121-138.
Ruan W, Huang X, Kwiatkowska M. Reachability analysis of deep neural networks with provable guarantees. In: Proc. of the IJCAI. 2018. 2651-2659.
Li J, Liu J, Yang P, Chen L, Huang X, Zhang L. Analyzing deep neural networks with symbolic propagation: Towards higher precision and faster verification. In: Proc. of the SAS. 2019. 296-319.
Yang X, Yamaguchi T, Tran HD, Hoxha B, Johnson TT, Prokhorov D. Reachability analysis of deep ReLU neural networks using facet-vertex incidence. In: Proc. of the HSCC. 2021. Article No. 18.
Xue B, Liu Y, Ma L, Zhang X, Sun M, Xie X. Safe inputs approximation for black-box systems. In: Proc. of the ICECCS. 2019. 180-189.
Dreossi T, Donzé A, Seshia SA. Compositional falsification of cyber-physical systems with machine learning components. Journal of Automated Reasoning, 2019, 63(4): 1031-1053.
Dreossi T, Fremont DJ, Ghosh S, Kim E, Ravanbakhsh H, Vazquez-Chanlatte M, Seshia SA. VerifAI: A toolkit for the formal design and analysis of artificial intelligence-based systems. In: Proc. of the CAV. 2019. 432-442.
Fremont DJ, Chiu J, Margineantu DD, Osipychev D, Seshia SA. Formal analysis and redesign of a neural network-based aircraft taxiing system with VerifAI. In: Proc. of the CAV. 2020. 122-134.
Huang C, Fan J, Li W, Chen X, Zhu Q. ReachNN: Reachability analysis of neural-network controlled systems. ACM Trans. on Embedded Computing Systems, 2019, 18(5s): Article No. 106.