带有情感算子的Agent形式化系统研究

随着人工智能的发展,有关Agent理论和技术的研究应用引起了人们的高度关注和重视.纵观以往的Agent研究,主要集中在Agent的构造上.随着生物学和心理学的发展,把情感加入Agent中,越来越受到计算机研究者的关注.提出了带有情感算子的Agent形式化模型Em-BDI-VSK,它融合BDI逻辑和VSK逻辑并加入情感,并构建了该模型的语义框架和公理体系.

基于形式化方法的区块链系统漏洞检测模型

随着区块链技术在各行各业的广泛应用,区块链系统的架构变得越来越复杂,这也增加了安全问题的数量.目前,在区块链系统中采用了模糊测试、符号执行等传统的漏洞检测方法,但这些技术无法有效检测出未知的漏洞.为了提高区块链系统的安全性,提出基于形式化方法的区块链系统漏洞检测模型VDMBS(vulnerability detection model for blockchain systems),所提模型综合系统迁移状态、安全规约和节点间信任关系等多种安全因素,同时提供基于业务流程执行语言BPEL(business process execution language)的漏洞模型构建方法.最后,用NuSMV在基于区块链的电子投票选举系统上验证所提出的漏洞检测模型的有效性,实验结果表明,与现有的5种形式化测试工具相比,所提出的VDMBS模型能够检测出更多的区块链系统业务逻辑漏洞和智能合约漏洞.

基于Isabelle/HOL的文件系统形式化设计与验证

对于构建可信操作系统而言,文件系统设计和实现的正确性至关重要,即使是已经得到广泛运用的文件系统仍然有漏洞被检测出来。采用形式化方法对文件系统的设计和实现的正确性进行严格的验证是公认的可行方法。当前文件系统的形式化验证工作大多基于宏内核操作系统,而忽视了微内核操作系统架构下文件系统的验证。为此,提出一种微内核架构下采用内联数据机制的文件系统的形式化设计和验证方法。以高阶逻辑(HOL)和自动机模型为基础,将文件系统中的工作对象和系统资源抽象为系统对象来构建文件系统的工作状态,形式化地描述文件系统的相关系统调用的功能语义,将系统调用提供服务的过程抽象为系统工作状态发生跃迁的过程,并给出文件系统功能正确性和安全属性的断言。以实现的安全可信微内核操作系统(VSOS)中的安全可信文件系统(VSFS)为例,在设计阶段构建VSFS的有限状态机模型,并在Isabelle/HOL中抽象描述VSFS的可移植操作系统接口(POSIX)系统调用,分析和归纳出VSFS文件系统正确性断言,使用定理证明的方式来验证VSFS的正确性。实验结果表明,该方法在Isabella/HOL中完成VSFS有限状态机模型细粒度的形式化验证,满足预期的安全需求规范。

一种面向嵌入式操作系统的形式化验证方法

操作系统是整个计算机系统的核心与基石,其可靠性与安全性至关重要.操作系统的故障或漏洞可能会导致系统崩溃、数据丢失、隐私泄露和安全攻击等问题,特别是在安全攸关系统中,一旦操作系统发生错误,就可能会造成重大人员伤亡或财产损失.一直以来,如何保障操作系统的安全性和可靠性对学术界和工业界都是一个重大挑战.目前验证操作系统安全性的方法有软件测试、程序静态分析、形式化方法等.其中,形式化方法是最有潜力确保操作系统安全可信的方法,通过使用形式化方法,建立数学模型并进行系统的形式化分析和验证,从而发现潜在的错误和漏洞.在操作系统中,形式化方法可以用于验证操作系统的功能正确性、完整性以及系统安全性等.在已有的针对操作系统形式化验证的成果基础上,提出了一个面向嵌入式操作系统的形式化验证方案,采用VCC(verified C compiler)、CBMC(C bounded model checker)以及PAT(process analysis toolkit)工具分别对操作系统单元层面、模块层面和系统层面进行验证.该方法已成功应用到某操作系统的任务调度架构案例中,对于嵌入式操作系统的分析验证具有一定的通用性。

基于MK的实数公理系统相容性和范畴性的Coq形式化

数学定理机器证明是人工智能基础理论的深刻体现.实数理论是数学分析的基础,实数公理系统是建立实数理论的重要方法.Morse-Kelley公理化集合论(MK)作为现代数学的基础,也为实数构建提供了严谨的数学框架和工具.本文使用定理证明器Coq,基于MK对实数公理系统进行了深入探索.在优化了MK形式化代码的基础上,形式化构建了完整的实数公理系统,并通过形式化Landau《分析基础》中的实数模型,证明其相对于MK相容,此外,还形式化证明了实数公理系统所有模型在同构意义下是唯一的,验证了实数公理系统的范畴性.本文全部定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.该系统可方便地应用于拓扑学和代数学理论的形式化构建.谨以此文庆祝我国著名控制系统专家秦化淑研究员九十华诞!

