闫倩倩，缪炜恺

（华东师范大学上海市高可信计算重点实验室，上海 200062）

0 概述

对于轨道交通系统、航空航天控制系统、核电控制系统等安全控制系统，其嵌入式控制软件是否能正确执行预期功能会影响到人身安全。因此，如何确保嵌入式控制软件的正确性成为研究人员的关注热点［1-3］。众所周知，形式化的需求规约可有效提高软件的质量，精确描述软件功能，并通过形式化建模执行严格的需求确认和验证，为后续的开发提供便利。

然而，如何把形式化方法应用到真实的工业软件中依然是一大挑战［4］。首先，目前缺乏建立形式化规约的方法。一方面，由于软件需求大多使用自然语言撰写而自然语言描述具有不准确性，软件工程师在构建需求规约时未必能准确且精确地描述系统功能；另一方面，领域专家几乎不可能使用复杂的形式化表示法描述系统需求，多数领域专家缺少坚实的离散数学基础，并且学习复杂的数学符号和证明技巧既费时又费力。其次，形式化的需求确认和验证大多由软件工程师主导，缺乏领域专家视角。传统的形式化验证侧重于使用形式化证明方法发现软件中的逻辑错误，如不一致性，但这对领域专家来说是难以理解的。

在形式化方法的需求建模阶段，根据不同的建模需求，大致有基于统一建模语言的方法UML［5］、基于属性描述语言的方法PSL［6］、基于规约描述语言的方法SDL［7］、基于逻辑的方法Z［8］和Event-B［9-10］、基于进程代数的方法CCS［11］和CSP［12］等。……