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

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

基于ASP的CSP模型验证性质反例生成技术研究

为了解决当前通信顺序进程(CSP)模型检测不支持在验证工具的一次运行中验证多个性质的问题,建立了基于ASP的CSP并发模型验证框架。主要研究在该框架下当待验证的系统性质不满足时生成相应性质反例的技术。把ASP程序调试中的ASP程序支撑原因分析技术应用于该问题的研究,提出了相应的反例生成算法,实例表明了该算法的正确性。     

基于ASP的CSP并发系统验证研究

传统并发通信顺序进程(CSP>性质的验证通常使用3个不同的模型层面,从而增加了系统的复杂性和验证 工具开发的难度;同时,主流的并发系统模型验证工具不支持在系统的一次运行中验证多个性质,这也降低了性质验 证的效率。首先将CSP程序转换为ASP程序,然后将CSP进程并发规则和以LTL/CTL公式表示的待验证性质转 换为ASP规则,从而建立了基于ASP验证CSP并发系统性质的统一框架。实验结果表明,基于ASP的CSP并发系 统验证技术易于实现,在保持较高验证效率的同时,能够支持在验证软件的一次执行中验证多条LTL/CTL公式。     

一种基于ILP和ASP的学习B语言描述的动作模型方法

动作模型学习可以使Agent主动适应动态环境中的变化,从而提高Agent的自治性,同时也可为动态域建模提供一个初步模型,为后期的模型完善和修改提供了基础.通过结合归纳逻辑程序设计(Inductive Logic Program-ming,ILP)和回答集程序设计(Answer Set Programming,ASP),设计了一个学习B语言描述的动作模型算法,该算法可以在混合规模的动态域中进行学习,并采用经典规划实例验证了该学习算法的有效性.     

采用SPIN的自动柜员机业务逻辑模型检测方法

由于自动柜员机需要提供可靠的服务,确保其业务逻辑的正确性具有非常重要的意义.然而,传统的测试方法不能对其正确性进行验证.以相关业务逻辑为具体实例,给出一种基于Spin( Simple Promela Interpreter,一种典型的模型检测工具)的自动柜员机的模型检测方法.介绍如何对自动柜员机业务逻辑进行建模、如何对其主要属性进行描述和验证.实验结果表明了所提方法的可行性.     

基于CSP和动态博弈的电子支付系统模型

分析电子支付系统的安全问题,提出基于通信顺序进程和动态博弈的电子支付系统模型。该模型对协议主体的各种不诚实行为和3种质量的通信媒介建模,可以用于分析协议主体和通信媒介之间的合作和竞争行为。对进程失效和由于消息丢失或消息延迟导致的通信失效建模,能分析各种失效情况下协议的安全属性。     

一种基于CSP的协议模型技术

讨论了为建立协议模型而进行的CSP扩充问题．主要向CSP中引入了可终止进程的概念，给出了可终止进程的判定方法；提出了用CSP来描述异步通信的手段；介绍了如何实现从FSM模型向CSP模型的转换；最后给出了AB协议的CSP描述．     

基于线性时态逻辑的Petri网模型检测研究

线性时态逻辑Petri网结合了Petri网和时序逻辑的优点,清晰简洁的描述并发系统事件间的时序和因果关系,包括系统的活性和安全性.其中自动机的体积是模型检验的一个关键性问题,为了得到尽可能小体积的自动机,在LTL公式转换为Büchi自动机之前,对LTL公式进行预处理来减少冗余,然后通过布尔技术优化自动机.     

模型检测方法在入侵检测中的应用研究

入侵检测系统的智能性逐渐受到重视,基于逻辑的模型检测方法是一种有效的误用检测方法.介绍基于逻辑的模型检测方法的研究现状,提出一种基于模型检测的入侵检测模型,描述模型的工作原理和优点.     

基于时态逻辑的UML交互模型检测研究

该文详细介绍了统一建模语言和模型检测技术,在此基础上,该文研究了基于交互自动机和时态逻辑的UML交互模型性质检测方法,提出了模型检测所需的Marking算法。该算法通过对交互自动机全部状态的遍历,检测各状态的时态逻辑公式(CTL公式)的真值,以判断用户设计的UML交互模型是否符合计算机软件系统应满足的性质及规范。     

多智体系统时序认知规范的SPIN模型检测

SPIN模型检测器主要用来检测线性时序逻辑描述的规范,而多智体系统的规范采用时序认知逻辑描述比较方便。本文着重讨论了如何利用SPIN模型检测线性时序认知逻辑的方法,根据局部命题的理论,将模型检测知识算子和公共算子表述的规范规约为模型检测线性时序逻辑的问题,从而使SPIN的检测功能由线性时序逻辑扩充到线性时序认知逻辑。本文通过一个RPC协议分析实例来说明模型检测线性时序认知逻辑的方法。     

ProMiner:系统性质驱动的双向一致性检验框架

在模型驱动软件开发过程中,基于模型的测试方法往往用于检验软件代码针对软件模型的一致性以确保软件质量.然而,随着当今软件系统规模的不断扩大,相应的软件开发过程也变得越来越灵活,代码有时会先于模型被修改,以更忠实地体现系统功能和实现机制.传统的基于模型的测试方法只能检测代码之于模型的一致性而不能反作用于模型层面,模型的修改者只能人为地评估修改的正确性,大大降低了效率并增加了系统的潜在隐患.为此,对传统基于模型的测试方法的一致性检验进行了扩展,实现了一致性检验框架ProMiner,通过抽取表达模型与代码的不一致的系统性质来自动定位模型中与实际运行系统不匹配的部分,并将其表示为可直接用于模型检测的线性时序逻辑(LTL)表达式,以支持软件模型和代码间双向的一致性检验.实验结果表明,ProMiner可有效查找软件模型和代码间的不一致并生成可直接检测模型的系统性质,从而实现了自动化的模型与代码间的双向一致性检测,不仅提高了一致性检测的有效性,而且大大减少了人力开销.     

Model Checking Temporal Aspects of Inconsistent Concurrent Systems Based on Paraconsistent Logic

Classical logic cannot be used to effectively reason about concurrent systems with inconsistencies (inconsistencies often occur, especially in the early stage of the development, when large and complex concurrent systems are developed). In this paper, we propose the use of a paraconsistent temporal logic (QCTL) for supporting the verification of temporal properties of such systems even where the consistent model is not available. We introduce a novel notion of paraKripke models, which grasps the paraconsistent character of the entailment relation of QCTL. Furthermore, we explore the methodology of model checking over QCTL, and describe the detailed algorithm of implementing QCTL model checker. In the sequel, a simple example is presented, showing how to exploit the proposed model checking technique to verify the temporal properties of inconsistent concurrent systems.     

有界模型检查可执行文件的安全属性

引入模型检查方法对可执行文件进行脆弱性分析.对可执行文件形式化建模,采用有界模型检查技术验证可执行文件的安全属性,并在X86体系结构上开发了一个用于可执行文件的模型检查器.实验以内存泄漏和栈溢出漏洞为例,将其属性描述为线性时序逻辑公式,在可执行文件的状态迁移系统模型中验证公式是否能满足,实验结果表明对可执行文件的有界模型检查是一种有效的静态分析方法.     

Verifying ReLU Neural Networks from a Model Checking Perspective

Journal of Computer Science and Technology - Neural networks, as an important computing model, have a wide application in artificial intelligence (AI) domain. From the perspective of computer...     

有界模型检测同步多智体系统的时态认知逻辑

提出在同步的多智体系统中验证时态认知逻辑的有界模型检测(bounded model checking,简称BMC)算法.基于同步解释系统语义,在时态逻辑CTL*的语言中引入认知模态词,从而得到一个新的时态认知逻辑ECKL_n.通过引入状态位置函数的方法获得同步系统的智能体知识,避免了为时间域而扩展通常的时态认知模型的状态及迁移关系编码.ECKL_n的时态认知表达能力强于另一个逻辑CTLK.给出该算法的技术细节及正确性证明,并用火车控制系统实例解释算法的执行过程.     

基于线性时序逻辑的实时系统模型检查

模型检查是一种用于并发系统的性质验证的算法技术.LTLC(linear temporal logic with clocks)是一种连续时间时序逻辑,它是线性时序逻辑LTL的一种实时扩充.讨论实时系统关于LTLC公式的模型检查问题,将实时系统关于LTLC公式的模型检查化归为有穷状态转换系统关于LTL公式的模型检查,从而可以利用LTL的模型检查工具来对LTLC进行模型检查.由于LTLC既能表示实时系统的性质,又能表示实时系统的实现,这就使得时序逻辑LTLC的模型检查过程既能用于实时系统的性质验证,又能用于实时系统之间的一致性验证.     

Liveness Checking as Safety Checking for Infinite State Spaces

In previous work we have developed a syntactic reduction of repeated reachability to reachability for finite state systems. This may lead to simpler and more uniform proofs for model checking of liveness properties, help to find shortest counterexamples, and overcome limitations of closed-source model-checking tools. In this paper we show that a similar reduction can be applied to a number of infinite state systems, namely, (ω−)regular model checking, push-down systems, and timed automata.     

基于时态测试器的实时分支时态逻辑模型检测

基于自动机理论的模型检测技术在形式化验证领域处于核心地位, 然而传统自动机在时态算子上不具备可组合性, 导致各种时态逻辑的模型检测算法不能有机整合.本文为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测, 提出一种RTCTL*正时态测试器构造方法, 以及相关符号化模型检测算法.证明了所提出的RTCTL*正时态测试器构造方法是完备的.也证明了该算法时间复杂度与被验证系统呈线性关系, 与公式长度呈指数关系.我们基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK 2.0.0.我们完成了MCTK与著名的符号化模型检测工具nuXmv之间的实验对比分析工作, 结果表明MCTK虽然在内存消耗上要多于nuXmv, 但是MCTK的时间复杂度双指数级小于nuXmv, 使得利用MCTK验证大规模系统的实时时态性质成为可能.