博文
UML序列图的操作语义及其在模型精化中的一致性检查
||||
标题： UML序列图的操作语义及其在模型精化中的一致性检查
作者：赵也非 杨宗源 谢瑾奎 刘强
摘要：给UML赋予形式化的动态语义，就可以在需求、设计早期，对关键系统属性进行自动验证，进而保证软件质量，对软件开发设计起到指导作用。本文首先给出了UML序列图的基本构成元素和五种操作子的操作语义，提出了精确定义和pi演算转换规则，然后，以一个电话协议模型为例，给出了系统的UML序列图和状态图，并转换为pi演算代码，使用模型检测器，对系统的死锁性和互模拟等价性进行了自动验证，最后，在理论上对关键系统属性进行推理和演绎，给出了时间复杂度及其证明。本文提出的从UML序列图到pi演算的映射规则是双射的，可以应用于正向/逆向软件工程。
关键字：UML序列图；操作语义；pi演算；一致性检查；软件确保
发表在：科技论文在线（精品论文）
发表日期：2009年8月
网址：http://www.paper.edu.cn/paper.php?serial_number=200908-428
https://m.sciencenet.cn/blog-107188-252574.html
上一篇：基于扩展UML 状态图和Markov 过程的系统性能分析
作者：赵也非 杨宗源 谢瑾奎 刘强
摘要：给UML赋予形式化的动态语义，就可以在需求、设计早期，对关键系统属性进行自动验证，进而保证软件质量，对软件开发设计起到指导作用。本文首先给出了UML序列图的基本构成元素和五种操作子的操作语义，提出了精确定义和pi演算转换规则，然后，以一个电话协议模型为例，给出了系统的UML序列图和状态图，并转换为pi演算代码，使用模型检测器，对系统的死锁性和互模拟等价性进行了自动验证，最后，在理论上对关键系统属性进行推理和演绎，给出了时间复杂度及其证明。本文提出的从UML序列图到pi演算的映射规则是双射的，可以应用于正向/逆向软件工程。
关键字：UML序列图；操作语义；pi演算；一致性检查；软件确保
发表在：科技论文在线（精品论文）
发表日期：2009年8月
网址：http://www.paper.edu.cn/paper.php?serial_number=200908-428
https://m.sciencenet.cn/blog-107188-252574.html
上一篇：基于扩展UML 状态图和Markov 过程的系统性能分析
