终止证明方法在形式化建模中的应用

随着形式化方法的普及和应用,定理证明器HOL4在形式化建模过程中无法自动完成终止证明的情况越来越多,而手动终止证明又缺少通用的证明思路.针对这种情况,提出规范化的手动终止证明方法.该方法从问题产生的本质入手,首先保证目标具备解决终止问题的必要条件,然后通过等效替换简化证明目标,最后以原有定理库为基础,寻找证明过程中缺失...     

智能机器人系统的形式化建模

基于作者先前巳为智能机器人系统提出并建造成的一种新型结构模型──环递阶模型［１，２］，应用形式语言理论，首次将智能机器人系统整体形式化地建模成了一种上下文无关文法．     

服务系统理论架构与建模

This paper proposed a theoretical framework of service system based on the theory of system science, and studied some related notions, such as the composition of a system, the relationship between systems, the system hierarchy structure, the evolution of a system, etc. In the next section, we discussed the modeling of service system and the future research work.     

不确定环境下hCPS系统的形式化建模与动态验证

随着科技的进步,新型复杂系统例如人机物融合系统（Human Cyber-Physical Systems,HCPS）已经与人类社会生活越来越密不可分.软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合.物理空间内环境的复杂多变、时空数据的爆发增长以及难以预料的人类行为等不确定因素威胁着系统安全.由于系统安全需求的增长,系统的规模和复杂度随之增加所带来的一系列问题亟待解决.因此,在不确定性环境下,构造智能、安全的人机物融合系统已经成为软件行业不可回避的挑战.环境不确定性使得人机物融合系统软件无法准确感知其所处的运行环境.感知的不确定性将导致系统的误判,从而影响系统的安全性.环境不确定性使得系统设计人员无法为人机物融合系统软件的运行环境提供准确的形式化规约.而对于安全要求较高的系统,准确的形式化规约是保证系统安全的首要条件.为了应对规约的不确定性,本文提出时空数据驱动与模型驱动相结合的建模方式,即通过使用机器学习算法,基于环境中时空数据对环境进行建模.根据安全软件的典型特征,采用动态验证的方式保证系统的安全,从而构建统一安全的理论框架.为了展示方案的可行性,本文以自动驾驶车辆与人驾驶的摩托车的交互场景为例说明了在不确定性环境下的人机物融合系统的建模与验证的具体应用.     

CPN在FCM形式化建模与验证中的应用

联邦概念模型(FCM)是整个联邦系统开发的依据.针对当前FCM建模能力差、可重用性低,以及很难实现FCM的动态行为验证的缺陷,分析了国内外形式化建模与验证方法研究的现状,提出了一种基于着色Pe‘网(CPN)的联邦概念模型形式化建模与验证方法,给出了用CPN建立与验证FCM的步骤,并以-制造系统为例,利用CPN Tools建立了系统的FCM,验证了所建模型的活性、家态和公平性.研究表明,CPN能够为FCM的形式化建模和验证提供有效的支持.     

混成系统形式化验证

混成系统是实时嵌入式系统的一种重要子类,其行为中广泛存在离散控制逻辑跳转与连续实时行为交织混杂的情况,因此行为复杂,难以掌握与控制.由于此类系统广泛出现在工控、国防、交通等与国计民生密切相关的安全攸关的领域,因此,如何对相关系统进行有效的分析与理解,从而保障系统安全运营,是一项具有重要意义的工作.常规的系统安全性分析手段,如测试、仿真等仅能在一定输入的情况下运行系统来观测系统行为,无法穷尽地检测复杂混成系统在所有可能输入下的行为,因此并不足以保证系统的安全性.区别于测试等方法,形式化方法通过求解系统模型状态取值范围等方法来确认系统模型中一定不会出现相关错误.因此,其对于保障安全攸关混成系统的安全性具有十分重要的意义.形式化方法由形式化规约与形式化验证两个方面构成.因此从以上两个角度分别对形式化规约方向上现有混成系统建模语言、关注性质以及形式化验证方向的混成系统模型检验、定理证明的现有主要技术与方法进行了综述性的回顾与总结.在此基础上,针对现阶段实时嵌入式系统复杂化、网络化的特性,对混成系统形式化验证的重要关注问题与研究方向进行了探索与讨论.     

