论文部分内容阅读
标准UML（unifiedmodellanguage）状态图中缺乏对并行环境精确的动态语义,不利于对其所描述的并行环境进行形式化分析、验证和确认,而CSP（通信序列进程）语言具有严格的数学定义和分析方法,可用于验证模型的正确性。针对此特点,提出了结合CSP的UML状态图的形式语义,同时给出在并行环境下UML状态图的合并方法。根据形式语义对UML状态图在并行环境中应用的正确性（模型检验）进行分析,通过操作系统进程调度在并行环境下运行实例的结果表明了该形式语义的正确性。