摘要
标准UML(unifiedmodellanguage)状态图中缺乏对并行环境精确的动态语义,不利于对其所描述的并行环境进行形式化分析、验证和确认,而CSP(通信序列进程)语言具有严格的数学定义和分析方法,可用于验证模型的正确性。针对此特点,提出了结合CSP的UML状态图的形式语义,同时给出在并行环境下UML状态图的合并方法。根据形式语义对UML状态图在并行环境中应用的正确性(模型检验)进行分析,通过操作系统进程调度在并行环境下运行实例的结果表明了该形式语义的正确性。
Aimed at the lack of precise dynamic semantics of standard UML（unified model language） state diagram in the parallel en-vironment,and the parallel environment described is not conducive formal analysis,verification and validation.CSP（communication sequential process） language has the strict mathematics definition and the analysis method,which can be used in confirming the accuracy of the model.First the form semantics integrated CSP with UML state diagram and the merge method of UML state diagram under the parallel environment is proposed.Then the accuracy（model checking） of the form semantics of the UML state diagram under the parallel environment is analyzed.Finally the accuracy of this form semantics via the operating system process scheduling under the parallel environment is explained.
出处
《计算机工程与设计》
CSCD
北大核心
2011年第3期945-947,1022,共4页
Computer Engineering and Design
基金
国家自然科学基金项目(60373000
60474072Z)
国家自然科学基金重大发展计划项目(90818008)
广东省自然科学基金项目(07001774
04009465)
关键词
统一建模语言
状态图
通信序列进程语言
并行环境
形式语义
模型检验
unified model language
state diagram
communication sequential process
parallel environment
formal semantics
model checking