工作流中资源的形式化建模

虽然人们为了使工作流管理完全计算机化付出了巨大的努力,但结果表明,这一目标即使在技术高度发达的今天,乃至可预见的未来也是不可能实现的,组成工作流的很多任务还只能由人来完成。首先对工作流中资源(主动资源)的分类方式进行讨论并把它们统一成一个资源元模型,然后给出了一个基于用户资格和特征的资源建模形式化描述。     

重写对策在基于HOL的形式化证明中的应用

讨论了重写对策在基于高阶逻辑定理证明系统HOL的形式化证明过程中的应用.通过REWRITE_ TAC对策、ASM_ REWRITE_ TAC对策和RW_ TAC对策,详细分析了重写对策的功能、应用方法、应用环境、应用中可能出现的问题以及解决办法,给出了DB.match搜索和DB.find搜索等重写对策的定理参数的选择方法,并进行了分析与比较.进一步说明了重写对策在基于HOL系统的形式化证明中的重要性,以期对HOL系统用户提供一些帮助与启发,促进HOL系统的进一步发展与完善,使形式化方法能够解决更多的实际问题.     

面向航天嵌入式软件的形式化建模方法

航天嵌入式软件是航天型号任务成败的关键之一.航天嵌入式软件是一种周期性、多模式的软件.软件的每个模式表示系统处于一定的状态,并进行相应的复杂计算.因此,提出了一种名为SPARDL的形式化建模方法.为了满足型号应用的需求,对这一方法进行了若干改进.为了表达航天器的时序性质,提出了一种基于区间逻辑的性质规范语言.为了支持工业应用,还设计了代码生成方法.这一建模方法已在航天工业领域得到了应用.     

一个机载软件需求形式化建模与分析实例研究

现代民机机载软件系统的功能与复杂度在快速增长的同时还必须满足更严格的安全标准, 使得在机载软件需求层级必须进行诸如一致性、完整性等分析与验证成为重要的挑战. 工作基于一个自主设计实现的面向机载软件自然语言需求形式化建模与分析工具平台(ART)展开对座舱显控软件子系统(EICAS)需求的建模与分析, 包括: ART工具平...     

基于模糊命题模态逻辑的形式推理系统

探讨基于可信度的模糊命题模态逻辑的形式推理,给出相关的模糊Kripke语义描述.其研究目的旨在解决基于模态命题逻辑的模糊推理的能行问题.在研究过程与方法上,以完全形式化的方法将模糊模态逻辑语法和语义统一在一个形式系统中,以模糊约束作为基本表达式,给出推理规则,建立了相应的模糊推理形式系统,并以形式系统中模糊约束集的可满足性来表示模糊推理的有效性,使模糊推理过程变得容易,为最终在计算机上实现基于模态逻辑的模糊推理打下了一定的基础.主要结论是证明了基于可满足性的模糊推理形式系统的可靠性与完备性.     

Process and Policy: Resource-Bounded NonDemonstrative Reasoning

