南京大学技术报告：Brief Introduction to UML 2.0（2/3）Activity & State Machine Modeling

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模型描述并发 ‰ 基于上一个观点描述的语义成为真并发语义

再谈Interleaving 用Interleaving的观点来理解并发，实际上是用非确定性特性代替系 统的并发特征。能够这样做的理由： 口保持动作的原子性： 在一定程度上对问题进行简化，以得到良好的代数性质。 目前的进程代数系统就是采用Interleaving模型描述并发，典型的 代表有CCS和CSP 基于Interleaving的模型描述并发的缺点是很多现象不能描述 口如组件对象内部多线程的并发执行 口毫无疑问，非确定性并不能代替并发 从CCS,CSP看Petri nets o Petri nets是描述真并发的典型系统，它没有CCS那样漂亮的演算 系统，但它可以刻画更多并发现象，如并发、矛盾及接触等等 Tian Zhang Nanjing University 6

Tian Zhang @ Nanjing University 6 再谈 Interleaving „ 用Interleaving的观点来理解并发，实际上是用非确定性 特性代替系 统的并发特征。能够这样做的理由： ‰ 保持动作的原子性； ‰ 在一定程度上对问题进行简化，以得到良好的代数性质。 ‰ 目前的进程代数系统 就是采用Interleaving模型描述并发，典型的 代表有CCS和CSP „ 基于Interleaving的模型描述并发的缺点是很多现象不能描述 ‰ 如组件对象内部多线程的并发执行 ‰ 毫无疑问，非确定性并不能代替并发 „ 从CCS, CSP看Petri nets ‰ Petri nets是描述真并发 的典型系统，它没有CCS那样漂亮的演算 系统，但它可以刻画更多并发现象，如并发、矛盾及接触等等

Petri nets defined in 1962 by Carl Adam Petri,extend state machines with a notion of concurrency Execution(transition)of Petri nets is nondeterministic,since multiple transitions can be enabled at the same time. Petri nets只给出模型，而没有演算。但是Petri nets,是一种真并发模 型，可以刻划更多的并发现象，如并发、矛盾及接触等。 Petri nets描述的系统中不存在一个统一的时钟，这一点也是网论的本质。 总之： [并发]Petri nets是一种真并发模型，用它可以描述更多的并发现象。针 对分布式对象系统中的多输入流并发现象，可考虑采用Petri nets [交互]Petri nets只有模型而没有没演算，利用它来验证系统的计算和语 义特性较为困难。不过，可以将Petri nets描述并发的思想应用到刻画系统 组件的交互之中。 Tian Zhang Nanjing University

Tian Zhang @ Nanjing University 7 Petri nets „ defined in 1962 by Carl Adam Petri, extend state machines with a notion of concurrency „ Execution (transition) of Petri nets is nondeterministic, since multiple transitions can be enabled at the same time. „ Petri nets只给出模型，而没有演算。但是Petri nets是一种真并发模 型，可以刻划更多的并发现象，如并发、矛盾及接触等。 „ Petri nets描述的系统中不存在一个统一的时钟，这一点也是网论的本质。 „ 总之： ‰ [并发] Petri nets是一种真并发模型，用它可以描述更多的并发现象。针 对分布式对象系统中的多输入流并发现象，可考虑采用Petri nets ‰ [交互] Petri nets只有模型而没有没演算，利用它来验证系统的计算和语 义特性较为困难。不过，可以将Petri nets描述并发的思想应用到刻画系统 组件的交互之中

CCS和CSP CCS和CSP是进程代数方法的代表，是描述通信和并发的演算 系统 口它们均以进程为计算单位，进程的基本组成是原子性动作 CCS和CSP都是既有模型又有演算，两者的不同点是： CCS用同步树(synchronizationtree)表示进程，或称为状态转移图， 而CSP用失败集(failureset)表示进程 CCS中，使用操作语义（互模拟语义）解释进程（的等价性）；而在CSP 中，则使用指称语义（失败语义）解释进程（的等价性） CCS和CSP等进程代数的演算系统均采用Interleaving模型描述 并发 标准的CCS和CSP均以同步通信的方式描述进程间的交互 有人在CCS的基础上进行一定的改进（从语法上，或从语义上）： 得到描述异步通信的演算系统 Tian Zhang Nanjing University 8

Tian Zhang @ Nanjing University 8 CCS和CSP „ CCS和CSP是进程代数方法的代表,是描述通信 和并发 的演算 系统 ‰ 它们均以进程为计算单位，进程的基本组成是原子性动作 „ CCS和CSP都是既有模型又有演算，两者的不同点是： ‰ CCS用同步树(synchronizationtree)表示进程,或称为状态转移图， 而CSP用失败集(failureset)表示进程 ‰ CCS中,使用操作语义(互模拟语义)解释进程(的等价性);而在CSP 中，则使用指称语义(失败语义)解释进程(的等价性) „ CCS和CSP等进程代数的演算系统均采用Interleaving模型描述 并发 „ 标准的CCS和CSP均以同步通信的方式描述进程间的交互 ‰ 有人在CCS的基础上进行一定的改进(从语法上,或从语义上), 得到描述异步通信的演算系统

Specification of Language (common A common technique for specification of languages firstly,define the syntax of the language; syntax defines what constructs exist in the language,and how the constructs are built up in terms of other constructs. secondly,describe its static and dynamic semantics. static semantics define how an instance of a construct should be connected to other instances to be meaningful dynamic semantics define the meaning of a well formed construct 口 well formed-fulfills the rules defined in the static semantics the meaning of a description written in the language is defined only if the description is well formed Tian Zhang Nanjing University

Tian Zhang @ Nanjing University 9 Specification of Language (common) „ A common technique for specification of languages ‰ firstly, define the syntax of the language; – syntax defines what constructs exist in the language, and – how the constructs are built up in terms of other constructs. ‰ secondly, describe its static and dynamic semantics. – static semantics define how an instance of a construct should be connected to other instances to be meaningful – dynamic semantics define the meaning of a well formed construct ß well formed - fulfills the rules defined in the static semantics ß the meaning of a description written in the language is defined only if the description is well formed

Specification of Language (graphic,such as UMI A specia/technique for specification of graphic languages if the language has a graphic syntax,it is important to define the syntax in a notation independent way firstly,to define the abstract syntax of the language - UML使用元模型给出抽象语法 ▣ secondly,to define concrete syntax by mapping the notation onto the abstract synfax -给出具体的Notation,可以是图形化的也可以是文本 thirdly,to describe its semantics 一UML中的语义是使用自然语言给出的 -UML中constructs的静态语义和动态语义是同时给出的 Tian Zhang Nanjing University 10

Tian Zhang @ Nanjing University 10 Specification of Language (graphic, such as UML) „ A special technique for specification of graphic languages ‰ if the language has a graphic syntax, it is important to define the syntax in a notation independent way ‰ firstly, to define the abstract syntax of the language – UML使用元模型给出抽象语法 ‰ secondly, to define concrete syntax by mapping the notation onto the abstract syntax – 给出具体的Notation，可以是图形化的也可以是文本 ‰ thirdly, to describe its semantics – UML中的语义是使用自然语言给出的 – UML中constructs的静态语义和动态语义是同时给出的