接口自动机.pptVIP

接口自动机与I/O自动机的集成 接口自动机 接口自动机(Interface Automata)是一种轻量级的形式模型，用于描述软件接口的时序行为。与传统模型不同的是，接口自动机不仅可以描述构件的行为，也可以描述构件对环境的假设，也就是描述环境的部分行为。同时在这个框架下，可以进行自动的相容性检查和精化检验。 输入使能：指一个I/O自动机在任何状态下都必须能够接受所有的输入动作。 当多个I/O自动机组合在一起时，任何一 个输出动作都不会被阻塞或拒绝。 乐观的角度：以一种交替的方式来定义自动机之间的精化。 接口自动机一方面，一个自动机可以拒绝接受某些输入动作；另一方面，当多个自动机组合时，有要求一个自动机的输出动作不能被其他的自动机所拒绝。 在多个接口自动机组合时，如果拒绝真的发生了，则试图加强对环境的限制，构造可以避免冲突的新的环境假设。只要存在一个环境可以避免冲突，就认为这些被组合的接口自动机是相容的。 接口自动机的模型：接口模型，面向自上而下的基于构件的设计。 I/O自动机的模型：构件模型，面向自下而上的基于构件的验证。 通过异常自动机可以将接口自动机和I/O自动机联系起来，这意味着两种模型可以在一个统一的框架下很好地工作。 异常自动机(Exception Automata)：一种特殊的I/O自动机。接口自动机的相容性问题可以转化为异常自动机上的非空判定问题，而接口自动机的精化问题可以转化为异常自动机上的前向模拟问题。 接口自动机 0 6 5 1 2 3 4 Ack? Send! Nack? Send! ack? Msg; Ok! Nack? Fail! send ack nack (a)User comp (b)User II comp msg send Nack? Send! Ok; Ack? send ack nack 0,0 1,1 1,2 1,3 1,4 1,5 假设有个软构件(comp)提供消息传递中继服务。和一个用户构件user，它总能够成功地进行消息传递。 当comp和user并发执行时，user构成comp环境的一部分。类似于I/O自动机的并发组合，可以定义接口自动机上的乘积操作，如图(a)。 当采用接口自动机的另一种方式，即“乐观”的方式，来处理非法状态，则如图(b)。 定义（I/O自动机） 一个输入/输出自动机是一个结构 其中： 是P的状态集合； 是P的初始状态集合； 是两两互不相交的动作集合； 是一个迁移关系，描述一组迁移步； Part(A)是一个 上的等价关系，最多含有可数多个等价类。 定义（接口自动机）一个接口自动机是一个结构 其中： 是P的状态集合； 是P的初始状态集合； 是两两互不相交的动作集合 ； 是一个迁移关系，描述一组迁移步。 我们可以定义接口自动机环境下的一些概念和记号，如 等。 并发组合与相容性 定义（可组合） 如果下列条件满足，则称接口自动机P和Q是可组合的。 记 shares(P,Q)= 首先定义接口自动机上的乘积操作。这个操作与I/O自动机上的并发组合操作是一致的，不同之处在于：每一个I/O自动机都是输入使能的，而接口自动机却不一定是。 定义（接口自动机的乘积） 任给两个可组合的接口自动机P和Q，他们的乘积定义为如下所示的接口自动机 定义（非法状态）给任意两个可组合的接口自动机P和Q， 的非法状态集合Illegal(P,Q)定义如下： 当接口自动机P和Q的乘积是闭的（没有外部动作）时，如果 的所有状态都是不可达的，那么我们就称P和Q是相容的；当 是开的（存在外部动作）时，当存在一个环境使得 中的所有非法状态都不可达时，就称P和Q是相容的。这样的环境称为合法环境。 定 义（环境）接口自动机R的一个环境是满足下列四个条件的一个接口自动机:(1)E与R是可组合的；(2)E非空； (3) ; (4)Illegal(R,E)= 。 定义（合法环境）设P,Q为两个可组合的接口自动机、E是