10.3321/j.issn:1002-8331.2006.16.036
为SOFL Specification自动生成消息序列(MSC)
形式化方法以其精确的描述能力,可验证性,和自动化潜力而得到了人们的关注.特别是在一些对安全性要求非常高的领域,已经有了很多成功的案例.但他始终没有在业界得到推广.原因之一就是基于数学符号的形式化语法十分晦涩难懂,这给开发人员之间,开发人员和客户之间的交流造成了巨大的障碍.我们认为要解决这一问题,就需要为形式化规范提供更直观,更为大家所熟悉的行为表现方式.文章介绍如何自动生成MSC(message sequence chart)来描述SOFL(Structured Object oriented Formal Language)[12]specification的行为.通过用MSC来动态模拟规范的行为的执行过程,可以很好地帮助人们理解规范内容,这对于规范校验(specification validation)有重要的意义.此外,我们为支持这一MSC自动生成过程编写的一款工具原形,也会在文中作简要介绍.
形式化方法、SOFL、MSC、模拟、规范校验
42
TP311(计算技术、计算机技术)
2006-07-19(万方平台首次上网日期,不代表论文的发表时间)
共4页
114-117