汽车电子控制系统安全设计的形式化验证

汽车电子控制系统已成为现代汽车的核心组成部分,因此,深入研究汽车电子控制系统安全设计和验证方法有助于提高车辆安全性能,增强车辆竞争力。本文阐述了汽车电子控制系统安全性的重要性,探讨了当前汽车电子控制系统安全设计和验证方法的局限性,以及汽车电子控制系统安全设计的形式化验证方法,形式化验证方法能够有效地在产品设计早期识别和消除潜在的问题和安全隐患,为汽车电子控制系统的安全设计和验证提供了新的思路。

基于Agent人工智能的异构网络多重覆盖节点入侵检测系统设计

异构网络具有结构复杂、多重覆盖面积大等特征,使得网络入侵检测较为隐蔽,威胁网络运行的安全性;为此,对基于Agent人工智能的异构网络多重覆盖节点入侵检测系统进行了研究;通过检测Agent和通信Agent装设主机Agent,以Cisco Stealthwatch流量传感器作为异构网络传感器检测攻击行为,采用STM32L151RDT664位微控制器传输批量数据,由MAX3232芯片实现系统电平转化,实现硬件系统设计;软件部分设计入侵检测标准,采用传感器设备捕获网络实时数据,通过Agent技术解析异构网络协议并提取数据运行特征,综合考虑协议解析结果及与检测标准匹配度,实现异构网络多重覆盖节点入侵检测;经实验测试表明,基于Agent人工智能的异构网络多重覆盖节点入侵检测系统入侵行为的漏检率和入侵类型误检率的平均值仅为6%和5%,能够有效提高检测精度,减小检测误差。

Agent系统软件体系结构形式化建模方法

基于Agent技术为复杂分布式问题提供了求解方法。软件体系结构是控制软件复杂性、提高软件系统质量、支持软件开发和复用的重要手段之一。软件体系结构设计可用于描述Agent与Agent之间的交互和组织结构的规划,因此Agent系统能从良好的体系结构设计中受益。该文整合了图表句法理论和层次谓词变迁网理论,提出一种形式化建模方法,从抽象层(架构)和实现层(动态行为)两方面来构建Agent系统的软件体系结构。模型具有可验证和追踪性,为Agent系统软件体系结构分析与评估提供了良好的基础。

多Agent系统形式化建模方法研究

简要总结了多Agent系统(MAS)形式化建模方法的研究现状;以面向对象Petri网(OPN)和π演算为基础,给出了一种直观的MAS体系结构模型(Multi-Agent Systems Architecture Model,MASAM)。OPN可以形象地描述MAS的初始化结构及动态行为,而π演算可以刻画MAS的动态演化;另外,可以利用Petri网和π演算的相关分析方法和支持工具分析和验证系统模型,在系统开发早期发现并避免体系结构级的错误。

电子商务中多Agent系统形式化建模与分析

多Agent系统(Multi-agent Systems,MAS)已在电子商务中得到了广泛应用。由于MAS是一个动态系统,现有的形式化方法不适合描述MAS的动态体系结构,而π演算适合描述具有动态结构的系统,以π演算为形式化基础对MAS进行建模与分析。通过构造一个电子商务系统的形式化模型,描述了π演算的建模和分析过程。π演算不但能描述Agent之间的交互,而且可以对系统的一些关键属性进行分析,如分析系统的死锁性等。

形式化方法与应用专题前言

随着硬件运算速度变得越来越快、体系结构变得越来越复杂,软件的功能也变得越来越强大而复杂,如何开发可靠的软件系统,已经成为了一项巨大的挑战.形式化方法是利用数学理论与方法论证检验软件系统可靠性与安全性的方法,包括模型检验、定理证明等多种技术手段.近年来,利用形式化方法解决软件可靠性与安全性问题已经获得了越来越广泛的应用.

基于形式化方法的平交道口控制系统安全设计

铁路平交道口控制系统是一种典型的安全苛求系统,为提高铁路平交道口的安全性,提出一个能适应双线双向接车的自动控制系统.首先,分析现有铁路平交道口的作业流程,利用新的控制系统解决现有系统中常见的三个问题,即出清检查、制动距离限制、连续接车中防护门短时间开放问题;其次,基于Event-B语言以及精化策略对设计的自动控制系统建立形式化模型;最后,检查证明义务以验证需求属性是否被满足,并应用动画器Animation展示系统功能的正确性.结果显示:相比传统的道口管理系统,本文提出的自动控制系统增加了双线连续接车功能,且使用形式化建模和验证,避免系统设计中存在的二义性,对平交道口安全管理有一定的参考意义.

基于多Agent系统网管模型的形式化建模

