论文部分内容阅读
模型验证是对有限状态系统的一种形式化确认方法.近几年,模型验证方法已逐步扩展到实时系统应用中.为解决实时系统的模型验证问题,本文采用离散时段演算作为实时系统规格说明的形式语言,用时间自动机作为实时系统的实现模型,对模型验证问题进行了细致的分析,并提出了一种具有实际应用价值的方法--商技术.该方法可以避免当多个时间自动机并行组合时可能产生的状态空间组合爆炸问题,同时还可以简化整个模型验证问题.