多Agent交互策略模型检测方法

提出一种基于模型检测的多Agent交互策略验证方法,首先通过责任政策语言建模多Agent的交互策略,基于责任政策语言的操作语义将政策模型转换为模型检测器NuSMV的输入,利用时态逻辑声明表征策略冲突的系统性质,然后利用模型检测器NuSMV自动验证政策模型对性质的可满足性,并根据模型检测器产生的反例分析交互策略中的各种错误。该方法可提高交互策略的验证效率,确保多Agent系统设计的正确性。     

Verilog程序的命题投影时序逻辑符号模型检测

为了保证以Verilog硬件描述语言设计的片上系统的正确性,提出了Verilog程序的符号模型检测方法．依据形式化操作语义将Verilog程序建模为有限状态机,将设计规范用命题投影时序逻辑公式描述,并采用命题投影时序逻辑符号模型检测工具对程序进行验证,从而证明片上系统满足设计规范．以Verilog程序描述的四位同步二进制计数系统的验证实例表明,Verilog程序的命题投影时序逻辑符号模型检测方法是可行的．     

进位保留加法器的命题投影时序逻辑组合验证

为保证硬件设计的正确性,提出了对硬件设计组合验证的新方法．该方法在命题投影时序逻辑的统一框架下,实现对硬件系统行为的建模,对所期望性质的形式化描述,并利用命题投影时序逻辑合理且完备的公理系统对系统性质进行验证,从而证明硬件系统满足期望的性质,保证设计的正确性．进位保留加法器的验证实例说明了该方法的可行性．     

基于场景的并发系统需求验证方法研究

为验证并发系统需求设计的正确性,提出一种基于场景的并发系统需求验证方法.首先,用UML顺序图建模并发系统需求场景,通过定义顺序图的操作语义及转换规则,将顺序图的XML描述文件自动转换为Promela程序,而后将描述系统需求的Promela程序和描述系统规约的线性时序逻辑作为模型检测器SPIN的输入,用模型检测的方法自动...     

基于惰性切片的线性时态逻辑性质验证

惰性切片是一种有效的状态空间缩减方法,但是它无法直接判定一个模型是否满足所期望的线性时间性质。针对该问题,提出了一种基于惰性切片的线性时态逻辑公式验证方法。该方法首先构造给定线性时态逻辑公式的否定Büchi自动机与系统模型的乘积自动机,然后使用惰性切片算法在该乘积自动机上以惰性方式搜索可接受迹,从而把线性时间性质验证问题转换为通过可达性分析搜索可接受状态的不变性检测过程。实验结果证明,基于惰性切片的线性时态逻辑公式验证算法在不损失验证结果正确性的前提下使惰性切片算法具备了验证线性时间性质的能力,同时也有效提高了LTL模型检测方法的可扩展性。     

规范多agent系统动态模型及其属性验证机制

针对规范多Agent系统（NMAS）并发性、动态性和规范性的特点,提出了一种规范多Agent系统动态模型和基于模型检验的属性验证机制.其中动态模型包括行为约束规范语言TNAL和联合行为转移结构两大部分.TNAL以现实世界法律法规为参考,实现了规范的时态特性和道义特性的建模.联合行为转移结构以多Agent联合行为作为状态转移标记,以规范剪枝后的计算树描述规范系统的动态语义,使系统属性描述语言和规范语言相互独立.以CTL*作为系统属性描述语言,借助现有模型检验工具即可实现NMAS的属性验证,这种实现方式使系统验证工作具有更高的灵活性.     

基于时间区间时序逻辑的实时系统统一模型检测

在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质. 为此, 该文使用一个离散时间区间时序逻辑公式建立实时系统模型, 使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质, 在此基础上, 离散时间区间时序逻辑统一模型检测问题即可归约为目前已解决的离散时间区间时序逻辑可满足性判定问题. 该文证明了新方法的有效性以及正确性, 为区间实时逻辑这一类的模型检测问题提供了方法.     

一种UML状态图模型检测方法

