为SOFL Specification自动生成消息序列(MSC)

• 作者: 王浩
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 形式化方法 SOFL MSC 模拟 规范校验
• 年，卷（期）: 2006,（16）
• 所属期刊栏目: 产品、研发、测试
• 页码范围: 114-117
• 页数: 4页
• 分类号: TP311
• 字数: 3495字
• 语种: 中文
• DOI: 10.3321/j.issn:1002-8331.2006.16.036

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王浩	上海交通大学软件学院	17	31	4.0	4.0