基于SCADE的形式化验证技术的改进研究

李 耀，郭 进，孔令晶，宋海权

（西南交通大学 信息科学与技术学院，四川 成都610031）

0 引 言

安全苛求系统 （safety critical system）是指对安全负有直接责任的系统，一旦出现差错会造成人员伤亡，大宗的财产损失或严重的环境破坏等灾难性后果。随着计算机技术的快速发展，软件在安全苛求系统中承担的功能越来越多，重要性急剧上升。然而随着软件规模及复杂度的增加，软件缺陷密度呈几何级数增长，失效问题越来越多［1］。近半个世纪，安全苛求系统由于软件问题造成的损失几乎难以估量。在最短的时间内开发出高质量的安全软件已经成为一个十分重大的挑战，传统的软件开发方式已经不能满足需求，SCADE开发应运而生。

SCADE （safety critical application development environment），高安全性应用开发环境，是法国爱斯特尔技术公司运用基于模型的方式为高安全性系统提供的完整的解决方案，能自动生成满足安全特性的嵌入式代码，在航空、航天、国防以及核工业等安全苛求领域得到了广泛的应用。目前，在空中客车，安萨尔多，欧洲直升机等公司，SCADE开发方式都有成功案例。其中，空中客车在开发A340／500－600机型的飞行控制系统中自动生成了17万行代码，总体开发成本节约了50%。国内在航空和铁路信号等领域也积累了很多经验。形式化验证是SCADE的核心功能之一，在保证软件安全过程中具有不可替代的作用。但SCADE形式化验证模型中的安全特性观察器的正确性一直依靠设计者的经验保障，缺乏验证方式，本文利用SCADE开发的特点，对此问题提出了一种解决方案。

1 SCADE开发基础

1.1 SCADE开发的特点

SCADE基于同步编程理论，以Lustre语言为核心，覆盖了从需求到代码的所有开发流程，包括需求管理、需求建模、模型检查、模拟仿真、测试覆盖率分析、形式化验证、代码生成、文档生成等［2］。SCADE开发解决了传统开发的很多不足［3］，传统开发方式工作量大，效率低，投入高，验证难，设计可能存在歧义，维护及升级复杂；而SCADE开发十分方便，具有开发质量好、效率高，成本低、风险小、验证时间短，能够保证软件质量等优点，从传统的以 “代码”为核心转变为以 “模型”为核心，避免手工编码，开发人员关注软件需求的正确性，体现了软件设计的真正意义。

SCADE具有严格的数学语义，运用了Correct By Construction的设计理念，能够在软件开发初期清除系统的模糊性和二义性，由精确的需求规范自动生成嵌入式代码，实现了开发流程的高度自动化，确保软件的可靠性、安全性。SCADE使用编辑器严格准确地对需求进行建模，自动检查需求的安全性、完整性、一致性，通过仿真器和设计验证器保障模型安全的需求，最后由代码生成器自动生成面向工程的目标代码，整个开发过程具有可追踪性，开发流程如图1所示。

图1 SCADE开发流程

1.2 模型建立

建模是SCADE对需求的一种准确、无歧义的图形化表达，是SCADE开发的基础。SCADE支持数据流图和安全状态机两种图形方式建模。安全状态机常常用于描述离散系统的状态及逻辑结构，而数据流图善于描述数据的处理过程，反应时序及因果关系，常常用于连续系统的建模。

数据流图通过用户定义的输入变量接收外界信号，经过模型处理，再以用户定义的输出变量为接口输出给执行机构。图2为电梯运行方向的数据流图。

图2 电梯运行方向数据流

图2中，Des＿Floor表示用户输入的目标楼层，Cur－rent＿Floor表示电梯当前所处的楼层。数据流图表示：当目标楼层大于当前楼层时，电梯处于上升状态；当目标楼层小于当前楼层时，电梯处于下降状态；当目标楼层相等当前楼层时，电梯处于停止状态。

数据流图和安全状态机都建立在严格的数学模型基础之上，具有严格的数学语义，保证了设计模型的精确性、完整性、一致性和无二义性。SCADE把两套机制很好的结合在一起，能够适合不同类型的系统尤其是混合系统的开发。

1.3 模型验证

SCADE提供模拟仿真和形式化验证两种方式保障模型安全。一般，在系统开发早期使用模拟仿真，而在设计的最后阶段使用形式化验证。

