软件体系结构形式化描述.ppt

1 软件体系结构 4 软件体系结构形式化描述覃征教授 SoftwareArchitecture THUSAGroup 2 内容概要 形式化描述简介软件体系结构的描述软件体系结构形式化描述实例 WRIGHTWRIGHT应用范例 THUSAGroup 3 抽象 认识事物本质的惯用法 抽象是人类对实际事物在针对某一特定关点下的简化突出我们希望认识的各个元素允许我们对关注的结构和行为进行辨识和分析在构建新的实例时可以作为蓝图 THUSAGroup 4 抽象实例 运动系统 THUSAGroup 5 抽象实例 动力系统 忽略了施力者和受力者的实体忽略了次要的环境作用 如地面 空气忽略了传力媒介突出了力和运动状态之间的关系 THUSAGroup 6 形式化的抽象 实际事物 形式化方法 THUSAGroup 7 内容概要 形式化描述简介软件体系结构的描述软件体系结构形式化描述实例 WRIGHTWRIGHT应用范例 THUSAGroup 8 软件体系结构的描述 软件体系结构和软件体系结构描述不同的两个概念软件体系结构是附属于系统之中 只要存在系统 体系结构就存在如 每个石头都会有重量软件体系结构描述是将体系结构可视化的手段和产物如 表示一个石头的重量 THUSAGroup 9 如何理解体系结构描述 THUSAGroup 10 体系结构描述方式 使用不同的策略和方法可对同一软件体系结构作不同的理解和描述如 描述一块石头的重量比较轻比另一块重一些大约2公斤四斤六两2 32Kg5 114751207磅 精确程度不同单位不同测量基准不同 描述方式不同 THUSAGroup 11 体系结构描述方式 体系结构描述方式标准语义丰富性语义精确性形式化程度主要描述方式非标准的图形符号UML模块接口语言MILADL Richness Preciseness Formalization O THUSAGroup 12 非标准图形符号描述 非标准图形符号描述用由矩形框和有向线段组合而成的图形表达工具 其中 矩形框代表抽象构件 有向线段代表辅助各构件进行通讯 控制或关联的连接件 特点语义丰富语义极不精确没有形式化基础用途商业展示设计草图 THUSAGroup 13 非标准图形符号描述 软件体系结构的非标准图形符号表示具有如下优点 直观形象简单易用 THUSAGroup 14 非标准图形符号描述 软件体系结构的非标准图形符号表示具有如下缺点 由于其术语和表达语义上存在着一些不规范和不精确 从而使得以矩形为基础的传统图形表达方法在不同系统和不同文档之间存在着许多不一致甚至矛盾 THUSAGroup 15 实例 EnterpriseJavaBeansArchitecture THUSAGroup 16 实例 Microsoft NetFrameworkArchitecture THUSAGroup 17 实例 DC LMP LinkManagementProtocolSoftware用于光纤网物理介质连接器的软件 THUSAGroup 18 UML 基于UML技术的软件体系结构描述方法1996年 Rational Catapulse公司发起workshop 倡议用UML进行体系结构描述和建模 特定领域体系结构建模 对UML中的stereotypes profiles等进行扩充 支持体系结构的表示2004年 UML2 0发布 增强了通用软件体系结构的描述能力 本质上UML是侧重于面向对象 OO ObjectOriented 软件系统设计的语言 THUSAGroup 19 UML特性 特点语义极其丰富语义相对精确有少量的形式化基础用途需求分析OO类设计行为设计和分析代码自动生成 THUSAGroup 20 UML与RUP UML本身只是一门语言 并不限定使用它的开发过程 但UML特别适合使用在RUP 统一开发工程 上 RUP定义了如何看待软件系统 视图 View UML定义了如何从某个角度描绘软件 图 Diagram THUSAGroup 21 RUP4 1视图 设计视图 实现视图 用例视图 进程视图 部署视图 系统综合者 性能 可扩展性 吞吐量 系统工程 系统拓扑结构 发布和安装 通讯 最终用户 功能性 词汇量 程序员 软件管理 RUPViews 分析员 测试员 动作 THUSAGroup 22 RUP4 1视图 用例图 UseCaseView 由专门描述可被最终用户 分析人员和测试人员看到的系统行为的用况组成 用例视图实际上没有描述软件系统的组织 而是描述了形成系统体系结构的动力 THUSAGroup 23 RUP4 1视图 设计视图 DesignView 又称逻辑视图 LogicView 包含了类 接口和协作 它们形成了问题及对问题解决方案的术语词汇 这种视图主要支持系统的功能需求 即系统提供给最终用户的服务 THUSAGroup 24 RUP4 1视图 实现视图 ImplementationView 包含了用于装配与发布物理系统的构件和文件 这种视图主要对系统发布的配置管理 它由一些独立的构件和文件组成 这些构件和文件可以用各种方法装配 以产生运行系统 THUSAGroup 25 RUP4 1视图 部署视图 DeploymentView 包含了形成系统硬件拓扑结构的节点 系统在器上运行 这种视图主要描述对组成物理系统部件分布 交付和安装 THUSAGroup 26 RUP4 1视图 进程视图 ProcessView 包含了形成系统并发与同步机制的线程和进程 该图主要针对性能 可伸缩性和系统的吞吐量 THUSAGroup 27 RUP视图的实现方式 Deployment Process Design UseCase Implementation RUPViews UseCaseDiagramSequenceDiagram ClassDiagramCompositeStructureDiagram DeploymentDiagram SequenceDiagramActivityDiagram ClassDiagramObjectDiagramSequenceDiagramActivityDiagramStateDiagramArtifactDiagram UMLDiagrams THUSAGroup 28 UML图实例 类图 ClassDiagram THUSAGroup 29 UML图实例 用例图 UseCaseDiagram THUSAGroup 30 UML图实例 序列图 SequenceDiagram THUSAGroup 31 UML图实例 协作图 CollaborationDiagram THUSAGroup 32 UML图实例 构件图 ComponentDiagram THUSAGroup 33 基于OO的软件体系结构描述方法 OO描述方法的优点 采用面向对象方法 更能反映软件体系结构的本质特征 提供了多个视图直观形象地反映体系结构元素所具有的功能 特征 通过类图 包图等反映体系结构的静态特征 并通过协作图 序列图 部署图等反映体系结构的动态特征 THUSAGroup 34 基于OO的软件体系结构描述方法 OO描述方法的缺点 缺少形式化的描述方法 造成设计人员由于对软件认识的角度 方法不同 生成的体系结构描述不尽相同 理解上存在的二义性 THUSAGroup 35 模块接口语言MIL MIL Module InterfaceLanguage 是将一种或多种传统程序设计语言模块连接起来描述软件的体系结构的方法 特点语义比较丰富 但局限在实现级别 层次较低语义精确 有编译器作保证没有或极少有形式化基础实例MicrosoftCOMIDLOMGCORBAIDL THUSAGroup 36 模块接口语言MIL MIL的优点 具有严格的语义基础 能够支持对较大的软件单元进行诸如 定义 使用 Definition Use 接口定义 InterfaceDefinition 和导入 导出 Import Export 等操作 一般来讲 MIL与实际的实现语言无关 只关注构件的对外表现协议以及构件之间的通讯关系 THUSAGroup 37 模块接口语言MIL MIL的缺点这些语言处理和描述的软件设计开发层次过于依赖程序设计语言 限制了它们处理和描述比程序设计语言元素更为抽象的高层次软件构架元素的能力 THUSAGroup 38 内容概要 形式化描述简介软件体系结构的描述软件体系结构形式化描述实例 WRIGHTWRIGHT应用范例 THUSAGroup 39 我们在哪里 THUSAGroup 40 软件体系结构的形式化描述 为什么需要形式化描述需要严格 精确无歧异的描述 以便在系统众多的涉众中进行交流需要演算的能力 使得在判断系统质量的时候可以由计算得出 而不是仅仅凭借经验推测需要进行体系结构分析自动化 THUSAGroup 41 软件体系结构的形式化描述 软件体系机构形式化描述风格风格的多样性问题风格的通用性问题风格的专用性问题 THUSAGroup 42 何谓形式化方法 形式化方法 借助抽象的方法将软件系统转化为数学模型如何抽象取决于关注点 THUSAGroup 43 形式化方法过程 软件系统 体系结构形式化模型1 体系结构形式化模型2 THUSAGroup 44 软件体系结构形式化基础 一阶谓词逻辑 FirstOrderPredicateLogic 集合论属性文法 AttributeGrammar 进程代数 ProcessAlgebra 通讯顺序进程 CSP CommunicatingSequentialProcesses 演算 Calculus Petri网状态机 StateMachine THUSAGroup 45 形式化方法的进化 ADL 纯形式化方法的不足形式化方法不能直接支持软件的各种概念 因此难以在实践中应用体系结构描述语言ADL ArchitectureDescriptionLanguage 应用通用的形式化方法对体系结构和风格进行建模和分析 在体系结构的抽象级上提供一个精确的语义 提供了强有力的分析能力 抽象和与实现的细节无关性 为体系结构元素定义了一系列符号 可以应用于实际的复杂系统的描述 THUSAGroup 46 ADL应当有什么功能 定义和描述结构概念 Capture 描述一个系统是如何被构件建立起来的 Construction 描述如何通过现有的构件生成新的系统 Composition 指导从多个不同的设计和实现中挑选最优方案 Selection 检验一个设计是否能够满足需求 Verification 检测一个需求对系统的隐含影响 Analysis 根据需求自动化构建系统 Automation THUSAGroup 47 ADL分类 根据结构分类隐式配置语言 ImplicitConfigurationLanguages 嵌入式配置语言 InlineConfigurationLanguages 显式配置语言 ExplicitConfigurationLanguages 前两者不能被认为是真正意义上的ADL THUSAGroup 48 ADL分类 续 根据研究范围分类研究体系结构配置结构的描述语言如Darwin CHAM ChemicalAbstractMachine 研究体系结构实例的描述语言如Rapide UniCon研究体系结构风格的描述语言如WRIGHT Aesop根据与实现细节的关系的描述语言实现无关语言 ImplementationIndependentLanguages 实现相关语言 ImplementationConstrainingLanguages THUSAGroup 49 几种ADL简介 THUSAGroup 50 几种ADL简介 续 Darwin采用 演算来分析 描述带有演化通信结构的并发系统 在 演算中 一个系统被表述成一组具有独立功能的进程集 集合中的每个进程可以与其它进程建立连接 每个连接都有一个连接名 Darwin采用 演算对系统行为进行建模 利用其强类型系统进行静态检查 THUSAGroup 51 几种ADL简介 续 XYZ ADL针对国内唐稚松院士提出基于时序逻辑的XYZ语言进行扩充 用来描述验证具有实时性 可靠性要求的软件体系结构 THUSAGroup 52 几种ADL简介 续 DSADL采用属性文法 AG 来形式化描述软件体系结构 传统的属性文法是在一上下文无关文法 ContextFreeGrammar CFG G VN VT P Z 上附加上下文有关的属性和规则 其中 VN是非终结符号集 VT是终结符号集 P是产生式集 Z是开始符号 假设G是规范CFG P中的产生式为p Xp 0 Xp 1 Xp np np 1 表示的右部所含符号的长度 Xp 0 VN Xp i V V VN VT 1 i np DSADL针对分布式软件的特征引入了并行描述机制 特殊的终结符号 条件产生式 THUSAGroup 53 几种ADL简介 续 OOADL采用Z语言形式化描述软件体系结构 其中Z语言是基于一阶逻辑 和集合论 等 的一种数学语言 OOADL以OO范例作为核心 增加了a kind of a part of 和 an instance of 等关键字来表示OO范例中的概括 聚集和实例化关系 THUSAGroup 54 几种ADL简介 续 WRIGHT采用CSP做为形式化描述语言 CSP是基于字母表 迹和拒绝集的概念 从形式上 CSP进程可以用一个3元组 A F D 表示 A表示字母表 Alphabet F表示失效 Failures D表示偏差 Divergences 进程的字母表是进程所参与的事件的集合 进程的迹是进程所允许的事件序列 THUSAGroup 55 通过ADL看软件 不同的ADL对软件的理解不同WRIGHT将软件理解为构件 连接器 端口 角色 以及这些元素之间的联系和约束 CSP的描述使其有利分析复杂行为 C2将软件理解为构件 端口和连接器 不过构件有且只有Top和Bottom两个端口 同时构件和构件之间仅通过Request和Notification两种信息进行通讯 适合描述交互式系统 ACME将软件理解为具有属性的构件和连接器 具有大多数ADL的共性元素 善于在不同ADL之间进行转换 THUSAGroup 56 通过ADL看软件 续 任何人都可以利用自己的关注点来看待并描述体系结构 即可以定义自己的ADL回忆 用自己习惯的方式来描述一块石头的重量比较轻比另一块重一些大约2公斤四斤六两2 32Kg5 114751207磅 你心目中的软件体系结构是什么样子 你是如何抽象软件 从而解决在设计和管理中的问题的 THUSAGroup 57 内容概要 形式化描述简介软件体系结构的描述软件体系结构形式化描述实例 WRIGHTWRIGHT应用范例 THUSAGroup 58 WRIGHT WRIGHT起源AFormalApproachtoSoftwareArchitecture RobertJ Allen Ph D Thesis CarnegieMellonUniversity TechnicalReportNumber CMU CS 97 144 May 1997 发展DynamicWRIGHT THUSAGroup 59 WRIGHT应用实例 应用 将一个字符串读入 修改字符串使其呈现大小写交替出现 然后输出如 Ilovethisgame ILoVeThIsGaMe假设系统设计管道过滤器系统 它分解输入流 使用过滤器Split 分别处理各子流 使用过滤器Upper和Lower 然后合并子流 使用过滤器Merge 本系统的模块分解图 侧重于实现 THUSAGroup 60 WRIGHT应用实例 WRIGHT眼中的系统 构件 连接器 图例 角色 端口 THUSAGroup 61 WRIGHT应用实例 WRIGHT语言描述 SystemCapitalize 定义一个系统Capitalize ComponentSplitportIn 输入协议 portLeft Right 输出协议 compspec Split构件规格说明 ComponentUpperportIn 输入协议 portLeft Right 输出协议 compspec Upper构件规格说明 ConnectorPipe Pipe连接器规格说明 Instancessplit Split upper Upper lower Lower merge Merge EndCapitalize 中内容为注释蓝色字为关键字 THUSAGroup 62 WRIGHT设计目标 支持体系结构配置的描述体系结构描述的最终目的是在高层抽象级上捕捉和利用一个系统的结构 它必须可以定义一个系统中的构件和构件之间的交互行为 支持体系结构风格的描述除了描述单一系统的体系结构 开发人员必须能描述一系列类似系统 这些体系结构风格提供了使用系统之间共性的方法 除此之外 在给定配置的情况下 两种描述必须可以结合在一起 这样我们就可以确定这两种描述是否符合同一种给定的风格 THUSAGroup 63 WRIGHT设计目标 续 支持属性分析描述行为的一个重要的目标是使用这种描述理解系统的属性 开发人员可以使用描述去分析系统或者风格 以确定系统是否满足他们的要求 支持在实际问题中的应用如果描述的符号仅仅能应用于有很大限制的环境中或者小系统中 那么这种描述将是不实用的 一种实用的符号表示可以扩展到描述复杂的实际问题 THUSAGroup 64 基于WRIGHT的形式化描述 作为一种体系结构描述语言 WRIGHT是根据构件 连接器和配置等基本体系结构的抽象而构造的 并为这些元素提供了清晰的记号 把构件形式化成计算 把连接器形式化成交互模式 下面分别介绍基于Wright的体系结构基本元素的形式化描述 THUSAGroup 65 基于WRIGHT的描述框架 构件 接口 接口类型 接口类型的参数化 接口类型约束 实例 计算 连接器 配置 附属 层次 风格 扩展风格 行为描述 事件 进程 并行组合 配置的拓扑结构 定义了配置可以共享的属性集合 定义新的风格 Wright体系结构形式化描述框架 THUSAGroup 66 基于WRIGHT的描述元素1 构件 构件 Component 一个构件描述了一个本地化 独立的计算 例如 在 管道 过滤器 系统中 一个典型的构件可以读取系统的所有输入并且把每个字母转换成大写字母 或者把一个输入流分成两个 每隔一个字符送到不同的输出 在一个数据库系统中 构件可能包括一个访问库和一个用户所请求的报表客户端 在WRIGHT中 对构件的描述包括两个方面 接口 Interface 和计算 Computation 一个接口有多个端口 Port 组成 每个端口表示构件参与的一种交互 在下例中 一个过滤器构件 分离过滤器 可能有三个端口 一个用于输入 另外两个用于输出 THUSAGroup 67 基于WRIGHT的描述元素1 构件 接口类型 InterfaceType 接口类型可以用于描述构件的端口 或者一个连接器的角色 在后者中 接口表示在角色中可能用到的端口接口的约束 例如 THUSAGroup 68 基于WRIGHT的描述元素1 构件 接口类型参数化WRIGHT允许把一个类型描述的任意部分变成预留空间 这些预留空间将在类型实例化是利用参数进行填充 因此 一个端口或者角色的类型 一种计算 一个接口的命名等等都可以参数化 THUSAGroup 69 基于WRIGHT的描述元素1 构件 接口类型参数化 续 除了在类型描述中预留空间之外 还有一种通过数字 Number 参数化类型描述 例如 ComponentSplitFilter nout 1 PortInput DataInputPortOutput1 nout DataOutputComputation 反复从端口Input读入数据 并将数据依次写入端口Output1 Output2 THUSAGroup 70 基于WRIGHT的描述元素1 构件 接口类型约束在WRIGHT风格描述中可声明在这个风格中的配置都必须遵循的属性 即约束 例如 实例名 类型名 取得类型的操作 类型名 意为 对于所有的连接器 它们的类型都必须是Pipe Pipe是连接器的一个类型 分隔声明和约束 THUSAGroup 71 基于WRIGHT的描述元素1 构件 一个 管道 过滤 系统实例 系统功能 读取一个字符流 并输出把每隔一个的字符转换成大写字母的字符流 THUSAGroup 72 基于WRIGHT的描述元素1 构件 SplitFilter构件描述 SplitFilter PortInput PortLeft PortRight THUSAGroup 73 基于WRIGHT的描述元素2 连接器 连接器一个连接器代表了构件集合内各种构件之间的交互 例如 一个管道代表了两个过滤器之间的一个序列流 一个过程的调用就是一种 调用 返回 模式控制的连接器 更复杂的连接还有数据库协议 例如 2 阶段提交和可靠安全网络消息的过滤 WRIGHT对连接器进行描述时 可以分为一个角色 Role 的集合和粘合 Glue THUSAGroup 74 基于WRIGHT的描述元素2 连接器 角色 Role 每个角色指定了在交互中单个参与者的行为 例如 在一个管道中有两个角色 数据源和接收器 Sink 同时 角色指定了交互中构件的参与者的期望 每种角色代表了一种构件将要做什么 例如 接收器角色代表了那个参与者所期望的行为 任何作为接收器的构件允许读取数据并且负责关闭连接 THUSAGroup 75 基于WRIGHT的描述元素2 连接器 粘合 Glue 一个连接器的粘合描述了参与者如何工作在一起创建一种交互 即连接器的粘合代表了完整的行为说明 实际上 我们把一个连接器解释成 如果真正的构件符合角色所指定的行为 那么构件的不同计算 Computation 将通过粘合而结合起来 如下例所示的一个管道例子 粘合描述了来自数据源的数据如何被传送到接收器 一个过程调用将表示调用者初始化一个调用 紧接着从过程定义器返回 连接器的粘合说明了构件的计算是如何组成一个更大的计算 THUSAGroup 76 基于WRIGHT的描述元素2 连接器 一个连接器描述实例 管道连接器 Pipe Source Sink Glue THUSAGroup 77 基于WRIGHT的描述元素3 配置 配置 Configuration 为了描述一个完整的系统体系结构 WRIGHT把对构件和连接器的描述结合在一起 形成配置 一个配置就是通过连接器把构件实例结合起来的一个集合 配置包括构件和连接器的生成 以及附属 Attachment 即将构件的端口和连接器的角色连接起来 THUSAGroup 78 基于WRIGHT的描述元素3 配置 实例因为在一个系统中可能多次使用给定的构件或者连接器 所以我们把先前的描述作为构件和连接器的类型 为了在一个配置中区分每种构件和连接器类型的不同实例 WRIGHT描述语言要求每个实例必须清晰并且具有唯一性 下例描述了一个具有实例声明的配置 定义构件连接器类型 定义构件连接器实例 连接端口和角色 THUSAGroup 79 基于WRIGHT的描述元素4 附属 附属 Attachment 在实例声明之后 就可以描述附属 Attachment 了 这样配置才算是完整的 附属说明了哪些构件参与哪些交互 从而定义了配置的拓扑结构 附属的声明把体系结构描述的每个元素结合在一起 例如 构件执行一种计算 Computation 这种计算的一部分是由端口 Port 指定的交互行为 这个端口与角色 Role 联系在一起 这说明了端口为了合法地参与连接器所指定的交互所必须遵从的规则 如果每个由各自的端口表示的构件遵从角色所规定的规则 那么连接器的粘合 Glue 则定义了机算是如何结合在一起形成更大的计算 实例见上例 THUSAGroup 80 基于WRIGHT的描述元素5 层次 层次WRIGHT支持层次描述 如下层次结构 服务器有内部结构 客户 服务器 THUSAGroup 81 基于WRIGHT的描述元素5 层次 与上图对应的层次描述 缩进可以帮助看清层次结构 接下页 THUSAGroup 82 基于WRIGHT的描述元素5 层次 定义次级构件实例Coordinator类型的c和SecurityManager类型的Security 将次级结构的构件和连接器连接起来 定义SecurityType的端口应该指向其内部结构的哪个端口 如图 THUSAGroup 83 基于WRIGHT的描述元素6 风格 风格WRIGHT可以用于定义体系结构的风格 一种风格定义了配置可以共享的属性集合 这些属性可以包括一个公共的词汇集和约束集 在WRIGHT中 通过声明一系列构件和连接器的类型引入公共的词汇集 并且使用声明的类型进行实例化说明 例如 管道 过滤器 风格将包括连接器类型 Pipe 的声明 然后 如果在 管道 过滤器 风格中声明一个配置 那么该配置就可以自动使用 Pipe 类型了 THUSAGroup 84 基于WRIGHT的描述元素7 扩展风格 扩展风格定义一种新风格的重要方法是把新风格描述成另外一种风格的子风格 如果新风格具有另外一种风格的所有约束条件 就可以新风格描述成该风格的子风格 例如 我们可以把管道风格定义成通过管道交互的线性序列的组合 这种风格具有 管道 过滤器 风格的所有限制 在定义子风格时 把父风格的名字放在子风格名字的后面 这样就可以包含父风格所定义的所有词汇和约束了 THUSAGroup 85 基于WRIGHT的描述元素8 行为 体系结构行为描述WRIGHT采用基于CSP 通信顺序进程 CommunicatingSequentialProcesses 的记号描述构件的行为和构件之间的协调关系 THUSAGroup 86 我们在哪里 THUSAGroup 87 行为描述法的要求 必须可以反映体系结构最常见的交互模式如过程调用 管道 事件 共享变量等等必须可以描述复杂的交互行为如哪一方先发起什么需求 然后另一方如何响应要求必须可以区分相似行为的细微不同例如同样是使用共享变量 具体是否需要初始化 如果需要 由谁来初始化等 THUSAGroup 88 CSP简介 CSP起源Hoare 1978解决序列化的进程描述以及这些进程并行执行时的交互问题理论成形Hoare Brookes Roscoe 1984以事件为基础的理论模型 构建动态的描述结构 并提出了进程间通讯的一些范式和准则 C A RHoare 1980年图灵奖获得者 THUSAGroup 89 CSP在哪里 Computation 用CSP精确描述 反复从端口Input读入数据 并将数据依次写入端口Output1 Output2 source x output1 x output2 x Computation THUSAGroup 90 CSP基本概念 事件 Event 引发其它事件或者被其它事件引发的情况 CSP中最基本的单位 事件集 Alphabet 对某一系统进行某种描述时所有相关的事件名称组成的集合 如果系统名为S 则事件集表示为 S进程 Process 连续交互发生的一组事件的整体 有一个特殊的进程叫STOP 表示系统停机 前束 Prefixing 由指定事件触发某一进程的关系 表示为e P选择行为 Alternative 在某种情况下 可以有多种进程发生 具体哪一种发生由环境决定不确定行为 Nondeterminism 在某种情况下 可以有多种进程发生 具体哪一种发生有进程自身决定 THUSAGroup 91 CSP实例 行为能被描述么 描述自动售货机的行为定义系统名称SVM 简单自动售货机 定义事件coin 投一枚硬币choc 得到一块巧克力定义本系统的事件集 SVM coin choc 系统简化本描述只和顾客投币并获取巧克力相关 因此其它的事件在此描述中均被忽略事件发生的精确时间被忽略无须区分一个对象本身触发和外界触发的事件 THUSAGroup 92 CSP表现SVM行为 当顾客投一个硬币 自动售货机就停止工作SVM coin STOP 当两个顾客分别投一个硬币后 均得到一块巧克力 之后再投币 自动售货机停止工作SVM coin choc coin choc STOP 当第一个和第二个硬币投下后 巧克力出来之前 不可以再投入新的硬币 巧克力出来之后 不投入新硬币 不会再有巧克力出来 即不可能有多于一个的硬币被连续投入 也不可能有多于一块的巧克力连续出来CSP前束操作符有右结合性 所以上式等价于SVM coin choc coin choc STOP 事件 前缀 进程 THUSAGroup 93 CSP的递归定义 现实当中有些对象在正常情况下的行为是永不停机的 用递归定义来描述这种情况对于系统SVM进程描述 SVM coin choc SVM THUSAGroup 94 CSP描述体系结构行为 引入成功完成的概念CSP中的STOP仅仅意味着系统停机 没有成功或者失败的意味 在体系结构描述中引入事件 成功完成 的概念 用 表示 WRIGHT定义 STOP事件可以伴随数据 通常e x表示输入一个参数 e x表示输出一个参数引入作用域 Scope 的概念存在于某一作用域中的进程仅在这个作用域中有效 效果等同于多元递归表示引入标签 Lable 的概念标签可以限定事件或者进程的归属者 其中对于某一单个事件的标签使用 例如l e 对于某一进程中的所有事件使用 例如l P通常使用 来表示所有通用的事件 如l 表示所有通用的事件加上l这个标签 THUSAGroup 95 CSP的优势和劣势 其他的可选方案Petri网 SDL I O自动机 状态图等在CSP中可以区分Alternatives和Nondeterminisms即由内部进行的决策和外部进行的决策是分开的CSP中有并行进程组合机制 可以表达一个符合多个进程描述的进程CSP拥有成熟的工具支持缺点CSP中 时间是不被考虑的CSP中 进程之间只存在触发的关系 THUSAGroup 96 CSP应用实例 我们用WRIGHT定义一个连接器ConnectorCSConnector Roleclient request x result y client Roleserver invoke x return y server Glue client request x server invoke x server return y client result y Glue client server Glue均为进程 request result invoke return为事件 X为参数client从使用者的角度来描述其行为 request和result均为client的事件 client是反复执行还是成功终止是由用户自己决定的 环境无法干涉server从服务提供者的角度描述其行为 invoke和return为server的事件 server是反复执行还是成功终止是由环境 这里特指用户 决定的glue从连接器的角度将两个角色的行为联系起来 Nondeterminism 表示由自身进行选择 Alternative 表示由环境进行选择 THUSAGroup 97 CSP连接端口和角色 端口行为也使用CSP表示例如ComponentDataUser portDataRead read DataRead definitionofotherports 端口定义了系统的实际行为 将一个构件的某个端口和一个连接器的某个角色连接起来 实际上端口将取代角色的位置 即角色只有占位符的意义 THUSAGroup 98 CSP深入 CSP具有复杂的演算和证明体系CSP模型 事件集 迹 拒绝集CSP是基于字母表 迹和拒绝集的概念 从形式上 CSP进程可以用一个3元组 A F D 表示 A表示事件集Alphabet F表示失效 Failures D表示偏差 Divergences 进程的事件集是进程所参与的事件的集合 进程P的字母表通常写成 P 进程的失效是迹与拒绝集组成的对 每个迹表示事件的有限序列 每个拒绝集是一个事件集 进程的迹是进程所允许的事件序列 例如 进程P 可以产生的迹是 a b aa ab ba 等等 迹的全集用Traces P 表示 事件的拒绝集可以用进程的失效对表示 失效对的第一个元素是进程的一个迹 第二个元素是进程在该迹上的一个拒绝集 CSP深入 续 一个失效是一个迹和一个事件集 对于一个给定的迹 可能存在多个拒绝集 因为拒绝集是子集闭合的 也就是说 如果一个构件拒绝了一个事件集 它就可以拒绝该事件集的任何子集 另外 一个进程可能可以分别拒绝事件的组合 但是并不是所有的组合 例如 进程可以拒绝事件a或者事件b 但是不能同时拒绝二者 于是 进程就有失效 a 和 b 但是没有 a b 然而 进程就有失效 a b 因为STOP选择意味着不发生任何事件 THUSAGroup 99 THUSAGroup 100 CSP深入 续 并发交织 interleaving 隐藏接口并行条件超时 timeout 和中断 interrupt 死锁检测 THUSAGroup 101 WRIGHT基于CSP语义进行的形式化校验 构件一致问题 连接器一致问题 风格约束 实例声明一致问题 激发器一致问题 定义1 测试2 测试3 定义2 测试5 测试6 测试7 测试4 测试8 测试9 测试1 一致问题测试 THUSAGroup 102 内容概要 形式化描述简介软件体系结构的描述软件体系结构形式化描述实例 WRIGHTWRIGHT应用范例 THUSAGroup 103 WRIGHT应用实例 实例内容概要AEGIS系统说明基于Wright的AEGIS体系结构描述 THUSAGroup 104 AEGIS系统说明 AEGIS武器系统是一个大型复杂的软件系统 它可以控制美国海军舰艇的许多防御功能 AEGIS系统的结构如下图所示 原始的体系结构描述由七个构件组成其中 实验控制模块提供了来自传感器和操作者的仿真输入 心跳 信号表示了仿真时间 跟踪数据被送往跟踪服务器 该服务器记录了当前在监视区域内所监视的移动物体 导弹 其他星体和潜水艇等等 规则创建模块接收描述活动的规则信息 GeoServer模块接收规则信息 来自规则创建模块 和跟踪信息 来自跟踪服务器 并根据几何模块判定哪一个轨迹和哪一个几何区域相交 这些信息 与轨迹和规则信息一起 被送往规则推理模块 在这个模块中决定采取任何什么行动 图中连线代表构件的交互 箭头表示了信息流的方向 THUSAGroup 105 AEGIS系统说明 AEGIS系统结构图 THUSAGroup 106 使用WRIGHT描述AEGIS 在WRIGHT描述中 我们将把体系结构中的每个元素当成一种类型 这些元素包括端口 角色 构件和连接器 1 接口类型一个系统中最小的构建块是一个接口的类型 接口的类型可以用于描述一个构件 端口 的接口或者交互协议上的约束 下图是一个接口说明实例 THUSAGroup 107 使用WRIGHT描述AEGIS 说明 ClientPullT是客户端构件端口的基本类型 表示一个客户可以使用open事件开始建立连接 ClientPullT的最初状态中包含一个进程的内部选择 ServerPushT进程是ClientPullT进程的补充 服务器期待着另外一方打开一个连接 然后 它将不断提供对这些请求的响应 直到关闭连接 THUSAGroup 108 使用WRIGHT描述AEGIS 2 连接器ClientServer连接器描述 见下图 客户服务器之间的交互事件间的关系 每一行对粘合 Glue 的描述都表示了事件对的联系 当客户端触发一个打开连接的事件时 服务器将观测到一个打开事件 THUSAGroup 109 使用WRIGHT描述AEGIS ConnectorClientServer RoleClient ClientPullTRoleServer ServerPushTGlue ClientServer连接器描述 上面的横线表示被激发的事件 InitiatingEvent 而不是观测事件 ObservingEvent THUSAGroup 110 用WRIGHT描述AEGIS 3 构件在AEGIS系统中 有三种构件 客户 例如 规则确认 服务器 例如 实验控制 和同时具有客户和服务器功能的构件 例如 GeoServer 下面我们将介绍Client构件 Server构件和配置描述 THUSAGroup 111 用WRIGHT描述AEGIS 说明 只要Client构件每个端口上符合ClientPullT协议 就可以完全控制其行为 为了简化起见 我们假设从打开它的每个连接开始 结束于关闭它的每个连接 在中间状态 进程UseService选择一个连接用于请求新的数据项 这个选择取决于客户 并且通过内部选择实现 构件1 Client描述 THUSAGroup 112 用WRIGHT描述AEGIS 构件2 Server描述 THUSAGroup 113 用WRIGHT描述AEGIS 构件2 Server说明 Server构件为一个或多个客户提供数据服务 对于每个客户 Server使用了ServerPushT协议 在这个协议中 每个客户都处于三个阶段 打开 用集合O表示 关闭 用集合C表示 或者 还未打开 THUSAGroup 114 用WRIGHT描述AEGIS 4 AEGIS系统体系结构配置通过上面介绍的接口 构件 连接器等体系结构基本元素并结合Wright的实例化等概念 可生成如下的AEGIS体系结构配置描述 THUSAGroup 115 小结 本章介绍软件体系结构的描述方法 讲述了语义基础 WRIGHT形式化描述以及形式化描述的验证 并介绍了基于WRIGHT的AEGIS系统体系结构的形式化描述实例 以期大家对软件体系结构形式化描述方法有初步的了解