我们在这里要验证的不是全部的安全性，而是正则安全性(regular safety properties)，它是安全性的一个子集，当然我们在定义的时候会使用到一些概念，例如正则表达式什么的，可以翻翻前面的还有计算理论和自动机理论学习笔记（要用到的知识有状态机，正则表达式，正则语言等等）

正则安全性

定义

如果PsafeP_{safe}Psafe是正则安全性，那么当且仅当BadPref(Psafe)BadPref(P_{safe})BadPref(Psafe)是正则语言

根据自动机理论，这个定义也等价于如果PsafeP_{safe}Psafe是正则安全性，那么当且仅当在2AP2^{AP}2AP上的有限自动机可以接受BadPref(Psafe)BadPref(P_{safe})BadPref(Psafe)

正则安全性的例子

之前我们提到过一个红绿灯的例子

each red phase should be immediately preceded by a yellow phase
只有在黄灯亮了之后红灯才能亮

下图展示了一个可以接受坏前缀的确定性的有限自动机，所以该安全性属于正则安全性

判断：每个不变性都是正则安全性
答案：正确
由前面的章节我们知道，不变性都具有一个不变条件Φ，如果找到一个状态是¬Φ\lnot Φ¬Φ，那么就说明存在坏前缀，也就不满足不变性，基于此，我们可以构建出对应的自动机来接受坏前缀

这个例子再具体一点，就用两个进程互斥的模型，此时Φ=¬crit1∨¬crit2\Phi=\lnot crit1\vee \lnot crit2Φ=¬crit1∨¬crit2，而¬Φ\lnot \Phi¬Φ就是Φ=crit1∧crit2\Phi=crit1\wedge crit2Φ=crit1∧crit2，直接代入上图就生成了一个自动机

回到LT属性的分类图，这里讲的正则属性，它是安全属性的一部分，所以也叫正则安全性，它包含了不变性以及安全性的一部分，还有一部分安全性不是正则的，如图中蓝色部分所示

验证正则安全性

现在我们有：

由TS建模的模型
正则安全属性P(将其表示为一个接受坏前缀的NFA)

要解决的问题是：

TS⊨PTS\vDash PTS⊨P？

这个问题与另一个问题“如何确定一个语言包含于一个NFA”类似，我们可以基于以下的做法：

构建一个非确定性自动机A，使它能够接受坏前缀的集合
构建一个新的转换系统TS’，使它结合了原有TS的以及A的行为
在新的转换系统TS‘上做不变性的检查

所以我们将验证TS⊨PTS\vDash PTS⊨P转换为验证T⊗A⊨never final stateT\otimes A\vDash \text{never final state}T⊗A⊨never final state

在上面我们看到，对于一个接受坏前缀的自动机来说，如果达到final state就是终止状态，就说明输入是一个坏前缀，而这里的never final state就是要求新生成的TS’永远不会到达终止状态。

接下来介绍符号⊗\otimes⊗(同步积)的运算，以描述生成新TS的过程

不存在终止状态的TS=(S,Act,→,I,AP,L)TS=(S, Act, →,I,AP, L)TS=(S,Act,→,I,AP,L)，以及一个非确定性自动机A=(Q,Σ,δ,Q0,F)A = (Q, Σ, δ, Q_{0}, F)A=(Q,Σ,δ,Q0,F)

product-TS：T⊗A=(S′,Act,→′,S0′,AP′,L′)T\otimes A= (S',Act,→', S_{0}', AP', L')T⊗A=(S′,Act,→′,S0′,AP′,L′)
其中
S′=S×QS'=S \times QS′=S×Q

所以product-TS中的状态表示为<S,Q>

Act仍然不变

最重要的部分就是这个转换→’,它表示为:
s→αs′∧q→L(s′)q′<s,q>→′<s′,q′>\dfrac{s\xrightarrow{α}s'\wedge q\xrightarrow{L(s')}q'}{<s,q>\rightarrow'<s',q'>} <s,q>→′<s′,q′>sαs′∧qL(s′)q′

如果s通过动作α转换s’，并且自动机从q接受L(s’)转换为q’，那么就在生成的TS上表示一个转换<s,q>→′<s′,q′><s,q>\rightarrow'<s',q'><s,q>→′<s′,q′>

