【实时系统的组合模型检验】许何.pdf

3001年6月6日郑国梁(签字) 论文答辩日期:指导教师

46>实时系统的组合模型检验 3验证采用Fischer互斥协议的并发系统的互斥特性 1 引论 1实时系统的描述模型 1时段特性模型规范和规约 2基本模型语言:时间自动机 2形式化定义:2转换系统并发实时系统和并发的时间自动机网 2.

实时系统的组合模型检验摘要实时系统的模型检验是利用计算机的快速计算能力,自动地验证用特定的模型描述语言刻画的实时系统是否满足某个给定的性质。实时系统的组合模型是为了方便用户描述并发实时系统而引入的。这些组合模型主要是在已有基本的描述模型中加入同步机制。我们使用时间自动机网来描述一个并发的实时系统,并对它进行可达性分析和线性时段特性的验证。文中介绍了相关的检验算法和工具实现。我们的工具一个是验证带共享变量和同步通道的时间自动机网的线性时段特性,另一个是对带同步标号的时间自动机网的可达性分析。文中还介绍了一种合成算法。