计算机工程与科学

作者：姚袭欣, 章博, 陈香兰, 乔磊, 李曦

单位：（中国科学技术大学软件学院，安徽 合肥 230026）

关键词：Event-B,实时系统建模,时间触发系统,分布式多时钟,

基金：国家自然科学基金（61772482）；开放基金（OBCandETL-2020-02）

安全关键信息物理系统的时间属性建模和验证至关重要。Event-B模型验证避免了基于状态遍历模型检查方法的状态空间爆炸问题，验证时耗少，适用于高并发系统。然而，常规的Event-B方法缺乏时间语义表达结构，特别是缺乏对可提高系统可预测性的时间触发属性的支持。首先，介绍支持时间触发系统的抽象建模框架TTEB，从系统行为和实现2个抽象层次对时间属性进行建模和精化。然后，通过有序事件链组成的时间触发转移描述行为层时间触发属性；通过全局时钟到分布式本地时钟的精化和分解实现行为模型到实现模型的转化；运用时间触发转移建模分布式时钟周期同步。最后，基于从车跟车系统建模与验证说明方法的可用性和有效性。

来源：2023年第4期

《计算机工程与科学》期刊编辑部

查看计算机工程与科学杂志2023年第4期