基于带数据约束实时系统的互模拟检测方法

带数据约束的实时系统是指一种既带有时间约束又带有数据变量约束的计算系统,其广泛存在于航空航天、工业控制、国防等安全攸关系统,并发挥着至关重要的作用。针对这类系统的形式化建模与验证是确保其正确性和可靠性的重要途径。文中首先研究了组合接口自动机、Z语言、时间自动机的形式规范—CT-ZIA,其能同时描述带数据约束的实时系统的时序行为性质和数据结构性质;其次,为了研究该规范上的互模拟形式化验证,给出了CT-ZIA上的互模拟关系定义;然后,为了互模拟算法的可判定性,对CT-ZIA中的时钟进行等价划分,提出了有限论域CT-ZIA的定义;最后,基于有限论域CT-ZIA模型,给出了其上互模拟检测算法,并说明其正确性。

基于MARTE的面向混成系统的模型形式化转换

混成系统是离散逻辑跳转与实时连续行为交织的复杂状态变迁系统,形式化建模与验证是确保混成系统正确性和可靠性的重要途径。首先介绍一种混成ZIA形式规范;然后,基于建模语言MARTE建立扩展Object-Z的规范,即OZMARTE,该规范弥补了MARTE规范在形式化描述方面的不足,同时为了方便描述混成系统中连续动态行为属性,给出对混成系统中连续变量的描述转换规则,增强了MARTE对混成系统的描述能力;最后,给出OZ-MARTE规范到混成ZIA规范的转换方法,因此针对混成ZIA规范的验证技术同样适用于对MARTE模型进行形式化验证。