面向轨交控制软件需求模型的量纲分析方法王尚ｎ冯劲草ｕ诸嘉逸ｎ黄怿豪ｎ郑寒月＂徐想容Ｄ缪炜恺１ １张翔２ ）蒲戈光＾ｎ（ 上海市高可信计算重点实验室上海２ ０ ０ ０ ６ ２ ）（ 军事科学院国防科技创新研究院北京１ ０ ０ ０ ０ ０ ）３ ＞（ 上海工业控制系统安全功能型平台上海２ ０ ０ ０ ６ ２ 〉摘要嵌人式控制软件是当前诸多控制系统的核心部件． 各类安全攸关系统， 例如轨道交通系统、航空航天系统和核电控制系统等， 其内嵌的控制软件的功能是否正确、安全直接关系到人们的生命与财产安全． 经过长期的研究和实践， 学术界和工业界都意识到系统需求作为软件工程生命周期的起始点， 是确保软件质量的根本途径． 因此，如何从源头上保障软件开发流程的正确性一直以来是软件工程领域重要的研究课题． 然而， 在工业界的软件开发中， 系统需求的正确性只能靠人工审查来保证， 人工审査自然语言系统需求的方法不但低效， 而且无法确认需求的正确性， 仍缺少一种对需求进行确认的形式化建模分析方法． 需求确认是保障所构建的形式化规约质量的重要工程活动， 而量纲分析作为需求确认中的一个重要手段， 可以检查出因量纲的错误定义而产生的潜在缺陷， 减少因量纲使用不当所造成的错误． 基于此， 我们针对轨道交通领域的特点， 提出了一种基于形式化工程方法的需求建模与量纲分析研究， 结合软件需求工程的基本原理， 从原始需求出发逐步完成需求规约的构建， 并给出了需求规约确认的其中一种方法， 以确认软件需求规约准确、充分地描述人们对软件期望的功能， 为该领域的需求分析提供保障．本文的主要贡献是： （ １ ） 提出了一种嵌人式控制软件需求建模的形式化工程方法ｄ ２ ） 提出了一种列车控制领域专用的需求描述语言Ａ ＴＰ ＲＤＬ （ Ａｕ ｔ ｏｍａ ｔ ｉ ｃ Ｔｒａ ｉｎ Ｐｒ ｏ ｔｅ ｃ ｔ ｉ ｏ ｎ Ｒ ｅｑｕ ｉ ｒｅｍｅ ｎ ｔＤｅ ｓｃ ｒ ｉ ｐ ｔ ｉ ｏｎ Ｌ ａｎｇｕ ａｇｅ ） ， 并对相应的需求文挡进行建模；（ ３ ） 针对嵌人式控制软件的特点， 提出了一种领域专用的面向需求层的量纲分析方法， 并构建了领域适用的量纲系统以４ ） 开发了一款工具用于支撑该方法的实际应用， 使工程师可以快捷地进行量纲分析． 通过应用本文提出的方法， 我们对真实的轨道交通列车控制软件的需求进行了实验， 实验结果表明此方法具有良好的可用性， 并在实际的列车控制软件开发项目中， 展现了优于工业界传统手工审查方法的缺陷发现能力和时间效率．关键词软件工程； 嵌人式软件； 形式化方法； 需求建模； 量纲分析； 需求确认中图法分类号Ｔ Ｐ３ １ １ＤＯＩ 号１ ０． １ １ ８ ９ ７ ／ ＳＰ ． Ｊ ． １ ０ １ ６．  ２ ０ ２ ０ ． ０ ２ １ ５ ２ＡＤｉｍ ｅｎ ｓｉ ｏ ｎａｌ Ａｎ ａｌ ｙｓ ｉ ｓＭｅｔｈ ｏｄ ｆｏｒｔ ｈｅＲｅｑ ｕｉ ｒ ｅｍｅｎｔ ｓＭｏｄｅ ｌ ｏｆＲ ａｉ ｌｗ ａｙＣｏｎ ｔ ｒｏ丨Ｓｏ ｆｔｗ ａ ｒｅＷＡＮ ＧＳ ｈａ ｎｇｕＦ ＥＮ Ｇ Ｊ ｉ ｎ－ Ｃａｏ＂Ｚ Ｈ ＵＪ ｉ ａ－ Ｙ ｉｎＨ Ｕ Ａ Ｎ ＧＹ ｉ－ Ｈ ａ ｏ１ １ＺＨ Ｅ Ｎ ＧＨ ａ ｎ－ Ｙ ｕ ｅ１＇ＸＵＸ ｉａ ｎ ｇ－ Ｒｏｎ ｇ＂Ｍ ＩＡ ＯＷｅ ｉ－ Ｋａ ｉ１１Ｚ Ｈ Ａ ＮＧＸ ｉａ ｎｇ２ １Ｐ ＵＧ ｅ － Ｇ ｕ ａ ｎｇ１ ， ＇ ３＞ｌ ）（ Ｓｈ ａ ｎ ｇｈ ａ ｉ Ｋｅ ｙ Ｌａ ｂｏ ｒａ ｔ ｏ ｒｙｏ ｆＴｒｕ ｓ ｔ ｗｏ ｒｔ ｈ ｙ Ｃｏ ｍｐ ｕ ｔｉ ｎ ｇＳ ｈ ａ ｎｇｈ ａ ｉ２ ０ ０ ０ ６２ ）２）（ Ｎａ ｔ ｉｏ ｎ ａｌ Ｄｅｆｅ ｎ ｓ ｅＳｃ ｉｅｎ ｃ ｅａ ｎｄ Ｔｅ ｃｈ ｎ ｏ ｌ ｏｇ ｙ Ｉ ｎ ｎ ｏｖａ ｔｉｏ ｎ Ｉ ｎ ｓ ｔ ｉ ｔ ｕ ｔｅ＊  Ａ ｃａ ｄｅ ｍｙ ｏ ｆＭｉ ｌ ｉ ｔ ａ ｒｙ Ｓ ｃｉ ｅｎ ｃｅ ｓ＾ Ｂｅｉｊ ｉ ｎ ｇ１ ０ ０ ０ ０ ０ ）３ ）（ Ｓ ｈ ａ ｎｇｈ ａ ｉＴｒｕ ｓ ｔ ｅｄ Ｉ ｎ ｄ ｕｓ ｔ ｒｉ ａ ｌＣｏ ｎｔ ｒｏ ｌ Ｐ ｌａ ｔ ｆｏ ｒｍ Ｃｏ ． ，Ｌｔ ｄ －， Ｓ ｈ ａ ｎ ｇ ｈ ａ ｉ ２ ０ ０ ０ ６ ２ ）Ａｂ ｓｔｒａｃ ｔＥｍ ｂｅ ｄｄ ｅｄ ｃｏ ｎｔ ｒｏ ｌｓ ｏｆ ｔ ｗａ ｒ ｅｉ ｓ ｔｈ ｅｋ ｅ ｒｎ ｅ ｌ ｃｏｍ ｐｏ ｎｅ ｎ ｔｏ ｆｔ ｏｄ ａｙ，ｓ ｃ ｏｎ ｔ ｒｏｌ ｓｙ ｓｔ ｅ ｍｓ ． Ｆｏ ｒｔ ｈ ｅｓ ａ ｆｅ ｔ ｙ－ ｃｒｉ ｔ ｉ ｃａ ｌ ｃ ｏｎ ｔｒｏ ｌｓ ｙｓ ｔ ｅ ｍｓ ，ｓ ｕｃ ｈ ａ ｓ ｔ ｈｅ ｒａ ｉ ｌ ｗａ ｙ ｓｙｓ ｔ ｅｍ ，ａ ｅｒｏ ｓｐ ａｃ ｅｃｏ ｎｔ ｒｏ ｌｓｙ ｓ ｔ ｅ ｍ ａ ｎｄ收稿日期： ２ ０ １ ９ －１ ２－ ２ ４； 在线发布日期：２ ０ ２（Ｍ） ４－ １ ３ ． 本课题得到国家自然科学基金（ ６ １ ８ ７ ２ １ ４ ４ ） 、国家自然科学基金青年基金（ ６ １ ４０ ２ １ ７ ８ ） 资助．王尚， 硕士， 中国计算机学会（ ＣＣＦ ） 会员， 主要研究方向为需求工程、形式化工程方法． Ｅ－ｍ ａｉ ｌ ：  ４ ６ ６ １ ６ ８ ２ ２ ５ ＠ ｑ ｑ ． ｃｏｍ． 冯劲草， 博士， 中国计算机学会（ ＣＣＦ ） 会员， 主要研究方向为需求工程、形式化工程方法． 诸惠逸，博士， 中国计算机学会（ ＣＣＦ ） 会员， 主要研究方向为深度神经网络的验证． 黄怿豪， 博士， 中国计算机学会（ ＣＣＦ） 会员， 主要研究方向为需求工程、形式化工程方法． 郑寒月， 博士， 中国计算机学会（ ＣＣＦ ）会员， 主要研究方向为需求工程、自然语言处理． 徐想容， 硕士， 主要研究方向为自然语言处理． 缪炜恺， 博士， 副教授， 中国计算机学会（ ＣＣＦ）会员， 主要研究方向为形式化工程方法． 张翔（ 通信作者） ， 硕士， 助理研究员， 主要研究方向为软件质量保障． Ｅ－ ｍａ ｉ ｌ ： ｊａｒ ｃｈｅｒ ｓ ＠ １ ６ ３ ．ｃｏ ｎｘ蒲戈光， 博士， 教授， 中国计算机学会（ ＣＣＦ） 会员， 主要研究领域为程序分析、软件验证．１ １ 期 王尚等： 面向轨交控制软件需求模型的量纲分析方法 ２ １ ５ ３ｎ ｕｃ ｌ ｅ ａｒｐ ｏｗ ｅｒ  ｃｏ ｎｔ ｒｏ ｌｓ ｙｓ ｔ ｅｍ ，ｔ ｈ ｅｆ ｕ ｎ ｃ ｔ ｉ ｏｎ ａ ｎ ｄ ｓ ａ ｆ ｅｔ ｙｏｆ  ｔｈ ｅ ｃｏｎ ｔ ｒｏｌ ｓ ｏ ｆ ｔｗ ａ ｒ ｅ ｅｍ ｂｅ ｄ ｄ ｅ ｄ ｉ ｎ ｔ ｈ ｅｍａ ｒ ｅｄ ｉｒ ｅｃ ｔｌ ｙｒ ｅｌ ａ ｔ ｅｄｔ ｏ ｔｈ ｅｓ ａ ｆｅ ｔ ｙｏｆ ｐ ｅｏ ｐｌ ｅ’ｓｌ ｉ ｖｅ ｓａ ｎ ｄｐ ｒ ｏｐ ｅｒ ｔｙ ．Ａ ｆ ｔ ｅ ｒ ｌ ｏｎ ｇ－ｔ ｅｒ ｍｒ ｅ ｓｅ ａ ｒ ｃ ｈａ ｎ ｄｐｒａ ｃ ｔ ｉｃ ｅ ，ｂ ｏｔ ｈａ ｃａ ｄ ｅｍｉ ａａ ｎｄｉ ｎｄ ｕ ｓ ｔ ｒ ｙ ｒ ｅａ ｌ ｉ ｚｅ ｄｔ ｈ ａ ｔｓｙ ｓ ｔ ｅｍ ｒ ｅ ｑｕ ｉｒ ｅ ｍ ｅ ｎｔ ｓ ａ ｒ ｅ ｔ ｈ ｅｓ ｔ ａ ｒ ｔ ｉｎ ｇ ｐｏ ｉ ｎｔｏｆｔｈ ｅ ｓｏ ｆ ｔｗ ａ ｒ ｅ ｅｎｇｉ ｎ Kn
惤鼂ｅ