使用ACL2进行B组件复用及GeneSyst工具在B事件规范行为分析中的应用

### 使用ACL2进行B组件复用及GeneSyst工具在B事件规范行为分析中的应用 #### 1. 使用ACL2进行B组件复用 ##### 1.1 理论基础 在相关研究中，假设存在S′，其写框架为WS - WT，并且对于同一框架上的任何谓词P，都有[S′]P ⇔ [S]P。在flat(S; T)的定义中使用的S/WS - WT满足这些要求。由此，当S′ ≡ S/WS - WT时，可以得出flat(S; T)等价于S; T，即[S; T]Q ⇔ [flat(S; T)]Q。 ##### 1.2 案例研究 - **串行总线控制器** - **系统开发流程**：对于串行总线控制器（标准SAE J1708），B开发首先在非常抽象的层面上对整个系统进行建模，以指定重要属性。通过细化得到协议模型，最后再次细化以获得寄存器传输级别的控制器描述（BHDL级别）。从BHDL，电路被转换为VHDL，进行模拟和综合。 - **验证过程**：该案例研究的目标不是验证电路的VHDL描述，而是用一个已知正确的非平凡示例来确认方法的有效性。从在B中验证的BHDL电路描述开始，将其分别转换为ACL2和VHDL（使用KeesDA开发的转换器）。VHDL描述约400行，使用140个内部信号，然后使用TIMA开发的转换器将该VHDL描述转换为ACL2。此时有同一电路的两个ACL2描述，验证它们的等价性。 - **验证结果**：ACL2模型中，VHDL设计有148个函数，BHDL描述有21个函数。为进行等价性证明定义了65个定理，并使用了一个已定义的关于位向量及其操作的库。证明过程并不困难，仅需几小时的人工时间（而原始B开发需要数周），在特定处理器上证明本身用时17.23分钟。手动修改模型引入错误，特别是类型和算术表达式方面的错误，ACL2能够检测到这些错误。 |模型|函数数量| | ---- | ---- | |VHDL设计的ACL2模型|148| |BHDL描述的ACL2模型|21| - **计数器** - **模型定义**：将BHDL模型转换为ACL2后，定义了相应的sim - step、system、hyp - input和hyp - st函数。以下是计数器的BHDL模型的sim - step和system函数定义： ```lisp (defun b-sim-step (in st) (let ((reset (nth *b-reset* in)) (rst (nth *b-rst* in)) (compt (nth *b-compt* st))) (list (B compt compt rst reset) (B alm compt reset)))) (defun b-counter (input st) (if (atom input) st (b-counter (cdr input) (b-sim-step (car input) st)))) ``` - **双模拟关系证明**：有两个ACL2模型，一个对应VHDL设计，另一个对应BHDL模型，且两个模型都是周期精确的。为证明两个模型之间的双模拟关系，首先定义关系Sim ⊆ STVHDL × STBHDL。证明Sim是模拟关系分两步：一是从任意状态开始，时钟周期后，当reset为1时，两个模型处于符合Sim的相似状态；二是从相似状态开始，消耗相同输入（考虑必要的类型转换）后，两个模型仍处于相似状态。通过对时钟周期数（即输入列表的长度）进行归纳证明。还定