Brief Introduction to UML 2.0 II -Activity State Machine Modeling (for SEG seminar) Tian Zhang Nanjing University,China October 2005 成
Brief Introduction to UML 2.0 II – Activity & State Machine Modeling Tian Zhang Nanjing University,China October 2005 (for SEG seminar)
Outline ■Foreword 0 OO visual modeling and formal methods Specification of UML2.0 language ■Activity Modeling ■ State Machine Modeling Tian Zhang Nanjing University 2
Tian Zhang @ Nanjing University 2 Outline Foreword OO visual modeling and formal methods Specification of UML2.0 language Activity Modeling State Machine Modeling
OO建模的图形化和形式化方法 Based on graphic mode,e.g.UML,MSC/SDL easy to use hard to translate,execute 口 对需求、设计的结果缺乏进行分析、验证的手段 Based on formalization,e.g.Z,VDM;logic,algebra,Petri nets, state machine 理论上可以解决上述问题，但复杂的形式使其难以推广 如何把直观自然的OO图形建模法和形式化技术相结合，是目前 普遍关注的问题（如何折中！） Tian Zhang Nanjing University 3
Tian Zhang @ Nanjing University 3 OO建模的图形化和形式化方法 Based on graphic mode, e.g. UML, MSC/SDL easy to use hard to translate, execute 对需求、设计的结果缺乏进行分析、验证的手段 Based on formalization, e.g. Z, VDM; logic, algebra, Petri nets, state machine 理论上可以解决上述问题，但复杂的形式使其难以推广 如何把直观自然的OO图形建模法和形式化技术相结合，是目前 普遍关注的问题（如何折中！）
常见的几种动态行为语义模型 基于逻辑的形式化方法 一阶线性/分支时序逻辑、模态μ演算、分布时序逻辑、TLA以及 线性逻辑 用来描述系统的生命期约束性质，如系统的安全性、活性、公平性及不 变性等 在逻辑的形式公理系统上，还可以进行系统的特性推理 基于刻画系统并发行为的模型和方法 CCS,CSP,ACP等基于进程代数 I/O自动机、Buchi自动机等自动机模型 Petri nets 口Actor模型 Tian Zhang Nanjing University
Tian Zhang @ Nanjing University 4 常见的几种动态行为语义模型 基于逻辑的形式化方法 一阶线性/分支时序逻辑、模态μ演算、分布时序逻辑、TLA以及 线性逻辑 – 用来描述系统的生命期约束性质,如系统的安全性、活性、公平性及不 变性等 – 在逻辑的形式公理系统上,还可以进行系统的特性推理 基于刻画系统并发行为的模型和方法 CCS,CSP,ACP等基于进程代数 I/O自动机、Büchi自动机等自动机模型 Petri nets Actor模型
关于并发的形式语义 并发性是指一个系统内部发生的两个事件之间不存在因果关系。 口因果关系不等同于先后关系，有因果必有先后，但反之则未必 0 在一个存在并发性行为的系统中没有统一的时钟 ▣用“不存在因果关系”来描述计算机网络的并发性是最合适的 对并发性的另外一种理解： 口并发性是指一个系统内部发生的两个事件之间的先后次序不确定 即，如果有多个进程在活动，那么这些进程中全体事件的集合一定可 以按照执行时间的先后排成一个全序 口Milner认为这样做在数学处理上比较简单 ▣基于这种观点描述的语义称为交叠式语义(interleaving semantics; CCS和CSP等进程代数的演算系统就是基于interleaving模型描述并发 口基于上一个观点描述的语义成为真并发语义。 Tian Zhang Nanjing University 5
Tian Zhang @ Nanjing University 5 关于并发的形式语义 并发性是指一个系统内部发生的两个事件之间不存在因果关系。 因果关系不等同于先后关系，有因果必有先后，但反之则未必 在一个存在并发性行为的系统中没有统一的时钟 用“不存在因果关系”来描述计算机网络的并发性是最合适的 对并发性的另外一种理解： 并发性是指一个系统内部发生的两个事件之间的先后次序 不确定 – 即，如果有多个进程在活动，那么这些进程中全体事件的集合一定可 以按照执行时间的先后排成一个全序 Milner认为这样做在数学处理上比较简单 基于这种观点描述的语义称为交叠式语义 (interleaving semantics); – CCS和CSP等进程代数的演算系统就是基于interleaving模型描述并发 基于上一个观点描述的语义成为真并发语义