接口自动机.ppt

接口自动机与I O自动机的集成 接口自动机 接口自动机 InterfaceAutomata 是一种轻量级的形式模型 用于描述软件接口的时序行为 与传统模型不同的是 接口自动机不仅可以描述构件的行为 也可以描述构件对环境的假设 也就是描述环境的部分行为 同时在这个框架下 可以进行自动的相容性检查和精化检验 输入使能 指一个I O自动机在任何状态下都必须能够接受所有的输入动作 当多个I O自动机组合在一起时 任何一个输出动作都不会被阻塞或拒绝 乐观的角度 以一种交替的方式来定义自动机之间的精化 接口自动机一方面 一个自动机可以拒绝接受某些输入动作 另一方面 当多个自动机组合时 有要求一个自动机的输出动作不能被其他的自动机所拒绝 在多个接口自动机组合时 如果拒绝真的发生了 则试图加强对环境的限制 构造可以避免冲突的新的环境假设 只要存在一个环境可以避免冲突 就认为这些被组合的接口自动机是相容的 接口自动机的模型 接口模型 面向自上而下的基于构件的设计 I O自动机的模型 构件模型 面向自下而上的基于构件的验证 通过异常自动机可以将接口自动机和I O自动机联系起来 这意味着两种模型可以在一个统一的框架下很好地工作 异常自动机 ExceptionAutomata 一种特殊的I O自动机 接口自动机的相容性问题可以转化为异常自动机上的非空判定问题 而接口自动机的精化问题可以转化为异常自动机上的前向模拟问题 接口自动机 0 6 5 1 2 3 4 Ack Send Nack Send ack Msg Ok Nack Fail send ack nack a Usercomp b UserIIcomp 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是的一个环境 如果中的状态在中都是不可达的 那么就称E为 P Q 的一个合法环境 定义 相容性 如果接口自动机P和Q是非空的 可组合的 且存在一个 P Q 的合法环境 那么就称它们是相容的 两个接口自动机的并发组合是通过将它们的乘积限制在相容状态上而获得的 直观地讲 如果从一个状态出发存在环境可以阻止系统进入非法状态 那么就称该源状态为一个相容状态 定义 接口自动机的并发组合 设P Q为两个可组合的接口自动机 则它们的并发组合接口自动机P Q定义如下 精化关系 RefinementRelation 用来描述不同抽象级别的构件之间的一致性关系 在输入使能的情况下 一般采用路径包含或模拟的方式来定义精化关系 这样可以保证系统实现的所有行为都是系统规范所允许的 然而对于接口自动机这种非输入使能的形式模型来说 就不合适了 如果我们要求系统实现的合法输入动作集合也是系统规范的合法输入动作集合的子集 那么系统实现所适用的环境将比系统规范所适用的少 接口自动机精化关系定义在了一种新型的模拟关系 交替模拟的基础上 接口自动机P精化了接口Q的条件是 Q的所有输入步都能被P所模拟 而P的所有输入步都能被Q所模拟 精确的定义还要考虑P和Q的内部迁移 这些迁移的执行是相互独立的 小结 异常自动机是对经典的I O自动机模型的一种简单扩充 在这种新的形式模型的框架下 接口自动机的组合与精化都可以