基于ASP及稳定失败语义的CSP模型检测

来源 :桂林电子科技大学 | 被引量 : 0次 | 上传用户:xiezuoyaoxiezuoyao
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
CSP(Communicating Sequential Processes)是Hoare提出的一种代数语言,主要用于对并发系统进行描述与验证。主流的CSP模型检测工具包括FDR、PAT等。FDR通过操作语义将进程转化为相应的迁移系统,并依据迁移系统显式导出指称语义模型,转化过程较复杂且不易修改和扩展;性质描述采用CSP进程形式,与时态逻辑公式(LTL、CTL)相比,表达能力不强,特别是对活性的描述不足。PAT虽然采用LTL描述,但只能描述迹语义下系统性质,不能表示事件的可达性(available)。上述模型检测工具普遍不支持在验证工具的一次运行中验证多个性质。  为了解决以上问题,本文将ASP(Answer Set Programming)应用于基于稳定失败语义的CSP模型检测,将进程的稳定失败模型和LTL公式转化为ASP程序,将系统性质验证转化为回答集求解问题。采用LTL描述系统性质,扩大了稳定失败语义下系统性质验证范围。同时针对稳定失败模型只应用于无活锁的并发系统的特点,构造了基于ASP的CSP进程无活锁的静态分析算法,该算法保守地标记进程无活锁,可用于包含隐藏算子的并发系统的无活锁判定。具体地,主要研究内容如下:  (1)基于ASP的并发系统无活锁的静态分析技术研究。基于稳定失败语义的模型检测只能验证无活锁的并发系统性质,为了验证进程的无活锁性,提出了基于ASP的CSP进程静态分析方法。通过对各种组合算子(选择,并发,隐藏和重命名)的分析,构造进程循环集合(进程的迹中可以无限次出现的事件组成的集合)和无活锁标记的ASP规则。循环集合还可用来确定隐藏哪些事件既不会导致进程发散,又减小了系统规模。  (2)基于ASP及稳定失败语义的并发系统CSP模型检测框架研究。确定并发系统无活锁后,为实现基于稳定失败语义的并发系统的性质验证,建立了基于ASP及稳定失败语义的CSP模型验证框架,将CSP模型检测转换为ASP回答集求解问题,实现了以并发方式一次运行验证多条性质。  (3)CSP进程的稳定失败模型到ASP程序的转换。给出CSP进程的ASP谓词表示,针对不同的组合算子(谨慎选择、外部选择、内部选择、并发和隐藏)构造了对应稳定失败模型的生成规则。  (4)稳定失败语义下基于ASP的LTL公式描述与验证。给出了稳定失败语义下LTL公式到ASP规则的转换,其中LTL公式增加了新的操作符available,使之能够描述稳定失败语义下系统性质。实验结果表明了本文提出的模型检测方法能够验证稳定失败语义下并发系统的安全性和活性,且实现一次运行验证多条性质。
其他文献
目标追踪技术是计算机视觉研究领域中比较活跃的课题之一。随着计算机软硬件的发展,目标追踪技术已经在多个领域得到了应用,相关的算法研究日益深入。粒子滤波追踪算法作为一
数据仓库技术在决策支持系统中发挥着关键的作用,它对决策支持系统提供一些商业信息,从而提高策能力。然而,构建数据仓库仍然是一项富有挑战性和复杂性的任务,主要是因为数据
网格技术是当前计算机技术发展的一个重要方向,它把用通信手段连接起来的资源无缝集成为一个有机整体,给用户提供一种基于互联网的新型计算平台。网格信息服务是网格系统中的
图论是离散数学的骨干分支,离散数学则是计算机科学技术与网络信息科学的思想基础。近年来由于计算机尤其是大型计算机的发展,使得图论在数学,物理、化学、地理、生物等基础学科
随着集成电路工艺和计算机自动化控制技术的发展,基于多核架构的实时系统得到广泛应用,特别是在数字控制、指挥控制、信号处理以及军事领域等方面发挥着重要的作用,使得基于多核
近年来,随着XML数据的受到越来越多应用开发者的欢迎,对XML的标签树和标签图数据模型的检索处理成为了一个重要的研究课题。而XML索引是有效检索XML的自然途径。 结构摘要作
查询优化是数据库管理系统设计和实现所采用的一项重要技术,也是影响数据库系统性能的一个重要因素。数据库查询优化包括两方面,基于代价的查询优化和基于响应时间的查询优化
环境监测具有地理位置分散、环境恶劣、需要无人职守等特点。长期以来,无线数传电台方式在远程数据采集、监视与控制方面占据着主导地位。随着我国移动通信网络的完善,基于GS
网格是继万维网之后出现的一种新型网络计算平台,目的是为用户提供一种全面共享各种资源的基础设施。但因其大规模、分布、异构和动态等特性使得网格计算环境非常复杂,提出了
随着计算机图形学的发展,对植物建立模型并动态地模拟植物生长、死亡等生命活动已经成为虚拟现实领域的研究热点。由于植物的生长发育是一个非常复杂的过程,不仅受到物种自身