责任政策形式化验证方法

为了验证多Agent系统设计的正确性,将责任政策作为约束多Agent交互行为的高层"需求规格"或"通信协议",对其进行形式化建模及验证。研究了建模责任政策的形式化框架语言,基于责任状态模型建模责任政策的动态演化过程。给出了政策模型形式化验证方法,将政策模型的操作语义定义为Kripke结构的状态迁移系统,政策中Agent行为的约束规则声明为线性时序逻辑公式,使用模型检测器Nu SMV验证政策模型对线性时序逻辑公式的可满足性。实验结果表明,该方法可有效分析责任政策的设计缺陷,提高多Agent系统设计的正确性。     

基于模型检测的策略冲突检测方法

提出一种基于模型校验的策略冲突检测新方法。首先通过形式化描述语言进行系统建模,采用时态逻辑表征策略冲突的系统属性,然后利用NuSMV模型检测器验证属性的可满足性,并根据模型检测器产生的反例轨迹追溯策略冲突点。该方法可提高策略冲突检测的效率。     

基于Agent会话的数字车间运作模型的研究

使用会话作为分析Agent之间通信的基本单位。在基于Agent的数字车间中有多种类型的Agent分别实现着不同的功能，它们之间在进行交互时，因为任务和功能的不同而应采取不同的会话方式。在分析各种不同类型Agent之间7种主要类型的交互关系后，给出了基于Agent会话的车间运作过程，并用AUML描述了车间生产调度会话模式。最后采用Java语言在Agent开发平台JADE上实现了数字车间的调度系统，验证了基于Agent会话的数字车间运作模型的高效性和可靠性。     

CAUPS系统中的评估模型及多Agent协作策略

针对当前计算机辅助城市规划系统中普遍存在数据交换能力弱、协同性不强、效率低等问题，设计并实现了一个全新的计算机辅助城市规划系统，即CAUPS.详细介绍了CAUPS中实体关系的定义和构成，采用KQML的消息格式来完成多实体Agent间的通信，同时KQML也被用作实体Agent与知识库中规则间的交互传递方式.在此基础上利用实体关系可以定制出符合用户需求的评估模型.在性能上使用轻量级控制策略和重量级控制策略，实现了多实体Agent间的同步、协调和控制.基于实体关系自定义的评估模型实现方法以及多Agent协作策略等技术已成功应用于杭州钱塘江沿岸规划项目中.     

基于多代理系统的微网协同控制研究

针对传统集中控制和分散控制的缺陷,提出了一种基于多代理系统的微网控制策略协调和调度方法,设计和部署了总控制Agent用于调度和多个子Agent用于独立管理微网中的不同实体。总控制Agent对微网中不同的子Agent的控制策略进行协调和调度,子Agent根据具体调度策略进行本地执行,以保证微网物理设备满足电约束,这些Agent共同作用保证了微网在变化的环境中始终保持稳定运行。借助开源的JAVA代理开发框架,并遵循FIPA标准定义对Agent之间交互提供支持。利用Matlab/Simulink搭建了微网系统模型,模拟了微网在并网运行、孤岛运行以及并网/孤岛切换情形下各Agent协调和调度过程,仿真结果表明该设计可行、有效。     

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

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

基于行为语言的智能交互代理

提出了基于行为语言的智能交互代理,利用关键词匹配技术获取用户需求关键信息,触发cplus2asp系统根据行为语言描述的知识及规则进行推理得出调控策略,实现智能人机交互。该智能交互代理的实现方法解决了传统智能交互引擎交互接口不友好、交互过程复杂等问题的局限性。实验结果验证了该方法的有效性。     

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

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

基于移动Agent的分布式安全审计系统的研究

介绍了安全审计系统的重要性.设计并实现了基于移动Agent的分布式安全审计系统.该系统构造了多种类型的安全Agent,利用多Agent的相互交互、协作来实现分布式安全审计过程,满足网络动态变化的要求.指明了实现系统的关键技术和方法.     

基于模型检测的服务规则路由正确性验证方法

基于模型检测技术,提出了一种适用于集成了规则引擎的企业服务总线中的消息规则路由的正确性验证方法。首先将基于规则的消息路由转换为服务模型六元组,然后再将服务模型六元组转换为NuSMV输入程序,最后通过NuSMV工具实现自动化验证。给出了一个贷款审批业务的服务规则。路由的正确性验证实例证明了该方法的可行性。     

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

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