模拟仿真通过观察模型对指定输入的响应行为判断设计是否符合预期需求，但不能保证模型满足所有的安全性要求，无法证明模型无错误，SCADE提供形式化验证弥补此不足。

形式化验证通过数学推理对系统做详尽的分析，具有完备性的优点，不需要任何测试用例，是保障模型安全的重要方法。SCADE形式化验证首先需要在设计验证器中建立安全特性观察器模型Observe。Observer是安全特性属性在SCADE中的图形形式化表达，其输出始终为一Bool变量，且应当为true。设计验证器连接待验证的设计模型Design和Observer模型，持续检测待验证模型的输入、输出信号，证明在所有周期及所有可能的场景下Observer都是正确的，如图3所示。

图3 形式化验证模型

1.4 目标代码

SCADE开发的最终目标是生成可信代码。SCADE代码生成器 KCG通过了 DO－178BA 级、IEC 61508SIL3、EN 50128 3／4和IEC 60880的认证，以模型作为输入，根据用户设定的参数，自动生成面向工程且满足安全特性的ANSI C或 Ada代码和可跟踪文件［4］。

KCG对使用数据流图方式建立的逻辑结构，生成的代码仍然保持了逻辑结构的特点。如A＋B＞0，KCG生成代码如下：

2 SCADE形式化验证的不足

SCADE形式化验证流程如下：

（1）提取安全特性属性。安全特性属性是保证系统不会发生危险的属性，一般来自软件需求或安全性标准等，如 “电梯移动过程中不能打开电梯门”；

（2）建立安全特性观察器模型，将安全特性需求转换为图形表达；

（3）验证安全特性属性。SCADE整合待验证模型和安全特性观察器模型，自动验证系统是否满足安全需求，如果发现冲突，安全特性观察器模型输出false警报信号，同时给出反例；否则输出true，给出安全证明，如图4所示。

提取安全特性属性和建立安全特性观察器模型由人工完成，对设计者的专业知识及技能有一定的要求。安全特性观察器模型的正确性关系到验证结果的有效性，但SCADE不能检测安全特性观察器模型的正确性，无法验证模型是否正确表达了设计者的意图。

图4 SCADE形式验证过程

对于模拟仿真，由于测试向量的数量关系到仿真的完备程度，SCADE提供模型测试覆盖率MTC定量分析仿真的完备程度。模拟仿真是对模型的验证，MTC是对模拟仿真的验证，是验证的验证。而对形式化验证，SCADE未提供类似的验证方法，安全特性观察器的正确性缺乏判断依据，完全依靠设计者的经验保障。形式化验证是保障模型正确性、安全性广泛使用的重要方法，安全特性观察器是SCADE形式化验证的核心模型，其正确性关系到软件的安全性。如果安全特性观察器模型建立错误，设计验证器将以错误的观察器模型验证系统，软件中的故障可能没有被检测，潜伏在系统中，在一些特定的环境下暴露并带来灾难性的危害，这在安全苛求系统中是不容许的。

3 解决方案

安全特性观察器建立错误一般有两种情况：

（1）安全特性属性提取错误；

（2）安全特性观察器模型建立错误。

第一种错误一般是由于设计人员对系统的安全特性或需求理解错误造成的，在实际开发中，由于设计人员的专业能力较强，此种错误相对较少。第二种错误是指设计人员对安全特征理解正确，但建立安全特性观察器模型出现错误，所建模型完成的功能和预期功能不一致，偏离了设计者的本意，在安全特征较为复杂时该种情况尤为常见。本文针对第二种错误提出一种验证方法。

安全特性一般是对系统状态或性质的要求，通常可以用逻辑描述的方式形式化表述，在SCADE中以安全特性观察器模型表述。如电梯的安全特性 “电梯移动时，电梯门不能处于开门状态；电梯门处于开门状态时，电梯不能移动”。电梯移动包括上升和下降两种情况，以A表示电梯上升，B表示电梯下降，C表示电梯门打开。此安全特性可以表示为的逻辑形式，即和C不能同时为真，安全特性观察器模型如图5所示。

图5 电梯安全特性观察器模型

