【作者】 王建斌；

【导师】 韩江洪；

【作者基本信息】 合肥工业大学 ， 计算机应用技术， 2017， 硕士

【摘要】 矿井机车无人驾驶系统在设计时具有较高的安全要求,属于典型的安全关键系统。然而,在安全关键系统软件的设计过程中,传统上基于软件工程的方法,一方面,在需求分析阶段,由于自然语言编写的需求文档难以保证需求的完备性和一致性,另一方面,仿真和测试的也无法保证软件分析和验证的完全正确,这些因素给系统的安全带来了隐患。目前,针对传统软件工程方法在开发安全关键系统中遇到的问题,科研人员采用形式化方法来保证安全关键系统软件设计的正确性,进而提高系统的安全性。Event-B作为一种全新的形式化方法,具有逐步精化的建模策略和基于定理证明的模型验证方式。通过采用Event-B方法对安全关键系统软件进行建模与验证可以更早发现并修复系统的漏洞,对于安全关键系统软件的开发具有重要的借鉴意义。本文针对安全关键系统软件——矿井机车无人驾驶系统研发中遇到的问题,提出了基于Event-B形式化方法的解决方案,并选取矿机机车无人驾驶系统的核心功能——机车运行过程控制进行了形式化建模与验证的探索研究。分别对只具有离散属性的机车模式选择过程,和既具有离散属性又具有连续属性的机车自主行车过程控进行了基于Event-B方法的建模与验证。本文的研究结果表明,基于Event-B形式化方法可以准确的描述机车运行过程控制中的离散属性和连续属性需求。同时,通过定理证明的方式可以有效发现需求文档中存在的需求不一致性、需求缺失和需求模糊等问题,进而提早发现并修正这些漏洞,有效的提高了系统设计的正确性,为矿井机车无人驾驶系统的研发提供了一种借鉴,同时也为安全关键系统软件的研发提供了一种新的思路。更多还原

【Abstract】 As a typical safety critical system(SCS),the underground mine locomotive unmanned system(UMLUS)need to meet the requirements of high safety in designing processes.However,in the designing process of safety critical system software(SCSS),the traditional software engineering method is difficult to guarantee the requirements of completeness and consistency for the requirements document written by natural language,in the requirement analysis phase,and it also can’t analyze and verify the correctness of the software sufficiently in the simulation and testing phase.These factors bring hidden troubles to the safety of the system.In order to solve the problems which is introduced by traditional software engineering methods,formal methods have been adopted.It can ensure the correctness of design and development for SCSS and the safety performance of the system.As a new formal method,the Event-B provides the step-by-step refinement strategy for modeling and the theorem proving method for model verification,which can help discover and repair the vulnerability of the system in advance,and it is of great significance for the development of SCSS.For the problems in the development of SCSS,we present a formal method based on Event-B,and researche the modeling and verification of locomotive running process controlling,which is the core function of the UMLUS.And the modeling and verification based on Event-B are studied for the locomotive mode selection process with discrete attributes and the locomotive autonomous driving process with discrete attributes and continuous attributes.The results show that the formal method based on Event-B can accurately describe the discrete attribute and continuous attribute requirements for locomotive running process control.It can also effectively find out the requirement vulnerability,such as requirements inconsistency,requirements missing and requirements fuzzy.In summary,the Event-B method can discover and make up these vulnerabilities in advance.And it also improves the safety of the SCSS.As a new idea for the development of the SCSS,it also provides a reference to the development of UMLUS.更多还原