同济大学软件学院 杨 啸
随着嵌入式系统的广泛应用,产品的功能安全性已成为设计的重点问题之一,尤其在汽车领域。目前电子工业中最普遍的功能安全标准是IEC 61508[1]。
IEC 61508提出功能安全的概念,功能安全作为安全性的一部分,取决于系统或设备正确地响应其输入。功能安全性的保障是通过对潜在危险情况进行检测,并采取相应的安全措施或机制,来防止危害性事件发生或缓解其造成的危害。因此,监测产品是否发生故障对保证功能安全有重要意义。
在嵌入式环境的实时监测已有相关的研究,Donal Heffernan和Ciaran MacNamee将实时验证扩展到功能安全性的验证[2]。在他们的工作中,设计了硬件电路用于监测控制网(CAN)的消息,以实时验证安全性。,然而通过CAN总线无法监测软件内部变量,因此无法验证嵌入式应用本身是否发生故障。
本文旨在对嵌入式产品提供故障实时检测方案。设计了一个FPGA硬件模块,通过SPI(Serial Peripheral Interface)总线,在嵌入式产品运行阶段获取需要监测的变量信息,并根据FPGA内设计的验证模块检测故障是否发生。
Amir Pnueli[3]定义了线性时间逻辑(LTL),它为复杂系统的简化提供了强大的形式化体系。文献[4]使用LTL表达故障,并将其用于模型检验。
例如一个图像识别应用的故障是摄像头未启动或捕获图像超时或检测时间超时。用LTL公式表达如下:
为了能够在运行阶段检测应用的行为,监控模块需要获得相关的变量,被检测应用通过SPI总线将变量信息传输到监控模块。在研究中,假设传输是无误的并且足够快,以使验证能够实时地进行。
本设计使用Xilinx ZYNQ全可编程片上系统(All Programmable Systems on Chips, APSoCs)以软硬件协同的设计方法实现故障检测系统。系统主要包括五个功能模块:数据通信、数据解析、AP评估、公式验证和计时器。其中AP评估和公式验证使用FPGA实现,以保证结果输出的实时性,另外对于计时器,也使用FPGA硬件电路实现,以获得真实的物理时间。数据通信使用FPGA实现SPI从机接收功能,将接收到的数据存放在寄存器中,然后由软件部分读取并进行解析,获得所需变量的值。
系统整体架构如图1所示,ZYNQ分为PL和PS两部分,PL是可编程逻辑(Programmable Logic),由FPGA硬件电路实现;PS即处理器系统(Processing System),运行于ARM处理器。
图1 硬件监控模块架构框图
在接收到全局变量所需的值后,AP评估模块故障表达式的每个基本事件进行评估。故障表达式的最终结果在公式验证模块中实时评估,以检测故障是否发生。为了评估与时间有关的原子命题,在电路中设计了一个独立的时钟。外部接口用于向用户显示结果,或将结果发送给其他应用程序以实现安全性控制。
评估环境配置如图2所示。实时检测系统运行于ZYNQ,嵌入式应用通过SPI连接,并将检测结果显示在用户界面(PC)。
在实验中,通过在嵌入式应用运行期间注入故障,实时检测模块能够及时输出检测结果,并显示检测用时。根据检测结果和用时验证实时检测系统的有效性。
图2 实验评估环境
本实验使用前文提到的故障示例进行测试,测试结果如表1所示。其中第四项故障,由于并未设计在实时检测模块内,因此未检测到违反。检测结果表名实时检测系统能够在应用运行期间正确地检测到故障发生。
检测用时如表2所示。以视频常用帧率30fps,则图像采集周期为30ms,而故障检测用时远小于这一周期,可见FPGA具有良好的实时性。
表1 功能测试结果
表2 实时性测试结果(ms)
为了保证嵌入式产品的安全性,产品故障必须及时发现,否则当系统失效或事故发生,无法及时采取安全措施,或已经对环境和人员造成损害。
本文设计一个独立的实时检测系统模块,在软件的运行阶段,实时接收软件变量信息,并根据故障表达式判断故障是否发生。故障注入的测试表明,实时检测系统在软件发生故障时,能够准确和及时给出检测结果。
本文的研究工作设计了故障实时检测的原型系统,证明了在软件运行阶段检测故障的合理性,为保证产品安全提供有效依据。
[1]靳江红,吴宗之,胡玢.对功能安全基础标准IEC61508的研究[J].中国安全生产科学技术,2009,5(02):71-75.
[2]D.Heffernan,C.MacNamee,Runtime observation of functional safety properties in an automotive control network[J].Journal of Systems Architecture 68(2016):38–50.
[3]A.Pnueli,The temporal logic of programs,in:Foundations of Computer Science,1977,18th Annual Symposium on,IEEE,1977, pp.46–57.
[4]马琳. 基于故障树的航电软件系统安全性验证方法研究[D].南京航空航天大学,2012.