安全特性观察器本质上也是SCADE的节点，只是多了一些特定的验证运算符，但验证运算符可以在编辑器中设计。图3是在编辑器中描述电梯的移动状态，图5是在设计验证器中描述电梯的安全特性需求，两者采用的都是数据流图，本质相同，所以设计验证器中的安全特性观察器模型可以移植到编辑器中。在编辑器中建立的安全特性观察器模型同编辑器中的其他模型一样，可以模拟仿真，形式化验证和用KCG生成代码，比在设计验证器中拥有更多的验证方式。

通过以上的分析，安全特性属性可以用逻辑描述的方式形式化表示，KCG对逻辑结构的模型生成的可信代码保持了逻辑特征，所以在编辑器中完成安全特性观察器模型后，通过KCG生成C代码，安全特性观察器模型转化为了C代码表现形式，即安全特性属性转化为了C代码表现形式。通过比较C代码的逻辑结构和安全特性属性的逻辑描述的结构，可以验证安全特性观察器模型是否实现预期功能，如图6所示。

图6 解决方案

改进后，SCADE形式化验证流程如下：

（1）提取安全特性属性；

（2）将安全特性属性抽象为逻辑形式，复杂表达式可以化简；

（3）在编辑器中使用数据流图方式对安全特性属性建模；

（4）根据安全特性属性的特点，可以使用仿真或形式化验证方式验证安全特性观察器模型；

（5）使用KCG生成C代码；

（6）比较步骤2抽象的逻辑形式和C代码逻辑结构是否一致，不一致表明安全特性观察器模型建立错误，返回步骤3完善模型；

（7）将安全特性观察器模型移植到设计验证器中，同常规验证流程继续验证，如图7所示。

图7 改进后的验证流程

4 案例分析

某系统由A、B、C这3个模块组成，模块B完成核心计算功能，A为B提供运行所需的控制信息，包括控制信号、状态信息、调试信号，其中状态信息包括正常状态和故障状态；C为B提供数据，包括通信数据和临时数据，如图8所示。

系统运行时，模块A的输出信息必须满足以下安全需求：

图8 系统结构

（1）控制信号开放且状态信息为正常状态；

（2）或控制信号关闭且调试信号开放；

（3）或状态信息为故障状态且调试信号开放；

（4）“控制信号开放且状态信息处于正常状态”不能与“调试信号开放”同时出现。

模块C的输出数据必须满足以下安全需求：

（1）接收到的通信数据不为 “－1”且收到确认信号；

（2）或接收到的临时数据不为 “－1”且收到确认信号；

（3）或接收的通信数据为 “－1”且临时数据为 “－1”。

以上为系统的安全需求，为以逻辑形式准确、无歧义表达安全特性，做如下约定：

（1）以A表示控制信号开放；

（2）以B表示状态信息处于正常状态；

（3）以C表示调试信号开放；

（4）以D表示通信数据为 “－1”；

（5）以E表示模块C收到数据确认信号；

（6）以F表示临时数据为 “－1”；

基于以上约定，系统的安全需求可以抽象为如下逻辑形式

（A∧B∨瓙A∧C∨瓙B∧C）（瓙（A∧B∧C））（瓙D∧E∨瓙F∧E∨D∧F）

通过逻辑运算，安全特性需求可以等价简化为：

（A∧B∨C）（瓙（A∧B∧C））（E∨D∧F）

在编辑器中对化简前后的安全特性属性建立安全特性观察器模型，如图9所示。

图9 系统安全特性观察器模型

图9（a）、图9（b）分别为简化前后的安全特性观察器模型，两者功能相同，但模型图9（b）结构更清晰，层次更清楚，相对简单，建模不容易出错，减小了验证失败的概率。模型图9（a）、图9（b）并未直接实现系统需要的安全特性，期望模型的输入并不是A、B、C等信息，而是控制信号、状态信息等系统信息。在模型中将逻辑常量A、B、C、D、E、F分别转换为对应的系统信息，建立系统的安全特性观察器模型如图10所示。

图10 系统安全特性观察器模型

经过语法、语义检测后，由KCG生成C代码，验证所建立的模型是否实现了预期的期望。图10所示模型生成的C代码如图11所示。

图11 系统安全特性模型C代码

函数kcg＿comp＿array＿char＿＊比较参数是否一致，如kcg＿comp＿array＿char＿3 （＆inC－＞Attestation，（array＿char＿3＊）＆States.Got）比较确认信号 Attestation是否等于Got状态，表示收到确认信号，以E表示；＿L22表示控制信号开放且模型处于正常状态，以A∧B表示；＿L16表示调试信号开放，以C表示；inC－＞Communication＿Data＝＝ ＿L11表示通信数据为－1，以D表示；＿L11＝＝inC－＞Temp＿Data表示临时数据为－1，以F表示。outC－＞ValidateOut是安全特性观察器模型的输出信号，通过C代码的特点，outC－＞ValidateOut的逻辑结构可表示为

