为什么我们想要/需要进行抽象2.

四、关于验证的详细说明1、反例表示2、验证的定义3、验证过程4、验证结果判定

T_3

Q它代表系统所有可能处于的状态是一个有限集。

例如在简单的自动售货机模型中状态可能包括

“空闲”“已投币”“商品已售出”

Σ这些标签表示能够触发系统状态间转移的符号。

在自动售货机的例子里转移标签可以是

“投币”“选择商品”“出货”

等它们代表了能使系统从一个状态转变到另一个状态的事件或输入。

初始状态

q_{init}

集合是有限状态系统开始运行时所处的状态。

对于自动售货机初始状态可能就是

“空闲”

→⊆Q×Σ×Q此函数定义了系统如何基于输入符号从一个状态转移到另一个状态。

若

(q_1,

qinit2​确保两个系统的起始点以一致的方式关联。

转移对应对于

T_1

\alpha(q_1)\overset{a}{\to}_2\alpha(q_2)

T_1

Q1​{q空闲​,q1元币投入​,q2元币投入​,q选择商品​,q出货​}

转移标签集

{(q空闲​,投1元币,q1元币投入​),(q空闲​,投2元币,q2元币投入​),(q1元币投入​,选择商品,q选择商品​),(q2元币投入​,选择商品,q选择商品​),(q选择商品​,出货,q出货​)}。

T_2

{(q未投币​,投币,q已投币​),(q已投币​,选择商品,q出货​),(q出货​,出货,q出货​)}。

定义函数

\alpha(q_{init}^1)\alpha(q_{空闲})

q_{未投币}q_{init}^2

α(qinit1​)α(q空闲​)q未投币​qinit2​并且对于

T_1

\alpha(q_{空闲})\overset{投币}{\to}_2\alpha(q_{1

元币投入})

Q1​{q空闲​,q1元币投入​,q2元币投入​,q选择商品​,q出货​,q找零​}转移标签集

选择商品

{(q空闲​,投1元币,q1元币投入​),(q空闲​,投2元币,q2元币投入​),(q1元币投入​,选择商品,q选择商品​),(q2元币投入​,选择商品,q选择商品​),(q选择商品​,出货,q出货​),(q2元币投入​,找零,q找零​)}

定义等价关系

Q2​Q1​/∼{[q空闲​],[q1元币投入​],[q选择商品​],[q出货​],[q找零​]}其中

[q_{空闲}]

元币投入}]\overset{选择商品}{\to}_2[q_{选择商品}]

T_1

答案为了获得“更简单”的系统解释在实际应用中复杂系统的分析和理解往往具有很高的难度。

以自动售货机的有限状态系统为例一个详细描述的自动售货机状态系统可能包含众多状态如不同货币投入状态、各种商品选择状态、找零状态等以及复杂的转移关系。

这种复杂性使得对系统进行全面分析例如验证其是否正常工作、是否存在安全漏洞等变得十分困难。

通过抽象我们可以将这些复杂的状态和关系进行简化去除一些不必要的细节从而得到一个更易于理解和处理的“更简单”的系统。

例如将不同货币投入状态合并为一个“已投币”状态这样就减少了状态数量使得系统结构更加清晰便于我们进行分析和研究。

答案不。

它保留特定的属性。

解释抽象是对原始系统的一种简化表示它必然会舍弃一些细节。

在有限状态系统的抽象过程中不是所有原始系统的属性都会被保留下来。

例如在自动售货机从详细状态系统到简化状态系统的抽象过程中详细系统中关于投入不同金额货币的区分这一属性在简化抽象系统中可能就不再保留。

但抽象会保留某些特定属性这些属性通常是与我们关注的系统关键行为或特性相关的。

例如系统从“未投币”状态经过“投币”操作可以进入“已投币”状态进而进行“选择商品”和“出货”等基本行为属性会被保留以确保抽象后的系统仍然能够反映原始系统的核心功能。

解释这是抽象保留特定属性的一个体现。

在系统安全性方面如果我们对一个系统进行抽象后发现抽象后的系统满足安全要求即不存在安全风险那么可以推断原始系统也是安全的。

这是因为抽象过程虽然简化了系统但保留了与安全性相关的关键特征和行为。

例如在自动售货机系统中如果抽象后的系统在各种操作流程下都不会出现商品未付款就出货、投币丢失等安全问题那么由于抽象保留了这些关键行为的逻辑原始的详细系统同样也不会出现这些安全问题。

因为抽象系统是基于原始系统构建的其安全行为是对原始系统安全相关行为的一种提炼和保留。

答案不。

可能没有得到合适的抽象。

解释虽然抽象在一定程度上能够反映原始系统的属性但并不是所有的抽象都能有效地证明原始系统的安全性。

如果抽象过程中过度简化丢失了与安全性紧密相关的关键信息那么即使抽象后的系统看起来是安全的也不能确定原始系统一定安全。