为在开发过程早期发现系统设计的各种错误与不一致,提出一种UML状态图模型检测方法,用于验证设计模型与需求规约间的一致性.该方法通过元组定义UML状态图的主要元素,给出状态图的中间表示形式SC.基于SC上定义的操作语义,该方法将状态图转换为具有KRIPKE语义结构的状态迁移系统,并将系统需满足的性质表示为线性时序逻辑公式...     

基于时态逻辑的形式化联邦校核方法

提出了一种基于时态逻辑的形式化联邦校核方法，采用时态逻辑公式描述联邦各成员的行为逻辑关系，推导出与该时态逻辑公式对应的有限自动机模型，即规范自动机。同时，建立联邦全局行为的状态转移图，即实现自动机，通过检验规范自动机所接受的语言是否包含实现自动机所接受的语言来判断联邦运行时各成员的状态变化是否满足规范要求，达到校核联邦的目的。该方法可用来校核联邦及其成员的交互设计和逻辑行为运行的正确性和逻辑性，具有理论意义和应用价值。     

基于Petri网的多Agent系统设计与实现

以面向对象Petri网OPN为语义基础,从软件体系结构的角度,建立了一种直观的多Agent系统模型MASM,可以形象地描述Agent的内部结构和动态行为。为了缩小形式化模型与系统实现之间的差距,基于MASM设计了一个多Agent系统开发工具箱MASDT,提供了多Agent系统的基本实现框架。利用MASM对智能加油站系统进行建模和分析,并用MASDT开发了智能加油站系统原型,证实了所提出的一系列理论和方法对于实际系统开发具有一定的指导意义。     

基于智能体的OWL-S过程模型验证

为保证基于OWL-S的web服务组合的正确性和可靠性,对OWL-S过程模型进行时态和认知属性的验证.将原子过程视为单个服务作为Agent,将组合过程抽象为多智能体系统,把对OWL-S过程模型的验证转换成对多智能体系统的验证.提出了OWL-S语言的形式化模型OWL-S2FSM,设计从OWL-S2FSM到模型检测工具MCTK输入语言之间的转换算法,并应用MCTK对多智能体系统的规范进行验证.实验结果表明,该方法可以有效地验证多智能体系统的时态属性和认知属性.     

基于 KQML的多智能体系统建模与验证

为了保证 MAS相关属性的可满足性、有效性以及验证的高效性,提出了一种基于 KQML 通信语言的MAS建模以及能够实现自动验证相关规范的方法.设计并实现了 KQML 语言转化为完整描述状态转换关系的一组状态迁移七元组的算法,以及从七元组到多智能体模型检测工具 MCMAS输入语言ISPL的转化算法,从而实现多智能体系统的自动形式化建模,并用 MCMAS对多智能体系统规范的正确性进行验证.实验结果表明,所提出的算法不仅能够验证多智能体系统的时态规范,还能验证其特有的认知规范.     

基于STPA空管运行系统安全分析方法研究

在空管运行系统中,分析相关事故或不安全事件过程中常把责任归咎于某一方面的不足,然而,对重大事故的彻底调查几乎总能发现其他的因素,单一的事故假设已经不再满足复杂的运行系统。安全性是一个系统属性,而不仅仅是独立于系统之外的特性。将安全整合到系统工程中,视管制员的行为为其发生环境的产物,将安全视为系统控制问题。利用系统理论过程分析(STPA)空管运行系统,识别系统潜在的不安全行为,进而利用一阶线性时态逻辑(LTL)将识别出的不安全行为规范化描述,建立不安全行为约束的形式化表达式。通过NuSMV模型检测工具对安全约束的规范化描述进行模型验证,验证系统的安全性,评估系统的安全状态。为进一步的安全监控提供理论支持,同时为管制员及空管单位领导者提供决策支持,进而减少不安全事件发生。     

多Agent协同系统的Pi演算建模方法

MAS因自治性、反应性等特性适用于复杂的分布式系统,为了分析、模拟Agent的并发交互过程并设计出合理的MAS,应用了形式化方法Pi演算进行建模． 首先介绍了多Agent协同系统中Agent之间的广播、中介和代理3种通信模型, 然后给出了Agent之间交互模式的Pi演算建模方法． 再以家庭物联网系统作为多Agent协作实例, 应用Pi演算对其建模, 模拟多个Agent协作过程中的通信． 最后, 采用移动工作台对模型的语义进行了验证, 表明了Pi演算对MAS建模的适用性．     

