企业网站模板大全,查询网域名查询,网站价格评估 优帮云,华为服务器文章目录 一、有限状态系统的抽象定义及相关阐述1、有限状态系统定义2、 有限状态系统间的抽象关系#xff08;Abstract#xff09;2.1 基于函数的抽象定义2.2 基于等价关系的抽象定义 二、 基于上面的定义出发#xff0c;提出的思考1. 为什么我们想要/需要进行抽象2. 抽象是… 文章目录 一、有限状态系统的抽象定义及相关阐述1、有限状态系统定义2、 有限状态系统间的抽象关系Abstract2.1 基于函数的抽象定义2.2 基于等价关系的抽象定义 二、 基于上面的定义出发提出的思考1. 为什么我们想要/需要进行抽象2. 抽象是否保留所有属性3. 示例如果抽象是安全的那么原始系统就是安全的4. 抽象总能证明一个安全系统的安全性吗5. 我们如何寻找“合适”的抽象6. 细化的定义7. 如何进行细化的方法 三、CEGAR分析流程解析可达性问题设定1、 构建抽象系统 抽象2、 对抽象系统进行模型检查 检查2.1 模型检查结果判断 - 答案为否 T 1 T_1 T1 是安全的2.2 模型检查结果判断 - 答案为是不确定 3、 验证抽象反例 验证3.1 验证结果判断 - 存在具体反例 不安全3.2 验证结果判断 - 不存在具体反例虚假的 4、利用虚假抽象反例进行细化 细化 四、关于验证的详细说明1、反例表示2、验证的定义3、验证过程4、验证结果判定 五、基于反例分析的细化过程介绍1、确定关键索引 j j j2、分析集合关系3、构建新的抽象系统 T 3 T_3 T3 六、参考文献 一、有限状态系统的抽象定义及相关阐述
1、有限状态系统定义
有限状态系统Finite state system, FSS T T T 由多个关键部分构成
有限状态集合 Q Q Q它代表系统所有可能处于的状态是一个有限集。例如在简单的自动售货机模型中状态可能包括 “空闲”“已投币”“商品已售出” 等每个状态描述了系统在某一时刻的特定条件或配置。转移标签集合 Σ \Sigma Σ这些标签表示能够触发系统状态间转移的符号。在自动售货机的例子里转移标签可以是 “投币”“选择商品”“出货” 等它们代表了能使系统从一个状态转变到另一个状态的事件或输入。初始状态 q i n i t q_{init} qinit属于 Q Q Q 集合是有限状态系统开始运行时所处的状态。对于自动售货机初始状态可能就是 “空闲” 状态。转移函数 → ⊆ Q × Σ × Q \to\subseteq Q\times\Sigma\times Q →⊆Q×Σ×Q此函数定义了系统如何基于输入符号从一个状态转移到另一个状态。若 ( q 1 , a , q 2 ) ∈ → (q_1, a, q_2)\in\to (q1,a,q2)∈→意味着当系统处于状态 q 1 q_1 q1 且接收到输入符号 a ∈ Σ a\in\Sigma a∈Σ 时会转移到状态 q 2 q_2 q2。比如若 ( “空闲” , “投币” , “已投币” ) ∈ → (“空闲”, “投币”, “已投币”)\in\to (“空闲”,“投币”,“已投币”)∈→表明自动售货机在 “空闲” 状态下接收到投币操作后会转变为 “已投币” 状态。
2、 有限状态系统间的抽象关系Abstract
抽象关系的定义可以基于函数也可以基于等价关系来定义。
2.1 基于函数的抽象定义
设 T 1 T_1 T1 和 T 2 T_2 T2 为两个有限状态系统。若存在函数 α : Q 1 → Q 2 \alpha : Q_1 → Q_2 α:Q1→Q2满足以下两个条件则称 T 2 T_2 T2 是 T 1 T_1 T1 的抽象记为 T 1 ≺ T 2 T_1 ≺ T_2 T1≺T2
初始状态对应 α ( q i n i t 1 ) q i n i t 2 \alpha(q_{init}^1) q_{init}^2 α(qinit1)qinit2即该函数将 T 1 T_1 T1 的初始状态 q i n i t 1 q_{init}^1 qinit1 映射到 T 2 T_2 T2 的初始状态 q i n i t 2 q_{init}^2 qinit2确保两个系统的起始点以一致的方式关联。转移对应对于 T 1 T_1 T1 中的每一个转移 q 1 → a 1 q 2 q_1\overset{a}{\to}_1 q_2 q1→a1q2在 T 2 T_2 T2 中都有对应的转移 α ( q 1 ) → a 2 α ( q 2 ) \alpha(q_1)\overset{a}{\to}_2\alpha(q_2) α(q1)→a2α(q2)。这表明 T 1 T_1 T1 在输入 a a a 时的行为通过函数 α \alpha α 在 T 2 T_2 T2 中得到体现。
例如设 T 1 T_1 T1 为一个较为详细的自动售货机有限状态系统 其状态集 Q 1 { q 空闲 , q 1 元币投入 , q 2 元币投入 , q 选择商品 , q 出货 } Q_1 \{q_{空闲}, q_{1 元币投入}, q_{2 元币投入}, q_{选择商品}, q_{出货}\} Q1{q空闲,q1元币投入,q2元币投入,q选择商品,q出货} 转移标签集 Σ 1 { 投 1 元币 , 投 2 元币 , 选择商品 , 出货 } \Sigma_1\{投 1 元币, 投 2 元币, 选择商品, 出货\} Σ1{投1元币,投2元币,选择商品,出货} 初始状态 q i n i t 1 q 空闲 q_{init}^1 q_{空闲} qinit1q空闲 转移关系为 { ( q 空闲 , 投 1 元币 , q 1 元币投入 ) , ( q 空闲 , 投 2 元币 , q 2 元币投入 ) , ( q 1 元币投入 , 选择商品 , q 选择商品 ) , ( q 2 元币投入 , 选择商品 , q 选择商品 ) , ( q 选择商品 , 出货 , q 出货 ) } \{(q_{空闲}, 投 1 元币, q_{1 元币投入}),(q_{空闲}, 投 2 元币, q_{2 元币投入}),(q_{1 元币投入}, 选择商品, q_{选择商品}),(q_{2 元币投入}, 选择商品, q_{选择商品}),(q_{选择商品}, 出货, q_{出货})\} {(q空闲,投1元币,q1元币投入),(q空闲,投2元币,q2元币投入),(q1元币投入,选择商品,q选择商品),(q2元币投入,选择商品,q选择商品),(q选择商品,出货,q出货)}。 设 T 2 T_2 T2 为一个简化的自动售货机有限状态系统 其状态集 Q 2 { q 未投币 , q 已投币 , q 出货 } Q_2\{q_{未投币}, q_{已投币}, q_{出货}\} Q2{q未投币,q已投币,q出货} 转移标签集 Σ 2 { 投币 , 选择商品 , 出货 } \Sigma_2 \{投币, 选择商品, 出货\} Σ2{投币,选择商品,出货} 初始状态 q i n i t 2 q 未投币 q_{init}^2q_{未投币} qinit2q未投币 转移关系为 { ( q 未投币 , 投币 , q 已投币 ) , ( q 已投币 , 选择商品 , q 出货 ) , ( q 出货 , 出货 , q 出货 ) } \{(q_{未投币}, 投币, q_{已投币}),(q_{已投币}, 选择商品, q_{出货}),(q_{出货}, 出货, q_{出货})\} {(q未投币,投币,q已投币),(q已投币,选择商品,q出货),(q出货,出货,q出货)}。
定义函数 α ( q 空闲 ) q 未投币 \alpha(q_{空闲}) q_{未投币} α(q空闲)q未投币 α ( q 1 元币投入 ) α ( q 2 元币投入 ) q 已投币 \alpha(q_{1 元币投入})\alpha(q_{2 元币投入}) q_{已投币} α(q1元币投入)α(q2元币投入)q已投币 α ( q 选择商品 ) α ( q 出货 ) q 出货 \alpha(q_{选择商品})\alpha(q_{出货}) q_{出货} α(q选择商品)α(q出货)q出货。此时 α ( q i n i t 1 ) α ( q 空闲 ) q 未投币 q i n i t 2 \alpha(q_{init}^1)\alpha(q_{空闲}) q_{未投币}q_{init}^2 α(qinit1)α(q空闲)q未投币qinit2并且对于 T 1 T_1 T1 中的转移如 q 空闲 → 投 1 元币 1 q 1 元币投入 q_{空闲}\overset{投 1 元币}{\to}_1 q_{1 元币投入} q空闲→投1元币1q1元币投入在 T 2 T_2 T2 中有 α ( q 空闲 ) → 投币 2 α ( q 1 元币投入 ) \alpha(q_{空闲})\overset{投币}{\to}_2\alpha(q_{1 元币投入}) α(q空闲)→投币2α(q1元币投入)因为 α ( q 空闲 ) q 未投币 \alpha(q_{空闲}) q_{未投币} α(q空闲)q未投币 且 α ( q 1 元币投入 ) q 已投币 \alpha(q_{1 元币投入}) q_{已投币} α(q1元币投入)q已投币 且 q 未投币 → 投币 2 q 已投币 q_{未投币}\overset{投币}{\to}_2 q_{已投币} q未投币→投币2q已投币其他转移也类似满足对应关系所以 T 2 T_2 T2 是 T 1 T_1 T1 的抽象 T 1 ≺ T 2 T_1\prec T_2 T1≺T2。
2.2 基于等价关系的抽象定义
给定 T 1 T_1 T1 状态集 Q 1 Q_1 Q1 上的一个等价关系 ∼ ⊆ Q 1 × Q 1 \sim\subseteq Q_1 × Q_1 ∼⊆Q1×Q1可按如下方式定义 T 1 T_1 T1 的抽象 T 2 T 1 / ∼ T_2 T_1/ \sim T2T1/∼
状态集 T 2 T_2 T2 的状态集 Q 2 Q 1 / ∼ Q_2 Q_1/ \sim Q2Q1/∼即 Q 2 Q_2 Q2 的元素是 Q 1 Q_1 Q1 在等价关系 ∼ \sim ∼ 下的等价类。转移关系在 T 2 T_2 T2 中当且仅当存在 q 1 ∈ q 2 q_1\in q_2 q1∈q2 和 q 1 ′ ∈ q 2 ′ q_1\in q_2 q1′∈q2′其中 q 2 q_2 q2 和 q 2 ′ q_2 q2′ 是 Q 2 Q_2 Q2 中的等价类使得在 T 1 T_1 T1 中有 q 1 → a 1 q 1 ′ q_1\overset{a}{\to}_1 q_1 q1→a1q1′ 时才有转移 q 2 → a 2 q 2 ′ q_2\overset{a}{\to}_2 q_2 q2→a2q2′。
继续以自动售货机为例设 T 1 T_1 T1 的状态集 Q 1 { q 空闲 , q 1 元币投入 , q 2 元币投入 , q 选择商品 , q 出货 , q 找零 } Q_1\{q_{空闲}, q_{1 元币投入}, q_{2 元币投入}, q_{选择商品}, q_{出货}, q_{找零}\} Q1{q空闲,q1元币投入,q2元币投入,q选择商品,q出货,q找零}转移标签集 Σ 1 { 投 1 元币 , 投 2 元币 , 选择商品 , 出货 , 找零 } \Sigma_1 \{投 1 元币, 投 2 元币, 选择商品, 出货, 找零\} Σ1{投1元币,投2元币,选择商品,出货,找零}转移关系为 { ( q 空闲 , 投 1 元币 , q 1 元币投入 ) , ( q 空闲 , 投 2 元币 , q 2 元币投入 ) , ( q 1 元币投入 , 选择商品 , q 选择商品 ) , ( q 2 元币投入 , 选择商品 , q 选择商品 ) , ( q 选择商品 , 出货 , q 出货 ) , ( q 2 元币投入 , 找零 , q 找零 ) } \{(q_{空闲}, 投 1 元币, q_{1 元币投入}),(q_{空闲}, 投 2 元币, q_{2 元币投入}),(q_{1 元币投入}, 选择商品, q_{选择商品}), (q_{2 元币投入}, 选择商品, q_{选择商品}), (q_{选择商品}, 出货, q_{出货}),(q_{2 元币投入}, 找零, q_{找零})\} {(q空闲,投1元币,q1元币投入),(q空闲,投2元币,q2元币投入),(q1元币投入,选择商品,q选择商品),(q2元币投入,选择商品,q选择商品),(q选择商品,出货,q出货),(q2元币投入,找零,q找零)}
定义等价关系 ∼ \sim ∼ 如下如果两个状态在货币处理方式上相同则它们等价。即 q 1 元币投入 ∼ q 2 元币投入 q_{1 元币投入}\sim q_{2 元币投入} q1元币投入∼q2元币投入因为都涉及投币操作只是金额不同 q 空闲 q_{空闲} q空闲 自成一个等价类 q 选择商品 q_{选择商品} q选择商品 自成一个等价类 q 出货 q_{出货} q出货 自成一个等价类 q 找零 q_{找零} q找零 自成一个等价类。
那么 Q 2 Q 1 / ∼ { [ q 空闲 ] , [ q 1 元币投入 ] , [ q 选择商品 ] , [ q 出货 ] , [ q 找零 ] } Q_2 Q_1/\sim\{[q_{空闲}], [q_{1 元币投入}], [q_{选择商品}], [q_{出货}], [q_{找零}]\} Q2Q1/∼{[q空闲],[q1元币投入],[q选择商品],[q出货],[q找零]}其中 [ q 空闲 ] [q_{空闲}] [q空闲] 是 q 空闲 q_{空闲} q空闲 的等价类 [ q 1 元币投入 ] [q_{1 元币投入}] [q1元币投入] 是 q 1 元币投入 q_{1 元币投入} q1元币投入 和 q 2 元币投入 q_{2 元币投入} q2元币投入 的等价类等。
对于 T 1 T_1 T1 中的转移 q 1 元币投入 → 选择商品 1 q 选择商品 q_{1 元币投入}\overset{选择商品}{\to}_1 q_{选择商品} q1元币投入→选择商品1q选择商品因为 q 1 元币投入 ∈ [ q 1 元币投入 ] q_{1 元币投入}\in[q_{1 元币投入}] q1元币投入∈[q1元币投入] 且 q 选择商品 ∈ [ q 选择商品 ] q_{选择商品}\in[q_{选择商品}] q选择商品∈[q选择商品]所以在 T 2 T 1 / ∼ T_2 T_1/\sim T2T1/∼ 中有 [ q 1 元币投入 ] → 选择商品 2 [ q 选择商品 ] [q_{1 元币投入}]\overset{选择商品}{\to}_2[q_{选择商品}] [q1元币投入]→选择商品2[q选择商品]。同理对于 T 1 T_1 T1 中的其他转移也可按此规则确定 T 2 T_2 T2 中的转移关系。
二、 基于上面的定义出发提出的思考
1. 为什么我们想要/需要进行抽象
答案为了获得“更简单”的系统解释在实际应用中复杂系统的分析和理解往往具有很高的难度。以自动售货机的有限状态系统为例一个详细描述的自动售货机状态系统可能包含众多状态如不同货币投入状态、各种商品选择状态、找零状态等以及复杂的转移关系。这种复杂性使得对系统进行全面分析例如验证其是否正常工作、是否存在安全漏洞等变得十分困难。通过抽象我们可以将这些复杂的状态和关系进行简化去除一些不必要的细节从而得到一个更易于理解和处理的“更简单”的系统。例如将不同货币投入状态合并为一个“已投币”状态这样就减少了状态数量使得系统结构更加清晰便于我们进行分析和研究。
2. 抽象是否保留所有属性
答案不。它保留特定的属性。解释抽象是对原始系统的一种简化表示它必然会舍弃一些细节。在有限状态系统的抽象过程中不是所有原始系统的属性都会被保留下来。例如在自动售货机从详细状态系统到简化状态系统的抽象过程中详细系统中关于投入不同金额货币的区分这一属性在简化抽象系统中可能就不再保留。但抽象会保留某些特定属性这些属性通常是与我们关注的系统关键行为或特性相关的。例如系统从“未投币”状态经过“投币”操作可以进入“已投币”状态进而进行“选择商品”和“出货”等基本行为属性会被保留以确保抽象后的系统仍然能够反映原始系统的核心功能。
3. 示例如果抽象是安全的那么原始系统就是安全的
解释这是抽象保留特定属性的一个体现。在系统安全性方面如果我们对一个系统进行抽象后发现抽象后的系统满足安全要求即不存在安全风险那么可以推断原始系统也是安全的。这是因为抽象过程虽然简化了系统但保留了与安全性相关的关键特征和行为。例如在自动售货机系统中如果抽象后的系统在各种操作流程下都不会出现商品未付款就出货、投币丢失等安全问题那么由于抽象保留了这些关键行为的逻辑原始的详细系统同样也不会出现这些安全问题。因为抽象系统是基于原始系统构建的其安全行为是对原始系统安全相关行为的一种提炼和保留。
4. 抽象总能证明一个安全系统的安全性吗
答案不。可能没有得到合适的抽象。解释虽然抽象在一定程度上能够反映原始系统的属性但并不是所有的抽象都能有效地证明原始系统的安全性。如果抽象过程中过度简化丢失了与安全性紧密相关的关键信息那么即使抽象后的系统看起来是安全的也不能确定原始系统一定安全。例如在自动售货机系统中如果抽象时将投币验证环节完全简化掉使得抽象系统中不存在投币验证相关状态和转移那么这个抽象系统可能看似“安全”因为没有涉及投币验证相关的错误可能但实际上原始系统中存在投币验证这一关键安全环节所以不能依据这个抽象系统来证明原始系统的安全性。这就说明只有合适的抽象即保留了与安全性相关的关键属性和行为的抽象才能用于证明原始安全系统的安全性。
5. 我们如何寻找“合适”的抽象
答案Refinement!细化解释细化是寻找合适抽象的一种方法。当我们最初得到的抽象可能不理想没有保留我们所需要的关键属性时就需要对抽象进行细化。以自动售货机为例如果最初的抽象系统过于简化丢失了投币验证环节我们可以通过细化操作重新引入与投币验证相关的状态和转移关系使抽象系统更加接近原始系统的真实行为从而保留关键属性。通过不断地对抽象进行调整和细化使其既能简化原始系统以便于分析又能保留我们关注的关键属性如安全性、功能性等最终得到一个“合适”的抽象能够有效地用于对原始系统的分析和验证。
6. 细化的定义
“Let T1 be a FSS and T2 its abstraction.“A refinement of T2 is an FSS T3 such that T1 ≺ T3 ≺ T2.” 设T1是一个有限状态系统FSST2是它的抽象。T2的一个细化是一个有限状态系统T3使得T1 ≺ T3 ≺ T2。这里定义了细化的概念即存在一个新的有限状态系统T3它与T1和T2存在特定的抽象关系。T1是原始系统T2是T1的抽象系统而T3是对T2的细化T3比T2更接近T1在抽象程度上处于T1和T2之间。也就是说T3相对于T2保留了更多T1的细节和特性但又不像T1那样复杂仍然具有一定的抽象性。
7. 如何进行细化的方法
一种方法是——反例引导的抽象细化CEGAR。CEGARCounter - Example - Guided Abstraction Refinement反例引导的抽象细化的方法。CEGAR方法通常基于对抽象系统分析过程中发现的反例来指导对抽象系统进行细化使其更精确地反映原始系统的行为从而在抽象与原始系统之间找到一个更合适的中间系统即实现对抽象系统的细化。
三、CEGAR分析流程解析
可达性问题设定
首先我们面临一个可达性问题给定一个状态 q f q_f qf从有限状态系统 T 1 T_1 T1 的初始状态出发能否到达该状态 q f q_f qf 呢这个问题是整个分析流程的核心关注点我们后续的所有操作都是围绕判断这个可达性展开。
在程序bug查错的问题中可以将出错分支添加一个可达性检查如果执行到出错分支那么就说明程序出错了。 1、 构建抽象系统 抽象
为了简化问题的分析我们构建一个 T 1 T_1 T1 的抽象系统 T 2 T_2 T2。通过抽象我们将复杂的 T 1 T_1 T1 系统简化为一个更容易分析的 T 2 T_2 T2 系统但同时保留了与可达性问题相关的关键特征。
2、 对抽象系统进行模型检查 检查
在得到抽象系统 T 2 T_2 T2 后我们对其进行模型检查。具体检查的内容是从 T 2 T_2 T2 的初始状态出发能否到达状态 α ( q f ) \alpha(q_f) α(qf) 呢这里的 α \alpha α 是从 T 1 T_1 T1 到 T 2 T_2 T2 的抽象映射函数将 T 1 T_1 T1 中的状态 q f q_f qf 映射到 T 2 T_2 T2 中的 α ( q f ) \alpha(q_f) α(qf)。
2.1 模型检查结果判断 - 答案为否 T 1 T_1 T1 是安全的
如果模型检查的答案是“否”即从 T 2 T_2 T2 的初始状态无法到达 α ( q f ) \alpha(q_f) α(qf)那么我们可以得出结论 T 1 T_1 T1 是安全的。这是因为抽象系统 T 2 T_2 T2 虽然简化了 T 1 T_1 T1但保留了可达性相关的关键属性。如果在 T 2 T_2 T2 中都无法到达对应的抽象状态那么在更复杂的原始系统 T 1 T_1 T1 中也必然无法到达目标状态 q f q_f qf所以可以判定 T 1 T_1 T1 是安全的。
2.2 模型检查结果判断 - 答案为是不确定
如果模型检查的答案是“是”即从 T 2 T_2 T2 的初始状态可以到达 α ( q f ) \alpha(q_f) α(qf)此时我们不能直接得出关于 T 1 T_1 T1 的确定性结论只能说“不确定”。因为抽象系统可能因为简化而引入了一些在原始系统中不存在的“虚假”路径。
当答案为“是”时模型检查会返回一条在 T 2 T_2 T2 中到达 α ( q f ) \alpha(q_f) α(qf) 的路径这条路径被称为“ **抽象反例 **”。它展示了在抽象系统 T 2 T_2 T2 中从初始状态到 α ( q f ) \alpha(q_f) α(qf) 的一种可能的执行路径。
3、 验证抽象反例 验证
得到抽象反例后我们需要检查这个抽象反例是否在原始系统 T 1 T_1 T1 中有对应的“具体反例”这个过程称为验证。
3.1 验证结果判断 - 存在具体反例 不安全
如果经过验证发现抽象反例在原始系统 T 1 T_1 T1 中有对应的具体反例那么我们就找到了一个真正的反例这表明原始系统 T 1 T_1 T1 是不安全的。因为这个具体反例展示了从 T 1 T_1 T1 的初始状态可以到达我们关注的状态 q f q_f qf而这个状态可能代表了某种不安全的情况比如自动售货机在未付款时就出货的状态等。
3.2 验证结果判断 - 不存在具体反例虚假的
如果验证后发现抽象反例在原始系统 T 1 T_1 T1 中没有对应的具体反例那么这个抽象反例就是“虚假的“spurious””。也就是说它是由于抽象过程的简化而产生的在实际的原始系统 T 1 T_1 T1 中并不存在这样的执行路径。
4、利用虚假抽象反例进行细化 细化
对于虚假的抽象反例我们利用它来对抽象系统 T 2 T_2 T2 进行细化。通过分析虚假抽象反例产生的原因我们可以在抽象系统中添加更多的细节使其更接近原始系统 T 1 T_1 T1 的真实行为从而得到一个更精确的抽象系统。例如如果虚假抽象反例是由于在抽象过程中忽略了某个关键状态或转移关系导致的我们就可以在细化过程中重新引入这些元素。经过细化后我们可以再次对新的抽象系统进行模型检查和后续的验证步骤不断重复这个过程直到能够确定原始系统 T 1 T_1 T1 的可达性情况。
通过这样的 CEGAR 分析流程我们能够逐步深入地分析复杂的有限状态系统 T 1 T_1 T1 的可达性问题通过抽象、检查、验证和细化等步骤在简化分析的同时确保分析结果的准确性。
四、关于验证的详细说明
在有限状态系统FSS的分析过程中验证是一个关键环节用于确定从抽象系统如 T 2 T_2 T2中得到的反例在原始系统如 T 1 T_1 T1中是否真实存在。
1、反例表示
在抽象系统 T 2 T_2 T2 中我们得到一个反例路径 σ 0 q 0 1 → a 1 q 0 2 → a 2 q 0 3 ⋯ → a k q 0 k 1 \sigma_0 q_0^1 \xrightarrow{a_1} q_0^2 \xrightarrow{a_2} q_0^3 \cdots \xrightarrow{a_k} q_0^{k 1} σ0q01a1 q02a2 q03⋯ak q0k1此路径作为 T 2 T_2 T2 中的反例。
2、验证的定义
验证的核心问题是在原始系统 T 1 T_1 T1 中是否存在这样一条路径 σ q 1 → a 1 q 2 → a 2 q 3 ⋯ → a k q k 1 \sigma q_1 \xrightarrow{a_1} q_2 \xrightarrow{a_2} q_3 \cdots \xrightarrow{a_k} q_{k 1} σq1a1 q2a2 q3⋯ak qk1满足以下条件 q 1 q i n i t 1 q_1 q_{init}^1 q1qinit1即路径起始于 T 1 T_1 T1 的初始状态。 q k 1 q f q_{k 1} q_f qk1qf即路径最终到达我们关注的状态 q f q_f qf。对于所有的 i i i都有 α ( q i ) q 0 i \alpha(q_i) q_0^i α(qi)q0i这里的 α \alpha α 是从 T 1 T_1 T1 到 T 2 T_2 T2 的抽象映射函数意味着 T 1 T_1 T1 路径上的状态通过抽象映射后与 T 2 T_2 T2 反例路径上的状态相对应。
3、验证过程
a. 定义可达状态集合对于 1 ≤ i ≤ k 1 1 \leq i \leq k 1 1≤i≤k1我们计算 R e a c h i Reach_i Reachi它表示所有能够 “模仿” q 0 i → a i ⋯ → a k q 0 k 1 q_0^i \xrightarrow{a_i} \cdots \xrightarrow{a_k} q_0^{k 1} q0iai ⋯ak q0k1 并最终到 q f q_f qf 的状态集合。b. 初始化 R e a c h k 1 Reach_{k 1} Reachk1首先明确 R e a c h k 1 { q f } Reach_{k 1} \{q_f\} Reachk1{qf}因为在路径的最后一步只有目标状态 q f q_f qf 能够满足到达 q f q_f qf 的条件。c. 计算其他 R e a c h i Reach_i Reachi 集合对于 1 ≤ i ≤ k 1 \leq i \leq k 1≤i≤k通过公式 R e a c h i α − 1 ( q 0 i ) ∩ P r e ( R e a c h i 1 , a i ) Reach_i \alpha^{-1}(q_0^i) \cap Pre(Reach_{i 1}, a_i) Reachiα−1(q0i)∩Pre(Reachi1,ai) 来计算 R e a c h i Reach_i Reachi。其中 α − 1 ( q 0 i ) \alpha^{-1}(q_0^i) α−1(q0i) 表示在 T 1 T_1 T1 中通过抽象映射 α \alpha α 能映射到 q 0 i q_0^i q0i 的所有状态集合 P r e ( R e a c h i 1 , a i ) Pre(Reach_{i 1}, a_i) Pre(Reachi1,ai) 表示在 T 1 T_1 T1 中通过输入 a i a_i ai 能够到达 R e a c h i 1 Reach_{i 1} Reachi1 集合中状态的所有前置状态集合。通过取这两个集合的交集我们得到 R e a c h i Reach_i Reachi即满足既能够通过抽象映射对应到 q 0 i q_0^i q0i又能通过输入 a i a_i ai 到达下一步状态集合 R e a c h i 1 Reach_{i 1} Reachi1 的状态集合。
4、验证结果判定
存在具体的路径 σ \sigma σ即原始系统 T 1 T_1 T1 中存在与抽象系统 T 2 T_2 T2 反例对应的真实反例当且仅当iff R e a c h 0 ≠ ∅ Reach_0 \neq \varnothing Reach0∅。如果 R e a c h 0 Reach_0 Reach0 不为空集说明在 T 1 T_1 T1 的初始状态集合中存在能够按照我们所期望的路径通过一系列状态转移最终到达 q f q_f qf 的状态也就意味着找到了与抽象反例对应的具体反例反之如果 R e a c h 0 Reach_0 Reach0 为空集则表明在 T 1 T_1 T1 中不存在这样的路径即抽象反例是虚假的在原始系统中并不存在对应的真实反例。
通过以上验证过程我们能够准确判断抽象系统中的反例在原始系统中是否真实有效从而进一步对系统的安全性、可达性等性质进行准确分析。
五、基于反例分析的细化过程介绍
在对有限状态系统进行分析时基于反例分析的细化是优化抽象系统的重要手段。以下详细阐述该细化过程
1、确定关键索引 j j j
首先我们通过反向计算来寻找一个关键的整数 j j j。在这个过程中我们关注计算得到的一系列集合 R e a c h i Reach_i Reachi。 j j j 被定义为满足 R e a c h j ∅ Reach_j \varnothing Reachj∅ 的最大整数也就是说在反向计算过程中 R e a c h j Reach_j Reachj 是第一个变为空集的集合。这一步骤的关键在于通过分析 R e a c h Reach Reach 集合序列找到抽象与原始系统行为出现偏差的关键位置因为空集的出现暗示了在抽象过程中丢失了某些必要的状态或转移关系需要进行修正。
2、分析集合关系
在确定了 j j j 之后我们考察 P o s t ( α − 1 ( q 0 j ) ) Post(\alpha^{-1}(q_0^j)) Post(α−1(q0j)) 和 R e a c h j 1 Reach_{j 1} Reachj1 这两个集合的关系。这里 α − 1 ( q 0 j ) \alpha^{-1}(q_0^j) α−1(q0j) 表示在原始系统 T 1 T_1 T1 中通过抽象映射 α \alpha α 能映射到抽象系统 T 2 T_2 T2 中状态 q 0 j q_0^j q0j 的所有状态集合而 P o s t ( α − 1 ( q 0 j ) ) Post(\alpha^{-1}(q_0^j)) Post(α−1(q0j)) 则是这些状态通过一次转移后所能到达的状态集合。我们发现 P o s t ( α − 1 ( q 0 j ) ) ∩ R e a c h j 1 ∅ Post(\alpha^{-1}(q_0^j)) \cap Reach_{j 1} \varnothing Post(α−1(q0j))∩Reachj1∅这表明从能映射到 q 0 j q_0^j q0j 的原始状态出发经过一次转移后到达的状态集合与后续应该能够到达目标状态 q f q_f qf 的状态集合 R e a c h j 1 Reach_{j 1} Reachj1 没有交集。这种不相交的情况进一步说明了在抽象过程中状态 q 0 j q_0^j q0j 的抽象可能过度简化导致了状态转移的不连续性需要对其进行调整。
3、构建新的抽象系统 T 3 T_3 T3
为了修正这种过度简化的情况我们对状态 q 0 j 1 q_0^{j 1} q0j1 进行拆分。将 q 0 j 1 q_0^{j 1} q0j1 拆分成两个状态使得其中一个状态包含 P o s t ( α − 1 ( q 0 j ) ) Post(\alpha^{-1}(q_0^j)) Post(α−1(q0j))另一个状态包含 R e a c h j 1 Reach_{j 1} Reachj1。通过这种拆分方式我们在抽象系统中引入了更多的细节使得抽象系统能够更好地反映原始系统的状态转移关系。经过这样的处理后我们就得到了新的抽象系统 T 3 T_3 T3。这个新的抽象系统 T 3 T_3 T3 相较于之前的抽象系统 T 2 T_2 T2在保留原始系统关键特性的同时更准确地模拟了原始系统的行为从而在后续的分析中能够提供更可靠的结果。
通过以上步骤基于反例分析的细化过程能够有效地优化抽象系统使其更符合原始系统的真实情况为进一步准确分析系统的性质和行为提供了有力支持。
六、参考文献
主要参考https://mitras.ece.illinois.edu/ECE584/Archives/2012/lectures/Lecture20.pdf