初始状态S0′={<s0,q>∣s0∈S0,q0→L(s0)q}S_{0}'=\{<s_{0},q>|s_{0}∈S_{0},q_{0}\xrightarrow{L(s_{0})}q\}S0′={<s0,q>∣s0∈S0,q0L(s0)q}，初始状态要特别注意，这里不是<s0,q0><s_{0},q_{0}><s0,q0>，第二个q表示的是自动机中，初始状态q0q_{0}q0通过L(s0)L(s_{0})L(s0)转换后的状态集合

原子命题集合 AP’=Q

标签函数 L’(<s,q>)={q}

果然最容易理解的方式还是举例子啦，有这么一个红绿灯系统，建模为TS

至于这个red\yellow就直接当它是个状态好了，可能德国的红绿灯和我们这边不一样吧

在SyellowS_{yellow}Syellow状态下标签是{yellow}，SredS_{red}Sred状态下标签是{red}，Sred∣yellowS_{red|yellow}Sred∣yellow状态下标签是∅\varnothing∅，SgreenS_{green}Sgreen状态下标签也是∅\varnothing∅，所以AP={red,yellow}

它有一个性质P"只有在黄灯亮了之后红灯才能亮"，将这个性质转化为一个自动机（和上面的那张图一样的）

生成的新TS，它的状态S’有3x4=12个，类似<sgreen,q0>,<sgreen,q1>,<sgreen,qF>...<s_{green},q_{0}>,<s_{green},q_{1}>,<s_{green},q_{F}>...<sgreen,q0>,<sgreen,q1>,<sgreen,qF>...

然后是初始状态S0′S_{0}'S0′，看到L(s0)=L(sgreen)=∅L(s_{0})=L(s_{green})=\varnothingL(s0)=L(sgreen)=∅，看到q0这个地方，看看它接受∅\varnothing∅会变成什么？这个¬red∧¬yellow\lnot red\wedge \lnot yellow¬red∧¬yellow代表的就是∅\varnothing∅，所以接受∅\varnothing∅仍然是q0q_{0}q0，于是初始状态S0′=<sgreen,q0>S_{0}'=<s_{green},q_{0}>S0′=<sgreen,q0>

到了转换这边就有点麻烦了，这里的动作我们不关注，暂且不管Act了。

sgreens_{green}sgreen经过动作转变为syellows_{yellow}syellow，那么看看q0q_{0}q0接受L(syellow)L(s_{yellow})L(syellow)会变成什么？此时的L(syellow)L(s_{yellow})L(syellow)值为{yellow}，q0q_{0}q0接受{yellow}之后转变成了q1q_{1}q1，所以这样就是一条转换关系<sgreen,q0>→<syellow,q1><s_{green},q_{0}>\rightarrow <s_{yellow},q_{1}><sgreen,q0>→<syellow,q1>

再来看一条转换，syellows_{yellow}syellow经过动作转变为sreds_{red}sred，L(sred)L(s_{red})L(sred)的值为{red}，q1q_{1}q1接受{red}转换为q0q_{0}q0，所以这又是一条新的转换<syellow,q1>→<sred,q0><s_{yellow},q_{1}>\rightarrow<s_{red},q_{0}><syellow,q1>→<sred,q0>

按照上面的方法把每一个转换都验证一遍，得到了最终的新的TS

AP′=Q={q0,q1,qF}AP'=Q=\{q_{0},q_{1},q_{F}\}AP′=Q={q0,q1,qF}

L’标签函数最简单了，就留下自动机的状态就行了L′(<sgreen,q0>)=q0,L′(<syellow,q1>)=q1,L′(<sred,q0>)=q0,L′(<sred∣yellow,q0>)=q0L'(<s_{green},q_{0}>)=q_{0},L'(<s_{yellow},q_{1}>)=q_{1},L'(<s_{red},q_{0}>)=q_{0},L'(<s_{red|yellow},q_{0}>)=q_{0}L′(<sgreen,q0>)=q0,L′(<syellow,q1>)=q1,L′(<sred,q0>)=q0,L′(<sred∣yellow,q0>)=q0

构建完新的TS后，我们就要进行最后一步不变性检查了，上面说过要求新的TS无法到达终止状态，所以要检查的不变性Φ=¬qF\Phi=\lnot q_{F}Φ=¬qF，我们看一下上面那张图，发现状态里面有q0,q1q_{0},q_{1}q0,q1并没有qF{q_{F}}qF，所以原系统TS是满足性质P的。