This paper investigates the appropriateness of formal dialectics as a basis for nonmonotonic reasoning and defeasible reasoning that takes computational limits seriously. Rules that can come into conflict should be regarded as policies, which are inputs to deliberative processes. Dialectical protocols are appropriate for such deliberations when resources are bounded and search is serial.
AI, it is claimed here, is now perfectly positioned to correct many misconceptions about reasoning that have resulted from mathematical logic's enormous success in this century: among them, (1) that all reasons are demonstrative, (2) that rational belief is constrained, not constructed, and (3) that process and disputation are not essential to reasoning. AI mainly provides new impetus to formalize the alternative (but older) conception of reasoning, and AI provides mechanisms with which to create compelling formalism that describes the control of processes.
The technical contributions here are: the partial justification of dialectic based on controlling search; the observation that nonmonotonic reasoning can be subsumed under certain kinds of dialectics; the portrayal of inference in knowledge bases as policy reasoning; the review of logics of dialogue and proposed extensions; and the preformal and initial formal discussion of aspects and variations of dialectical systems with nondemonstrative reasons.     

典型系统基于架构的层级化建模技术研究

随着工业化与信息化的深度融合,计算机建模与仿真技术已广泛应用于系统或产品的研发过程中,但其存在模型混乱、碎片化、层次不清晰、复用性差的问题。基于对系统架构的理解,提出了一种基于系统架构开展系统层级化建模的方法。在建立模型时将整个系统分解为系统层、子系统层和部件层的多层次模型;各层级模型的接口均与系统架构定义的接口关系保持一致,实现设计的连续性,为基于模型的设计提供有效的支撑。该方法能清晰表述模型的目的、层级和颗粒度。文中以典型伺服作动系统为例进行了验证,结果证明了方法的有效性。     

基于混合推理机制的故障诊断专家系统

多数故障诊断专家系统采用单一的推理机制,或者基于规则的推理,或者基于事例的推理。而这两种推理机制都各有优缺点,采用单一推理机制会造成诊断的不准确性。论文将基于规则的推理和基于事例的推理相结合,设计了混合推理机制。在此基础上,论文设计了一个既有专家知识库,又有故障事例库,具有自学习能力的故障诊断专家系统(AFDES)。实验结果表明,论文设计的混合推理机制是比较有效的。     

基于双向推理的主体框架

文章提出了一个基于双向推理的主体框架FBRA,它是一个混合型的主体框架,主体既是反应的又是慎思的。它的推理内核是正向推理和反向推理相结合。正向推理用于对环境的反应,包括对其他主体的反应。反向推理基于溯因推理,用于信念修正、规划、多主体协调和多主体通信等。     

运用建模技术对制造业售后管理信息系统架构的设计与实现

管理信息系统发展至今30多年,已经深入到各行各业中。近年,日趋成熟的建模技术使得许多软件公司纷纷投入其中,并利用它辅助设计和开发软件。通过建模技术辅助设计与实现制造业售后管理信息系统架构,并设计出对应的各种数据模型,能突破系统原始开发扩展性和延伸性的局限。同时,成熟的数据模型又能对相关应用开发设计起到良好的引导作用,具有一定的参考价值与现实意义。并以此说明建模技术在系统开发中能起到降低开发难度,增强团队沟通能力,提高软件开发效率,提高软件开发移植性等优点。     

基于UML的软件体系结构建模方法研究

模型的有效集成是软件系统建模的关键。然而,通常基于UML的软件系统的四个模型中,从用例分析模型到其它设计模型之间存在一条很难逾越的鸿沟。本文通过引入软件体系结构模型,提出了基于UML的软件体系结构建模方法,进一步完善了软件系统的建模。     

用于离散控制系统知识聚集的案例推理技术研究

论文根据认知原理,结合案例推理、黑板结构等技术,提出了一种用于离散控制系统的基于案例推理的控制模板,实现在系统运行中自动进行知识聚集。     

应用系统中身份认证建模及推理方法

逻辑推理是对身份认证进行形式化研究的重要手段,但现有研究成果主要集中在认证机制、认证协议等单个方面,并不考虑应用环境,通过引入身份认证域,对应用系统中身份认证进行形式化描述;在此基础上,提出一种基于谓词的身份认证建模及推理方法,包括7种谓词、8个推理规则和一种4步骤推理方法等,并对基于静态口令、动态口令和数字证书的身份认证模型进行实例分析.