软件系统的建模简介

时序系统,并发系统和响应式系统
时序系统(Sequential System), 并发系统(Concurrent System), 响应式系统(Reactive System)是三种常见的系统模型。
时序系统是可以由输入-输出关系描述的,即连接可能的初始状态与可能的计算结果状态。因此,验证时序系统的正确性可以化规为证明一阶逻辑,即给定一个确定的初始状态条件,证明其程序必定停机,且停机状态满足给定的条件。
并发系统是利用并行计算来提高计算效率。并发系统比简单时许系统更难建模验证,因为其各个组件之间在互相传递信息。在某些特定时刻,各部分程序的运行形成了某种竞争,导致在同一时刻,整体程序可能会出现多于一种可能的执行结果。比如说,两个子程序同时试图改变某变量的结果,则其发生的不同顺序会得到不同结果。
响应式系统是指程序的各组件之间,或程序与外部环境的交互起重要作用的系统。响应式系统可以是时序系统或并发系统。验证交互式系统可能会包括对请求的响应或服务的可用性验证。

状态(States)
状态这一概念是描述一个系统的核心。它捕捉并描述了系统在执行过程中,某一特定时刻的信息。对每个状态s,其取值在程序运行过程中为true或false.
在一阶逻辑观点下,状态s可以被表示为关于程序中所有变量的一个赋值。
一个命题公式也可以描述状态,比如我们并不关心变量\(x,y\)取值情况,但我们关心在任一时刻\(x\le y\)是否成立。此时我们可以用状态\(p=true\)当且仅当\(x\le y\)来描述。
两个重要的重要集合是初始状态集(initial states)和最终状态集(final states).

状态空间(State Spaces)
一个状态空间是一个有向图\(\langle S,\Delta,I\rangle\), 这里S是由状态组成的集合,\(\Delta\subseteq S\times S\)是状态之间可行的转换关系,I是初始状态集。
我们称这样的一个图为自动机(automaton). 一个自动机的运行(run)是指一个序列\(s_0s_1\cdots\)使得\(s_o\in I,(s_i,s_{i+1})\in \Delta\), 且此序列要么无穷,要么最后一项在\(\Delta\)中没有后继。在交错模型(每个时刻,至多一个转换被执行)中,将一个系统的一次执行视为这样的一个状态序列,称为交错序列。

转换系统(Transition Systems)
转换系统展示了一个(时序或并发)系统的单位动作。一个转换系统可以用于生成一个用于描述系统的状态空间。状态空间给出了系统内不同状态的关系信息,而转换系统给出了状态空间的生成关系。因此,相对而言,转换系统更加清晰。
一个转换系统\(\langle S,T,\Theta\rangle\)定义如下:
(1) S是一个一阶结构(structure), 即包含一个标签(signature) \(G=(V,F_0,R_0)\),一个定义域D, 一个函数集F,一个关系集R,和一个映射\(f:F_0\cup R_0\to F\cup R.\) 变量集\(V\)包含了程序代码和标号所需要的字符。
(2) 一个有限的转换集\(T\), T中的每个转换t具有如下形式:\[p\ \to\ (v_1,\cdots,v_n):=(e_1,\cdots,v_n).\]这里条件p是一个没有量词的一阶逻辑公式,\(v_i\in V,e_1\)是结构G上的一阶项(term). 也就是说,在条件p成立时,\(v_i\)可以被赋值为\(e_i\),从而完成一个转换。
(3) 一个初始条件\(\Theta\),由不含量词的、变量属于\(V\)的一阶公式组成。\(\Theta\)指出了初始状态集应具备哪些条件。

对于一个转换t,其激活条件为p。如果状态s满足\(s\vDash^S p,\)称t在状态s下可激活。如果状态s经转换t变为s', 记为\(s'=t(s).\)

同时允许多个赋值似乎与转换系统中单位动作的观点相悖。然而,注意到我们将程序的标号也纳入到了变量中,因此每个转换结束后,我们可以对标号赋值以决定接下来执行哪个转换(即动作),使得每个动作是确定的。

程序的一个执行(execution)定义为:一列无穷状态\(s_0,s_1,\cdots\)满足:
(1) \(s_0\vDash^S \Theta\);
对每个\(i\ge 0\), 以下之一成立:
(2) 存在转换t,其激活条件为p,使得\(s_i\vDash^S p, s_{i+1} = t(s_i).\)
(3) 不存在满足(2)的转换t,则对\(\forall j\ge i, s_j=s_i.\)

