|
个人信息Personal Information
副教授 硕士生导师
招生学科专业：
计算机科学与技术 -- 【招收硕士研究生】 -- 计算机科学与技术学院
软件工程 -- 【招收硕士研究生】 -- 计算机科学与技术学院
网络空间安全 -- 【招收硕士研究生】 -- 计算机科学与技术学院
电子信息 -- 【招收硕士研究生】 -- 计算机科学与技术学院
毕业院校：南京大学
学历：南京大学
学位：工学博士学位
所在单位：计算机科学与技术学院/人工智能学院/软件学院
办公地点：江苏省南京市将军大道29号
南京航空航天大学 计算机科学与技术学院楼118房间
联系方式：hujun@nuaa.edu.cn
Formal verification for AltaRica3.0 models based on SPIN
点击次数：
所属单位：计算机科学与技术学院/人工智能学院/软件学院
发表刊物：Int. Workshop Comput. Sci. Eng., WCSE
摘要：AltaRica is a kind of modeling language for safety critical systems, AltaRica3.0 is its latest version. There is still no corresponding formal verification method to analyze and verify the AltaRica3.0 model. The main work of this article is to analyze the AltaRica3.0 model by using a model test tool SPIN to analyze the different characteristics of AltaRica3.0 in relation to the previous version. Considering the basic structure of the underlying model GTS, based on the idea of AltaRica3.0 flattening to a GTS model, the core conversion rules of the AltaRica3.0 model to Promela model and a conversion framework are proposed. Based on the case analysis of the wheel brake system (WBS) in civil aircraft, the AltaRica3.0 model was established, and the Promela model was generated by the conversion rule. According to the safety requirements of the wheel brake system in 4761, SPIN is used to verify the system security attributes formally.
是否译文：否
发表时间：2017-01-01
合写作者：Li, Wanqian,Wang, Mingming,Zhang, Weijun
通讯作者：胡军