例如在自动售货机系统中如果抽象时将投币验证环节完全简化掉使得抽象系统中不存在投币验证相关状态和转移那么这个抽象系统可能看似“安全”因为没有涉及投币验证相关的错误可能但实际上原始系统中存在投币验证这一关键安全环节所以不能依据这个抽象系统来证明原始系统的安全性。

这就说明只有合适的抽象即保留了与安全性相关的关键属性和行为的抽象才能用于证明原始安全系统的安全性。

答案Refinement!细化解释细化是寻找合适抽象的一种方法。

当我们最初得到的抽象可能不理想没有保留我们所需要的关键属性时就需要对抽象进行细化。

以自动售货机为例如果最初的抽象系统过于简化丢失了投币验证环节我们可以通过细化操作重新引入与投币验证相关的状态和转移关系使抽象系统更加接近原始系统的真实行为从而保留关键属性。

通过不断地对抽象进行调整和细化使其既能简化原始系统以便于分析又能保留我们关注的关键属性如安全性、功能性等最终得到一个“合适”的抽象能够有效地用于对原始系统的分析和验证。

“Let

设T1是一个有限状态系统FSST2是它的抽象。

T2的一个细化是一个有限状态系统T3使得T1

T2。

这里定义了细化的概念即存在一个新的有限状态系统T3它与T1和T2存在特定的抽象关系。

T1是原始系统T2是T1的抽象系统而T3是对T2的细化T3比T2更接近T1在抽象程度上处于T1和T2之间。

也就是说T3相对于T2保留了更多T1的细节和特性但又不像T1那样复杂仍然具有一定的抽象性。

一种方法是——反例引导的抽象细化CEGAR。

CEGARCounter

Example

Refinement反例引导的抽象细化的方法。

CEGAR方法通常基于对抽象系统分析过程中发现的反例来指导对抽象系统进行细化使其更精确地反映原始系统的行为从而在抽象与原始系统之间找到一个更合适的中间系统即实现对抽象系统的细化。

三、CEGAR分析流程解析

呢这个问题是整个分析流程的核心关注点我们后续的所有操作都是围绕判断这个可达性展开。

在程序bug查错的问题中可以将出错分支添加一个可达性检查如果执行到出错分支那么就说明程序出错了。

构建抽象系统

的确定性结论只能说“不确定”。

因为抽象系统可能因为简化而引入了一些在原始系统中不存在的“虚假”路径。

T_2

中有对应的具体反例那么我们就找到了一个真正的反例这表明原始系统

T_1

qf​而这个状态可能代表了某种不安全的情况比如自动售货机在未付款时就出货的状态等。

3.2

中没有对应的具体反例那么这个抽象反例就是“虚假的“spurious””。

也就是说它是由于抽象过程的简化而产生的在实际的原始系统

T_1

进行细化。

通过分析虚假抽象反例产生的原因我们可以在抽象系统中添加更多的细节使其更接近原始系统

T_1

的真实行为从而得到一个更精确的抽象系统。

例如如果虚假抽象反例是由于在抽象过程中忽略了某个关键状态或转移关系导致的我们就可以在细化过程中重新引入这些元素。

经过细化后我们可以再次对新的抽象系统进行模型检查和后续的验证步骤不断重复这个过程直到能够确定原始系统

T_1

的可达性问题通过抽象、检查、验证和细化等步骤在简化分析的同时确保分析结果的准确性。

在有限状态系统FSS的分析过程中验证是一个关键环节用于确定从抽象系统如

T_2

Reachi​α−1(q0i​)∩Pre(Reachi1​,ai​)

来计算

的初始状态集合中存在能够按照我们所期望的路径通过一系列状态转移最终到达

q_f

中不存在这样的路径即抽象反例是虚假的在原始系统中并不存在对应的真实反例。

通过以上验证过程我们能够准确判断抽象系统中的反例在原始系统中是否真实有效从而进一步对系统的安全性、可达性等性质进行准确分析。

在对有限状态系统进行分析时基于反例分析的细化是优化抽象系统的重要手段。

以下详细阐述该细化过程

1、确定关键索引

集合序列找到抽象与原始系统行为出现偏差的关键位置因为空集的出现暗示了在抽象过程中丢失了某些必要的状态或转移关系需要进行修正。

2、分析集合关系

Post(α−1(q0j​))∩Reachj1​∅这表明从能映射到

q_0^j

的原始状态出发经过一次转移后到达的状态集合与后续应该能够到达目标状态

q_f

Reachj1​。

通过这种拆分方式我们在抽象系统中引入了更多的细节使得抽象系统能够更好地反映原始系统的状态转移关系。

经过这样的处理后我们就得到了新的抽象系统

T_3

T2​在保留原始系统关键特性的同时更准确地模拟了原始系统的行为从而在后续的分析中能够提供更可靠的结果。

通过以上步骤基于反例分析的细化过程能够有效地优化抽象系统使其更符合原始系统的真实情况为进一步准确分析系统的性质和行为提供了有力支持。

六、参考文献

主要参考https://mitras.ece.illinois.edu/ECE584/Archives/2012/lectures/Lecture20.pdf