此逻辑结构和简化后的安全特性需求的逻辑结构完全一致，说明安全特性观察器模型完成预期功能，模型建立正确，可移植到设计验证器中完成系统验证。

5 结束语

本文在充分研究利用SCADE开发特点的基础上，利用编辑器和代码生成器的特点，使用逻辑描述的方式形式化描述安全特性属性，对SCADE形式化验证中安全特性观察器模型的正确性提出了一种验证方法，改进了SCADE形式化验证技术，能够有效的检验安全特性观察器模型的正确性，保证模型安全，降低模型检验中人的主观性，在实际应用中取得一定效果，对安全苛求系统软件开发有一定的现实意义和实用价值。但对于复杂的模型，特别是使用了设计验证运算符的模型，此方法有一定的困难，下一步的研究将尝试自动生成逻辑描述表达式，自动完成验证。

：

［1］LU Minyan.Software reliability engineering ［M］.Beijing：National Defense Industry Press，2010 （in Chinese）. ［卢敏燕.软件可靠性工程 ［M］.北京：国防工业出版社，2010.］

［2］YAN Wenqing.The software design of flight control system for UAV based on SCADE ［D］.Nanjing：Nanjing University of Aeronautics and Astronautics，2008 （in Chinese）.［颜雯清.基于SCADE的无人机飞行控制软件设计 ［D］.南京：南京航空航天大学，2008.］

［3］LI Lei.Research on software testing method of CBTC zone controller based on SCADE ［D］.Beijing：Beijing Jiaotong University，2010 （in Chinese）.［李雷.基于SCADE的 CBTC区域控制器软件测试方法研究 ［D］.北京：北京交通大学，2010.］

［4］ZHANG Xiaochun，JIN Ping，SUN Quanyan.Modeling and autogeneration of C code on SCADE bench［J］.Software，2011，32 （5）：74－77 （in Chinese）.［章 晓 春， 金 平， 孙 全 艳.SCADE平台下的图形化设计和代码自动生成 ［J］.软件，2011，32 （5）：74－77.］

［5］ZHANG Lu.SCADE supported software development of zone controller in CBTC system ［D］.Beijing：Beijing Jiaotong University，2010 （in Chinese）.［张路.基于SCADE的CBTC区域控制器软件开发 ［D］.北京：北京交通大学，2010.］

［6］HU Gangwei，LI Zhenshui，GAO Yakui.A research on software development methods with SCADE ［J］.Journal of System Simulation.2009，20 （Suppl）：286－288 （in Chinese）.［胡钢伟，李振水，高亚奎.SCADE软件开发方法研究 ［J］.系统仿真学报，2009，20 （Suppl）：286－288.］

［7］LIN Feng.Research on SCADE－based formal verification technology［J］.Measurement ＆ Control Technology，2011，30（12）：71－74 （in Chinese）.［林枫.基于SCADE的形式化验证技术研究 ［J］.测控技术，2011，30 （12）：71－74.］

［8］LIN Feng.Implementation of trigonometric function by SCADE suite［J］.Computer Systems ＆ Applications，2012，21 （3）：228－231 （in Chinese）.［林枫.三角函数的SCADE Suite实现方法 ［J］.计算机系统应用，2012，21 （3）：228－231.］

［9］ZHOU Jiaming.Formal modeling and verification for the rail transit control system designed by SCADE base on PVS ［D］.Shanghai：East China Normal University，2011 （in Chinese）.［周佳铭.基于PVS对SCADE开发轨交控制系统的形式化建模与验证 ［D］.上海：华东师范大学，2011.］

［10］WANG Xin.Based on SCADE the software design of flight control system for UAV ［D］.Nanjing：Nanjing University of Aeronautics and Astronautics，2008 （in Chinese）.［王鑫.基于SCADE的无人机飞行控制系统软件设计 ［D］.南京：南京航空航天大学，2008.］

［11］ESTEREL Technologies.SCADE suite.［EB／OL］.［2012－11－01］.http：／／www.esterel－technologies.com／products／scade－suite／／.