[实时系统的组合模型检验]许何

【实时系统的组合模型检验】许何.pdf3001年6月6日 郑国梁(签字) 论文答辩日期:指导教师46>实时系统的组合模型检验 3验证采用Fischer互斥协议的并发系统的互斥特性 1 引论 1实时系统的描述模型 1时段特性 模型规范和规约 2基本模型语言:时间自动机 2形式化定义:2转换系统并发实时系统和并发的时间自动机网 2.实时系统的组合模型检验 摘要 实时系统的模型检验是利用计算机的快速计算能力,自动地验 证用特定的模型描述语言刻画的实时系统是否满足某个给定的性 质。实时系统的组合模型是为了方便用户描述并发实时系统而引 入的。这些组合模型主要是在已有基本的描述模型中加入同步机 制。我们使用时间自动机网来描述一个并发的实时系统,并对它 进行可达性分析和线性时段特性的验证。文中介绍了相关的检验 算法和工具实现。我们的工具一个是验证带共享变量和同步通道 的时间自动机网的线性时段特性,另一个是对带同步标号的时间 自动机网的可达性分析。文中还介绍了一种合成算法。
———— 文字由OCR识别(未校验)，可能存在错字；请以原始完整版为准。