运用多Agent系统实现分布、自治的网络管理是构造下一代网络管理系统的一条全新思路。然而,大多数基于多Agent系统的网管模型均采用非形式化的方法进行描述,容易造成人们对模型理解的歧义性和在系统开发过程中的随意性。一种利用有色Petri网对分布式网络管理模型进行形式化建模的方法被提出。利用该方法所建立的形式化模型,能够对分布式网管模型中多Agent系统的组成结构和运行机制进行全面刻画,能够描述模型中用到的Agent的各种特性。

基于Agent的跨境电子商务课程智能教学系统

当前,跨境电子商务课程智能教学系统功能模块多为单向形式,可控教学覆盖范围较小,导致平均成绩优化比下降,为此提出对基于Agent的跨境电子商务课程智能教学系统的设计与分析。首先,构建通信接口,并接入驱动装置,完成系统硬件的设计;其次,采用多目标的方式,扩大可控教学覆盖范围;最后,设计多目标Agent跨境电子商务课程教学功能模块,关联跨境电子商务教学知识库,完成系统软件设计。测试结果表明:针对选定的6个班级进行测试对比,最终得出的平均成绩优化比均可以达到20%以上,说明在Agent的辅助下,文章设计的系统应用效果更佳,具有实际的应用价值。

基于访问、感知和知道的多Agent系统形式化模型

提出了基于VSK-AF逻辑的多Agent系统形式化模型。VSK-AF逻辑是模态认知模型的扩展，它表示并且区分外部环境与Agents环境中客观真实的和可访问的信息、环境中可访问的和Agents感知到的信息以及Agents感知到的和知道的信息。在给出了该逻辑的语义模型和公理体系后，研究了模态算子之间的关系并将其对应到VSK-AF系统所具备的特性上。最后总结并讨论了进一步的研究工作。

MAS中Agent属性冲突形式化描述及消解系统研究

由于多智能体系统（MAS）中各个Agent具有自治性、分布性和异构性等特征,导致MAS内部经常会出现冲突现象。首先,运用数学方法对MAS中存在的属性冲突进行形式化描述,并将其分为6类,针对每类冲突提出了相应的消解对策。其次,对属性冲突智能消解系统（AACIRS）流程框架进行了分析,并在此基础上建立了AACIRS系统,实现了MAS中属性冲突的消解。从而为解决MAS中Agent属性冲突提供了解决方案,为MAS的稳定运行提供了技术保证。

面向航电系统任务安全性的形式化建模与验证

针对航电系统任务安全性分析缺少仿真与验证手段问题,提出了一种面向航电系统任务安全性的形式化建模与验证方法。首先,基于时间自动机理论与民航规章建立标准运行条件下航电系统任务过程的形式化模型。随后,将危险致因和安全约束分别以状态变迁的方式注入该模型,建立航电系统任务安全性验证模型。最后,通过遍历状态空间验证模型的活性、危险致因的可达性以及安全约束的充分性,实现任务安全性分析结果的自动化验证。实验结果表明,所提方法具有可行性和有效性,能够为持续进行的航电系统任务安全性分析和设计提供模型基础,确保分析结果的正确性和完整性。

多Agent系统中组织适应的形式化方法

多Agent系统(MAS)中的组织在调节Agent社会方面已被证明是成功的。然而,Agent的行为或动态环境的改变可能导致系统意图的不良执行,所以整个组织需要通过改变来适应新的环境。多Agent系统中从组织的社会结构、社会协定、目标到组织如何适应,提出了一种形式化描述方法,此方法为以后研究多Agent系统的组织适应奠定了理论基础。

多Agent系统的形式化开放混合体系结构模型研究

为了有效建立并统一多Agent系统(MAS)的理论与方法体系,提供MAS的有效设计与实现途径,重点讨论并建立了基于开放环境的MAS形式化开放混合体系结构模型.首先,采用面向Agent的程序设计(AOP)风范,并基于开放环境与组合技术,对Agent的BDI模型进行形式细化处理,引入开放混合结构模式的自治、交互Agent形式定义,在此基础上给出开放环境下的自治、交互MAS的形式化开放混合体系结构模型,并运用扩充了的形式开发语言Z++对其进行描述.该模型具有可扩展性与对开放环境适应性强、便于进行系统描述。

一种针对安全可达动态系统的形式化学习方法

在动态系统建模问题中,深度学习为建模提供了更便捷和灵活的方法,但其难以解释的特点降低了模型的可靠性。针对具有安全性和可达性的动态系统,提出了一种形式化模型学习方法,将安全性和可达性引入到对目标系统的学习过程中,使模型满足这两个性质。为保证所学系统在定义域上严格满足这两个性质,该方法基于现代控制理论中的Lyapunov方法和Barrier函数设计了可验证的Lyapunov Barrier函数(LBF),通过将其与动态系统联合学习,使得LBF能够为所学系统提供安全性和可达性保障。最后通过求解混合整数线性规划问题验证了模型确实满足相关性质,与DDPG的对比实验展示了这一方法的有效性。