| 基于SPIN内核的SDL模型检验工具设计 |
| |
| 引用本文： | 黄山,黄忠见,韩柯,王建伟.基于SPIN内核的SDL模型检验工具设计[J].数字社区&智能家居,2010(11). |
| |
| 作者姓名： | 黄山 黄忠见 韩柯 王建伟 |
| |
| 作者单位： | 中国人民解放军理工大学指挥自动化学院;中国电子系统设备工程公司研究所;西昌卫星发射中心指挥控制中心; |
| |
| 摘 要： | 规格描述语言SDL目前广泛应用于复杂通信协议和软件系统的建模。使用模型检验技术对SDL进行分析和验证可以检测出模型中的逻辑错误,大大提高SDL建模结果的精确性。论文研究了SDL的形式化语义SDL/PR中常用部分与模型检验工具SPIN的输入语言Promela之间的语义映射规则,并以此为基础开发了一个基于SPIN内核的SDL模型检验器SSMC Tool。
|
| 关 键 词： | SDL Model Checking 语义转换 SPIN 模型验证 |
Checking Tool Design of SDL Model Based on SPIN Kernel |
| |
| HUANG Shan,HUANG Zhong-jian,HAN Ke,WANG Jian-wei.Checking Tool Design of SDL Model Based on SPIN Kernel[J].Digital Community & Smart Home,2010(11). |
| |
| Authors: | HUANG Shan HUANG Zhong-jian HAN Ke WANG Jian-wei |
| |
| Affiliation: | 1.Institute of Command and Control;PLA University of Science and Technology;Nanjing 210007;China;2.The Mission Command and Control Center;Xichang Satellite Launch Center;Xichang 615000;3.Institute of China Electronic Systems Equipment Company;Beijing 100141;China |
| |
| Abstract: | |
| |
| Keywords: | SDL Model Checking semantic transition SPIN model verification |
| 本文献已被 CNKI 等数据库收录！ |