投影时序逻辑的公理系统与形式验证

为了采用定理证明的方法对并发及交互式系统进行验证,提出了一阶投影时序逻辑的公理系统．利用投影时序逻辑既可描述待验证系统性质和规范,又可描述其实现模型的特点,在同一投影时序逻辑框架可以方便地对待验证系统进行建模和性质描述,并使用公理系统完成系统性质的证明．最后通过一个实例来展示投影时序逻辑及公理系统在系统验证中的应用．     

NPCD-Agent：扩展的Agent思维状态模型

在基于Agent的计算中,现有研究对于动机的定义和动机影响Agent行为决策的分析比较片面,缺少对动机的清晰考虑和相应目标产生的描述.为此建立了具有动机的Agent思维状态模型,将动机分为社交行为准则（N）、策略（P）、契约准则（C)和内部愿望(D).形式化地描述了动机扩展的Agent思维状态模型(NPCD-Agent)和BNPCDGI逻辑,阐述了逻辑的语法、语义以及相应的公理系统.给出了动机算子基于Kripke可能世界的新的语义解释,验证了动机算子不存在逻辑全知问题.通过计算0-1规划和设定优先顺序,建立了动机冲突消解模型,改进了现有包含动机的Agent思维状态模型实现方法.实例分析表明,改进的Agent思维状态模型使得Agent行为决策过程更加理性.     

信息物理融合系统的面向对象Petri网建模

从多Agent系统的角度,以面向对象Petri网为语义基础,建立了一种信息物理融合系统体系结构模型,将系统抽象为传感器节点Agent、执行器节点Agent和控制器节点Agent．该体系结构模型利用面向对象Petri网形象、无歧义地刻画系统的整体和个体特性,描述系统的静态和动态语义,同时可利用Petri网的数学分析方法和支持工具对系统进行模拟、分析和验证,检测系统开发早期存在的错误,提高系统的正确性和可靠性．利用信息物理融合系统体系结构模型对目标跟踪系统的建模、分析与实现表明,信息物理融合系统体系结构模型可以有效地辅助系统的设计与开发．     

MSVL语言的公理系统的程序验证

MSVL语言是一种用于模拟、建模和验证程序的区间时序逻辑程序设计语言．为了证明区间时序逻辑程序的正确性,提出了MSVL语言的一个公理系统:包括正则形转换的状态公理和状态推演规则,以及将程序从一个状态转换到另一个状态的区间公理和区间推演规则．最后给出验证实例说明基于该公理系统的程序验证方法．     

硬件安全门级细粒度形式化验证方法

针对硬件设计长期缺乏有效的安全验证方法问题,提出了一种硬件安全门级细粒度形式化验证方法．该方法使用形式化语言在逻辑门层面上描述硬件电路的安全属性,构造包含安全属性跟踪逻辑的形式化语义语句,从而将硬件设计转化为电路语义模型,并结合霍尔逻辑三元组理论构造用于验证该模型安全属性的定理．定理的证明过程是以人机交互的方式在定理证明器环境下验证定理的合理性．实验结果表明,该方法能够形式化地遍历电路语义模型的状态空间,精确验证不同输入状态下电路语义模型的安全性．该方法通过构造安全属性跟踪逻辑提高了验证的精确性,结合定理证明提高了验证覆盖率,能够有效地验证硬件设计的安全性．     

使用扩展区间时序逻辑为并发工作流建模

针对集中式体系结构并发工作流的两种运行方式(活动并发执行和活动以任意顺序执行),对区间时序逻辑进行扩展,提出两个新操作符“交错”和“限制性交错”．根据工作流状态的偏序关系以及逻辑公式连接前后其模型的长度关系,证明用新操作符连接的区间时序逻辑公式适于表示并发工作流．结合一个并发工作流实例,说明如何用扩展区间时序逻辑表示活动及由活动组建的并发工作流,从而得到并发工作流的区间时序逻辑模型．利用并发工作流的区间时序逻辑模型验证并发工作流的活性和安全性,可大大提高并发工作流设计的可靠性．