如果用算法来进行的话就和前面不变性检验相似，使用DFS或者BFS来搜索状态。

总结

这里我们主要介绍有了TS模型和正则安全性P之后，如何检测TS模型满足正则安全性

对于正则安全性的模型检测，下面几种陈述都是等价的

T⊨PT\vDash PT⊨P
Tracesfin(TS)∩L(A)=∅Traces_{fin}(TS)\cap L(A)=\varnothingTracesfin(TS)∩L(A)=∅
TS⊗A⊨不变性"always¬F"TS\otimes A\vDash 不变性"always \lnot F"TS⊗A⊨不变性"always¬F"

首先将正则安全性P表示为一个接受坏前缀的自动机A，然后将TS模型与自动机A结合运算生成新的TS’，在新的TS‘上利用搜索算法检测不变性¬qF\lnot q_{F}¬qF是否成立

算法的时间复杂度为O(size(TS)⋅size(A))O(size(TS)·size(A))O(size(TS)⋅size(A))，这个挺好理解，因为DFS或者BFS要搜索每一个可达状态，而状态S’=SxQ，所以规模就是TS和A规模的乘积。

写给学生看的系统分析与验证笔记（九）——验证正则安全性(verifying regular safety properties)相关推荐

写给学生看的系统分析与验证笔记（七）——线性时间属性（Linear-Time Properties）
目录路径和状态图(Paths and State Graph) 状态图路径迹(trace) 刻画线性时间属性(LT Properties) 刻画基于信号量互斥系统的属性刻画无饥饿(starva ...
写给学生看的系统分析与验证笔记（十五）——计算树逻辑(Computation tree logic,CTL)
目录介绍计算树线性时间和分支时间的对比 CTL的语法 CTL的语义 CTL状态公式的语义 CTL路径公式的语义 CTL在TS上的语义 CTL等价的定义 CTL公式的性质介绍在前面我们已经介绍 ...
《The Non-Designer's Design Book(写给大家看的设计书)》--笔记整理
The Non-Designer's Design Book(写给大家看的设计书)-笔记整理这是一本实用性书籍,阐述了设计中的四大原则:亲密性.对齐.重复和对比,并介绍了如何运用颜色.字体,以及针对 ...
写给大家看的设计书阅读笔记1——设计的四大基本原则
设计的四大基本原则概述有一些基本的设计原则,每一个优秀的设计中都应用了这些原则.我们在观察评价一个设计作品时,也要从这几条基本原则去考虑. 亲密性 Proximity 彼此相关的项应当靠近,归组在一 ...
《写给大家看的设计书》《写给大家看的色彩书》《点石成金》《形式感》学习笔记...
为什么80%的码农都做不了架构师?>>> 首发:个人博客,更新&纠错&回复今天读了四本书<写给大家看的设计书><写给大家看的色彩书>& ...
《写给大家看的设计书》《写给大家看的色彩书》《点石成金》《形式感》学习笔记
首发:个人博客,更新&纠错&回复今天读了四本书<写给大家看的设计书><写给大家看的色彩书><点石成金>和<形式感>,学习学习设计. 笔 ...
用JDBC写一个学生管理系统（添加、删除、修改、查询学生信息）（二）
本文上接用JDBC写一个学生管理系统(添加.删除.修改.查询学生信息) 这次主要是对上一文中的查询方法做一下调整,用创建内部类的方法来实现学生信息的查询. 我们先要定义一个接口IRowMapper: ...
用JDBC写一个学生管理系统（添加、删除、修改、查询学生信息）
首先需要用Navicat Premium创建一个student表用Java连接好MySQL数据库(需要copy一个mysql-connector-java-5.1.44-bin.jar包,该包可在网 ...
读书笔记—写给大家看的PPT设计书
作者:[美]Robin Williams 第一部分写在设计之前在现实生活中你可以表现得不可思议地愚蠢,你的话可以让人听得毫无兴致,昏昏欲睡,但是在这个演讲的舞台上,你却是一个明星!同时你还承担着让 ...

写给学生看的系统分析与验证笔记（九）——验证正则安全性(verifying regular safety properties)

目录

正则安全性

验证正则安全性

总结

写给学生看的系统分析与验证笔记（九）——验证正则安全性(verifying regular safety properties)相关推荐

最新文章

热门文章