基于抽象解释的Prolog程序验证技术研究

作为一种通用的语义近似理论,抽象解释已广泛应用于各类程序的形式化验证中.现有基于抽象解释的逻辑程序验证技术未涉及与程序点相关联的程序性质的验证,设计能够描述此类性质的逻辑程序具体语义和抽象语义是构造相应验证工具的关键.本文给出了一种基于抽象解释的Prolog程序验证方法,该方法采用了具有路径信息的Prolog语义及其抽象作为语义基础,因而可用于验证与程序点相关联的程序特性.本文例子表明了该验证方法的有效性.     

无线传感器网络软件动态加载技术研究

以Arena操作系统的设计技术为基础,构建了一个适合无线传感器网络软件动态加载的总体设计方案,详细给出了动态对象加载器的接口设计技术。该设计减小了系统运行时的内核镜像,实现了系统在运行状态下动态加载和卸载软件模块的功能,同时保证系统长时间可靠运转并具备高可配置能力,从而有利于系统软件的升级和后期维护。模块动态加载实验验证了该设计方案的可行性。     

柔性制造系统中生产调度问题求解的一种符号算法

讨论了基于有序二叉决策图的有界Petri网符号分析,给出了其中镜像计算的一种新算法,进而建立了柔性制造系统生产调度问题的符号有序二叉决策图求解算法.该算法在求解过程中通过对状态空间及其搜索过程中相关数据的有序二叉决策图表示,避免了状态和搜索的显示枚举,实现了隐式高效操作,进而改善了算法的计算性能.仿真实验表明了算法的有效性.     

从经典逻辑知识构建ASP知识库的新方法

回答集程序设计(ASP)是一种主流的非单调知识表示工具。为了能够在利用ASP求解问题过程中使用现有的以经典逻辑表示的知识,给出了一种把以谓词逻辑公式表示的约束型知识和定义型知识转化为ASP程序或知识库的新方法,并以实例说明了其有效性。该方法满足转化后ASP程序的回答集与原公式集的模型具有一一对应关系。在实际应用中,该方法提供了一项从现存的以谓词逻辑为表示语言的知识库,构建以ASP为知识表示语言的非单调知识库的技术。     

基于进程迹的CSP模型验证框架

CSP(Communicating Sequential Processes)是构建并发系统和网络安全协议的经典方法。当前主流的CSP模型验证方法需将进程转化为迁移系统,转化过程比较复杂;性质采用迹进行规范,不利于活性的描述。提出了一种基于进程迹的CSP模型验证框架,其性质采用通用的规范方法LTL进行描述。利用ASP(Answer Set Programming)技术实现了一个CSP验证系统。实验表明,与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,在性质不满足时还可提供反例。     

基于对象分布式实时系统约束的一致性研究

在分布式实时系统中,时间约束规格的一致性是解决任务分配和调度等关键问题的必要前提。该文给出了一种基于对象分布式实时系统调度的通用模型,并对该模型进行了形式化描述。该模型克服了以往模型不能在应用系统的逻辑和功能部件上描述系统实时约束的不足,允许从方法和活动上描述所需的约束,降低了单一约束描述的繁杂程度。为了解决使用该模型进行约束规格的一致性问题,该文给出了绝对时间约束、相对时间约束、一致性约束以及相对时间约束和一致性约束之间的一致性判定的必要条件。     

基于OBDD的含圈与或图搜索算法研究*

与或图搜索是人工智能领域一项一定范围内通用的问题求解技术。基于传统数据结构的与或图表示技术极大地限制了与或图搜索算法可求解问题的规模。本文在Mahanti等提出的含圈与或图理论框架基础上,给出了基于OBDD的含圈与或图符号表示方法,并提出了一种求解含圈与或图最小代价解图的符号搜索算法。实验结果表明：该算法在处理大规模含圈与或图时具有明显优势。     

基于对象分布式实时系统的容错模型研究

该文在基于对象的分布式实时系统调度模型研究的基础上,对G-Net模型进行了扩展,即给出了一种基于时间约束G-Net的分布式实时系统容错模型。该模型提供了容错和模块化机制,降低了分布式实时系统设计的复杂性,提高了系统的可维护性,有助于大型复杂可靠的分布式实时系统的设计。最后,该文还给出了基于时间约束G-Net模拟器的结构。     

基于EHA模型检验Statecharts

模型检验是一种重要的形式化自动验证技术。Statecharts是一种用以规约复杂反应式系统行为的可视化语言。为了验证Statecharts模型是否满足所期望的性质,该文给出了一种基于EHA模型检验Statecharts的方法,首先把Statecharts转换为EHA,通过其操作语义得到Büchi自动机,然后与LTL公式所得的Büchi自动机相乘,最后检查该乘积自动机所能接受的语言是否为空,来判断是否满足所期望的性质。     

基于抽象解释的C程序信息保密性研究

在分析程序具体语义的基础上,提出一种信息保密性检测方法。构造具体语义和抽象语义的对应关系,根据待测程序性质构建抽象语义,同时在抽象基础上,采用限界思想来优化检测的效率。通过该方法降低程序检测的复杂性,减少时间和空间的浪费,提高了检测的效率和准确度。