Page 229 - 《软件学报》2021年第6期

姚广宇 等:芯片开发功能验证的形式化方法 1803

n
们要进行 2 次运行时验证.
该方法与测试方法不同,测试方法无论是白盒、黑盒或者其他方法,其基本原理都是基于枚举所有的测试
用例的方法.虽然运行时验证方法也要通过选择不同的输入来检验模型是否满足期望的性质,但是一个性质能
够代表一些测试用例的集合而不是一个单一的测试用例;同时,一个性质能够描述程序执行的动态性质,例如安
全性( p)、活性(◊q)以及弱公平性( (p→◊q))等.

Fig.2 UMC4M verification tool
图 2 UMC4M 验证工具
5 信号灯控制电路系统的建模与验证

利用基于 MSVL 的运行时验证技术和 UMC4M 验证工具,可以进行模型和代码等价性的验证.本节以信号
灯控制电路系统为例,说明该方法在小电路系统验证上的可行性.
5.1 系统功能需求分析

实现一个简易交通信号灯控制电路系统,该系统能够确保东西主干道和南北支干道上的车辆能够交替安
全行驶.系统需要实现如下功能:系统关闭时,4 个方向黄灯持续亮,以警示来往车辆注意行驶.系统启动后,任意
方向的信号灯都是红黄绿交替闪亮,周期为 60s.为确保安全,主干道和支干道的绿灯不能同时亮.根据功能需求,
可以将整个系统划分为秒脉冲发生模块、分频计时器模块和状态控制模块,具体原理图如图 3 所示.

Fig.3 Schematic diagram of signal light control system
图 3 交通信号灯控制系统原理图

系统在启动前会一直保持警示状态,启动后,系统处于工作状态,并在达到相应的时间条件下进行状态变
换,如图 4 所示.

Fig.4 System state transition diagram
图 4 系统状态迁移图