一种基于Event-B语言的时间触发系统建模方法

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

基于时间自动机的AADL端到端流规约验证方法

体系结构分析及设计语言(AADL)作为一种标准且直观的实时系统分析与设计工具，可以为系统设计、分析、验证、自动代码生成等关键环节提供统一的抽象表示。然而，AADL模型采用仿真的验证方法无法得到精确的端到端延迟验证结果，尤其是对于资源动态分配的实时系统。为解决结果不精确的问题，可结合基于系统有穷状态空间遍历的模型检验方法。首先，将实时系统AADL模型转换为时间自动机(TA)模型，以TA为理论体系进行模型检验。其次，基于反应链的需求分类定义端到端延迟需求表达模式。最后，给出对应需求模式的观察者模型，与系统模型并行组合，优化模型验证的时空资源消耗。