[1]李勇,曹子宁. 基于需求的形式化建模与验证方法研究[J].计算机技术与发展,2017,27(06):7-10.
　LI Yong,CAO Zi-ning. Investigation on Formal Modeling and Verification MethodBased on Specification[J].,2017,27(06):7-10.
点击复制

 基于需求的形式化建模与验证方法研究()
分享到：

《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]

卷:
27
期数:
2017年06期
页码:
7-10
栏目:
智能、算法、系统工程
出版日期:
2017-06-10

文章信息/Info

Title:
 Investigation on Formal Modeling and Verification MethodBased on Specification
文章编号:
1673-629X（2017)06-0007-04
作者:
 李勇; 曹子宁
 南京航空航天大学 计算机科学与技术学院
Author(s):
 LI Yong; CAO Zi-ning
关键词:
 ; 形式化方法; RSML-e ; 模型检测; NuSMV
Keywords:
 ; formal method; RSML-e; model checking; NuSMV
分类号:
TP31
文献标志码:
A
摘要:
 软件开发过程中需求阶段的错误比设计或实现阶段所引入的错误对系统的安全性与可靠性有更大的影响.为了能够在早期发现错误,降低开发成本,精确、简明地验证和规范软件系统和性质,在模型的形式化开发方法和模型检测的自动验证技术的研究基础上,提出了一种基于需求的形式化建模与验证的框架.运用基于四变量模型的需求状态机语言RSML-e建立了形式化模型,并给出了形式化的转换规则,将RSML-e模型转换为模型检测器NuSMV的输入模型,并进行了检测,建立起了一套整体的形式化开发框架,并以航空电子系统特定实例进行了建模与验证.验证结果表明,已建航电系统模型的安全性和可靠性是有效的.
Abstract:
 In the process of software development,the mistakes introduced in requirements phase have a more significant effect of the security and reliability than the phase of designing.In order to be able to detect the errors in the early phase of the software development and reduce development costs,and to describe the software system precisely and concisely,a formal modeling and verification framework has been proposed with the technology of automatic verification,in which the RSML-e model has been used and then the formal transformation rules have been given.Based on these rules,the proposed model can be transformed into the input model of the NuSMV,which is performed in model checking of the system.The specific instances of avionics system have been employed to implement modeling test experiments for verification.The experimental results show that the security and reliability of the established avionics system have been verified to be effective.

相似文献/References:

[1]高丽萍 褚伟.基于B方法的组件开发[J].计算机技术与发展,2007,(07):28.
　GAO Li-ping,CHU Wei.An Approach of Component Development with B Method[J].,2007,(06):28.
[2]张志锋 徐洁 邓璐娟 任雪利.基于B的UML形式化需求分析[J].计算机技术与发展,2007,(08):133.
　ZHANG Zhi-feng,XU Jie,DENG Lu-juan,et al.Requirement Analysis Formalized Using UML Based on B[J].,2007,(06):133.
[3]张志宏,吴庆波,邵立松,等.基于飞腾平台TOE协议栈的设计与实现[J].计算机技术与发展,2014,24(07):1.
　ZHANG Zhi-hong,WU Qing-bo,SHAO Li-song,et al. Design and Implementation of TCP/IP Offload Engine Protocol Stack Based on FT Platform[J].,2014,24(06):1.
[4]梁文快,李毅. 改进的基因表达算法对航班优化排序问题研究[J].计算机技术与发展,2014,24(07):5.
　LIANG Wen-kuai,LI Yi. Research on Optimization of Flight Scheduling Problem Based on Improved Gene Expression Algorithm[J].,2014,24(06):5.
[5]黄静,王枫,谢志新,等. EAST文档管理系统的设计与实现[J].计算机技术与发展,2014,24(07):13.
　HUANG Jing,WANG Feng,XIE Zhi-xin,et al. Design and Implementation of EAST Document Management System[J].,2014,24(06):13.
[6]侯善江[],张代远[][][]. 基于样条权函数神经网络P2P流量识别方法[J].计算机技术与发展,2014,24(07):21.
　HOU Shan-jiang[],ZHANG Dai-yuan[][][]. P2P Traffic Identification Based on Spline Weight Function Neural Network[J].,2014,24(06):21.
[7]李璨,耿国华,李康,等. 一种基于三维模型的文物碎片线图生成方法[J].计算机技术与发展,2014,24(07):25.
　LI Can,GENG Guo-hua,LI Kang,et al. A Method of Obtaining Cultural Debris’ s Line Chart Based on Three-dimensional Model[J].,2014,24(06):25.
[8]翁鹤,皮德常. 混沌RBF神经网络异常检测算法[J].计算机技术与发展,2014,24(07):29.
　WENG He,PI De-chang. Chaotic RBF Neural Network Anomaly Detection Algorithm[J].,2014,24(06):29.
[9]刘茜[],荆晓远[],李文倩[],等. 基于流形学习的正交稀疏保留投影[J].计算机技术与发展,2014,24(07):34.
　LIU Qian[],JING Xiao-yuan[,LI Wen-qian[],et al. Orthogonal Sparsity Preserving Projections Based on Manifold Learning[J].,2014,24(06):34.
[10]尚福华,李想,巩淼. 基于模糊框架-产生式知识表示及推理研究[J].计算机技术与发展,2014,24(07):38.
　SHANG Fu-hua,LI Xiang,GONG Miao. Research on Knowledge Representation and Inference Based on Fuzzy Framework-production[J].,2014,24(06):38.

更新日期/Last Update: 2017-07-20