条件(3)将有穷的(可停机的)执行序列转化成了无穷序列,从而避免了有穷于无穷的序列分类。
如果状态s出现在了任一个执行序列中,称状态s是可达的(reachable).

将命题变量分配到状态上
设AP是一个有限的命题变量集合(有时也称为单位命题(atomic propositions))。
在一个转换系统中,我们定义映射\[L_p:(S\times AP ) \to \{True,False\}.\]换言之,从每个命题的角度来看,对于每个AP中的命题p,我们选取了一部分状态满足p,其余的状态不满足;或从状态的角度来看,我们对每个状态s,都选取了一部分AP中的命题变量,称s满足这些命题,同时不满足AP中的其余命题。
这如同对每个状态贴上了一些命题的“标签”。对于有标签的转换系统,可以记作\((S,\Delta,I,L_p,2^{AP}).\)
需要指出的是,可能会有多个状态拥有完全相同的命题标签集。这说明,命题标签可能并不完全给出状态或系统的性质,只需要能给出模型检验所需信息即可。

状态空间的组合(Combining State Spaces)
如上所言,一个系统可能由多个子系统组成。我们可以在每个子系统中定义局部状态(local state), 再将各个状态空间进行组合,得到全局状态(global state)空间。
在组合子系统的状态空间之前,我们先定义双射\(L_i : T_i\to\Sigma_i\),将每个子空间的全体转换(transitions)\(T_i\)映射为一个命名。这样做的目的是,有可能来自不同子空间的多个转换拥有相同的名字,当全局执行此命名的转换时,每个子空间的这种转换都要被执行。对于那些命名唯一(不与其它子系统的转换共享命名)的转换,称为局部转换(local transition).
设每个子系统的状态空间可以表示为\(G_i = \langle S_i,\Sigma_i,\Delta_i,I_i\rangle\). 我们总是假定\(S_i\cap S_j=\emptyset,i\ne j.\) 一般地,对于的局部状态空间\(G_i,G_j\),我们用符号\(G_i\circ G_j\)来表示其组合。

异步组合(asynchronous composition)是局部状态空间组合的一种,用符号\(||\)连结。异步组合要求不同子程序的转换只能交替执行。

线性观点与分支观点
在线性观点(Linear View)下,我们关注从初始状态开始,每个交错执行的状态序列能否满足待检验的要求。设程序P的全体可行的执行集合记作EP,满足待检验条件的交错序列记作集合SP。线性观点关注是否有\(EP\subseteq SP\),但不关注任两个执行序列之间的关系(比如是否有共同的前缀)。

而在分支观点(Branching View)下,选取I中一个初始状态作为根结点,构造一棵树,每个结点是状态空间中的一个状态,其后继为可以转换到的新状态。于是此树的每条从根结点出发的最长路径对应一个可执行的状态序列。这样的树可以提供比线性观点更多的信息,如从一个给定的状态(不一定是初始状态),我们可以检验是否之后的所有状态都满足给定的条件,或者是否存在某状态满足给定的条件。分支观点能够让程序有非确定性(nondeterministic)选择时的性质更加清晰。

一般地,当系统无需与外部环境交互时(称作closed systems),采用线性观点即可;而对于需要与环境交互的系统(称作open systems),采用分支观点更合适。

偏序观点
偏序执行给出了并发系统的一种更直观的描述。交错执行的序列可以视为定义在事件中的全序集,它不区分非确定性与并发性,即可能有一些可以同时进行的转换,在交错之行序列观点下必须排序。
请注意,以上我们定义的状态空间、转换系统都是在交错序列的观点下的,即一个转换结束后才能执行下一个。
一个偏序执行(partial order execution)可以定义为\((E,\prec)\). E是由事件(events)组成的集合,\(\prec\)定义了一个偏序关系,指出\(a\prec b\)当且仅当事件b不能在a结束前开始。
偏序集的性质:传递性,反身性与反对称性。
交错执行则定义了事件集上的全序集,任意两个事件要么\(a\prec b\),要么\(b\prec a\). 但在偏序执行中,如果两个事件之间没有定义偏序关系,则它们可以同时执行。利用偏序观点可以减少定义状态之间的先后次序,从而提升建模效率。

    所属分类:Formal Methods     发表于2022-01-30