面向轨交控制软件需求模型的量纲分析方法  

A Dimensional Analysis Method for the Requirements Model of Railway Control Software

作　　者：王尚 冯劲草 诸嘉逸 黄怿豪 郑寒月 徐想容 缪炜恺 张翔 蒲戈光 WANG Shang;FENG Jin-Cao;ZHU Jia-Yi;HUANG Yi-Hao;ZHENG Han-Yue;XU Xiang-Rong;MIAO Wei-Kai;ZHANG Xiang;PU Ge-Guang(Shanghai Key Laboratory of Trustworthy Computing,Shanghai 200062;National Defense Science and Technology Innovation Institute,Academy of Military Sciences,Beijing 100000;Shanghai Trusted Industrial Control Platform Co.,Ltd,Shanghai 200062)

机构地区：[1]上海市高可信计算重点实验室,上海200062 [2]军事科学院国防科技创新研究院,北京100000 [3]上海工业控制系统安全功能型平台,上海200062

出　　处：《计算机学报》2020年第11期2152-2165,共14页Chinese Journal of Computers

基　　金：国家自然科学基金(61872144);国家自然科学基金青年基金(61402178)资助.

摘　　要：嵌入式控制软件是当前诸多控制系统的核心部件.各类安全攸关系统,例如轨道交通系统、航空航天系统和核电控制系统等,其内嵌的控制软件的功能是否正确、安全直接关系到人们的生命与财产安全.经过长期的研究和实践,学术界和工业界都意识到系统需求作为软件工程生命周期的起始点,是确保软件质量的根本途径.因此,如何从源头上保障软件开发流程的正确性一直以来是软件工程领域重要的研究课题.然而,在工业界的软件开发中,系统需求的正确性只能靠人工审查来保证,人工审查自然语言系统需求的方法不但低效,而且无法确认需求的正确性,仍缺少一种对需求进行确认的形式化建模分析方法.需求确认是保障所构建的形式化规约质量的重要工程活动,而量纲分析作为需求确认中的一个重要手段,可以检查出因量纲的错误定义而产生的潜在缺陷,减少因量纲使用不当所造成的错误.基于此,我们针对轨道交通领域的特点,提出了一种基于形式化工程方法的需求建模与量纲分析研究,结合软件需求工程的基本原理,从原始需求出发逐步完成需求规约的构建,并给出了需求规约确认的其中一种方法,以确认软件需求规约准确、充分地描述人们对软件期望的功能,为该领域的需求分析提供保障.本文的主要贡献是:(1)提出了一种嵌入式控制软件需求建模的形式化工程方法;(2)提出了一种列车控制领域专用的需求描述语言ATPRDL(Automatic Train Protection Requirement Description Language),并对相应的需求文档进行建模;(3)针对嵌入式控制软件的特点,提出了一种领域专用的面向需求层的量纲分析方法,并构建了领域适用的量纲系统;(4)开发了一款工具用于支撑该方法的实际应用,使工程师可以快捷地进行量纲分析.通过应用本文提出的方法,我们对真实的轨道交通列车控制软件的需求进Embedded control software is the kernel component of today’s control systems.For the safety-critical control systems,such as the railway system,aerospace control system and nuclear power control system,the function and safety of the control software embedded in them are directly related to the safety of people’s lives and property.After long-term research and practice,both academia and industry realized that system requirements are the starting point of the software engineering life cycle and the fundamental way to ensure software quality.Therefore,how to ensure the correctness of software development process from the source has been an important research topic in the field of software engineering.However,in the software development of industry,the correctness of system requirements can only be guaranteed by manual review.Manual review of system requirements described in natural language is not only inefficient,but also unable to ensure the correctness of requirements.There is still a lack of a formal modeling analysis method to validate requirements.Requirements validation is an important engineering activity to ensure the quality of the formalized specifications constructed.As an important method of requirements validation,dimensional analysis can check out potential defects caused by wrong definition of dimension and reduce errors caused by improper use of dimensions.At present,the dimensional analysis in computer systems is mostly based on the code level and not applied in the requirements field,while some hidden errors in safety-critical embedded control systems are mostly caused by the wrong use of dimensions in requirements,which leads to software development errors from the source.Therefore,we propose a requirements modeling and dimension analysis method by according to the characteristics of the railway,which is based on formal engineering method.First,the requirements engineer converts the original requirements specifications into the requirements specifications described using the domain-specific r

关 键 词：软件工程 嵌入式软件 形式化方法 需求建模 量纲分析 需求确认 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]