模型检测与定理证明相结合开发并验证高可信嵌入式软件

首先将软件的UML状态机模型转换为模型检测工具MOCHA的输入语言REACTIVEMODULES,在MOCHA中进行正确性验证,利用模型检测工具针对错误情况给出的反例路径,尽早修改软件的UML设计模型;然后将已验证过的UML模型转换为定理证明工具B方法的抽象规约,利用B方法的精化、验证及代码生成功能,直接生成正确的C代码。并给出了从UML状态机到REACTIVE MODULES建模语言及B AMN抽象规约的转换规则。实验结果表明,该方法可在软件工程中有效地提高高可信嵌入式软件开发和验证的效率。     

一种新型的机械同步运动误差微机检测技术

本文介绍了机械同步运动误差检测原理，提出时空相连微机软件细分方法，并在此基础上建立起一种新型的机械同步运动误差微机智能检测系统．最后，将该系统在ＣＤ３２０Ｇ型单啮仪上进行运动误差实测、对比与分析验证，获得令人满意的结果．     

MPSoC核协调可靠性和性能的形式化验证

为了在早期发现片上多核处理器（MPSoC）设计缺陷,本文提出了一种对核协调进行结构建模和性质刻画的形式化方法。在标记变迁系统中引入多项式函数替代动作表达核协调过程中对数据的改变,加入物理元器件发生故障的概率属性,形成用以描述核协调可靠性和性能的混杂马尔科夫决策过程模型。采用随机时序逻辑刻画系统性质,通过模型检测工具验证分析,以银行数据脱敏MPSoC为例,分析系统可靠性和时间延迟与能耗等性能指标。这些验证结果对于早期MPSoC设计人员具有较强的指导作用。     

模型验证中的公平性问题

研究模型验证中的公平性问题,全面定义了包括进程层面（process-level）的强/弱公平、事件层面（event-level）的强/弱公平以及全局强公平性（strong global fairness）等,把这些公平性条件集成进了一个模型验证工具PAT.该工具支持以on-the-fly的方式对线性时序逻辑性质进行验证.通过对多个基准模型进行实验,该工具在基于公平条件的模型验证中表现出良好的性能.     

利用双参数地基模型修正反应位移法弹簧

为得到一种模型简单、计算精度高,且能更好反映土-结构相互作用的地下结构抗震设计方法,根据双参数地基模型的原理,用比传统单参数模型更加接近土体性质的双参数模型简化土体,并根据受力和变形特性对双参数计算模型进行简化,最终得到能考虑土体间相互作用的修正反应位移法.修正方法计算模型与传统反应位移法相比,仅仅是法向弹簧的基床系数进行了一定的修正,仍然是一种模型简单的计算方法.建立数值模型进行分析,以动力时程计算结果为基准,并与传统反应位移法作对比验证修正方法的正确性.结果表明,相比传统采用离散弹簧模拟土体的反应位移法,修正方法的内力及变形误差能减小一半左右,由此得到修正方法是一种模型简单且计算精度较高的设计方法,能够应用到地下结构抗震设计中.     

Chinese-Wall模型在开放综合安全模型中的实现

Chinese Wall模型体现了随系统运行而不断改变的动态安全策略,但使用范围有限. 为了保持安全模型在适应不同领域的同时能够体现动态安全策略,基于一种开放的综合安全模型(OSSM),提出Chinese Wall模型的实现方法.该方法通过构造动态累加角色,记录必要的访问历史,然后结合历史访问及安全策略对当前访问请求作出决策,以体现策略的动态性.实现结果表明,该方法在保持模型综合性的同时,提高了其灵活性.     

Constructing formal verification models for hardware Trojans

The effectiveness of hardware security verification is affected by the way of constructing formal verification models.To solve this problem,this paper proposes a method which can automatically construct formal verification models for hardware Trojans detection.First,the method traverses the control flow graphs of the register transfer level design to extract the path conditions of assignment statements and the corresponding expressions.The constraint relations of the Kripke’ state transition are generated based on the path conditions and the expressions.Second,the constraint relations of the Verilog grammar are transformed to the grammar of the model checker and generate the formal verification models.Finally,a model checker verifies the models and detects the hardware Trojans when a predefined specification is verified as false.In experiments,the hardware Trojans in the Trust-HUB benchmarks are detected,which shows that the models constructed by our method can effectively detect hardware Trojans in register transfer level design.