向时间自动机转换的军事电子信息系统性质验证

日益复杂的军事电子信息系统面临正确性验证挑战,形式化验证方法如模型检验技术成为必需.给出基于时间Petri网表示的军事电子系统模型PMES的定义,然后给出PMES模型转换为时间自动机网的步骤,利用已有的基于时间自动机的模型检验工具对系统性质进行验证;系统的性质要求用时序逻辑语言CTL或TCTL公式表示.雷达干扰机系统说明了该方法的实际应用效果.     

基于多Agent系统的无人机智能指挥控制系统

无人机是一个具有自治性和反应性的智能系统,结合Agent的特性,将多Agent系统引入无人机智能指挥控制系统的研究与开发中.由于该系统具有复杂的动态结构和行为特征,提出了一种面向Agent的Petri网,用于系统的建模和分析,最后建立了无人机Agent、指挥中心Agent及系统的形式化模型.面向Agent的Petri网不但能描述系统的静态和动态语义,还可利用Petri网的支持工具对系统进行模拟和分析,在无人机智能指挥控制系统研究中具有较好的应用前景.     

天基预警系统资源调度问题分析

在介绍天基预警系统作战流程,以及天基预警系统资源和任务的分析和描述的基础上,提出天基预警系统资源调度问题,给出其输入输出结构,并以五元组的形式对该问题进行形式化描述。 关键词：天基预警系统、资源调度、形式化描述     

反导作战预案形式化建模研究

反导作战预案是提高作战决策方案生成实时性和准确性的关键.通过对反导作战预案具体应用流程的分析,结合SysML,OWL_DL和CBML等形式化建模语言,提出了一种具有模型验证环节的预案形式化建模方法;根据所提出的方法,分析提炼了反导作战预案构成要素,定义了SysML块定义图、预案要素、OWL_DL和XML Scheme元素之间的映射规则;依据相应的转换规则,分别建立了反导作战预案概念层模型、逻辑层模型、物理层模型和预案本体模型,并应用预案本体模型对概念层模型进行了模型一致性验证.     

时态逻辑形式化描述并发系统性质

时态逻辑是一种描述反应式(并发)系统中状态迁移序列的形式化方法,用于刻画并发系统所需验证的性质,是模型检测的基础.阐述了时态逻辑CTL 及其子逻辑CTL、LTL的语法及语义,然后分析运用时态逻辑描述并发系统性质,最后给出一个应用实例.     

战场信息分发服务语义描述方法的分析与比较

文章针对基于语义的战场信息分发这一特定应用,对OWL-S和SAWSDL两种常用的语义服务描述语言进行了深入的比较与分析。首先,以航迹信息为例构建了战场态势信息本体,并对战场传感器所提供的服务进行封装;然后,详细描述了如何采用OWL-S和SAWSDL描述本体及服务,并结合战场态势语义的特殊需求,对两种语言的描述能力、匹配组合的支持能力等性能进行了比较。分析表明OWL-S更适合于复杂多变的战场信息环境。     

想定驱动的仿真资源发现方法

为解决在云间共享架构的仿真环境下资源的自动发现问题,研究了仿真资源请求的描述方法及相应的资源发现算法,提出了想定驱动的仿真资源发现方法.方法通过扩展的军事想定描述语言表示仿真资源请求,使用双映射三过滤算法实现仿真资源的自动发现.分析表明,仿真想定驱动的资源发现方法可以实现在云间共享架构下仿真运行所需的大量资源的自动发现,并对发现结果具有语用校验功能,对于仿真环境的快速部署具有积极意义.     

基于Z形式化规范的多Agent协作模型研究

用形式化规范语言Z定义了多A gen t协作模型的基本元素,包括:A gen t、目标、角色、交互协议和过程,给出了应满足的一致性约束,并通过城市区域的连锁超市物流调度系统说明了该形式化规范为多A gen t协作提供了一致性和连贯性。     

C~3I系统中软件的程序设计方法问题

软件的可靠性是Ｃ￣３Ｉ系统成败的关键之一,用规范和程序分离的办法设计软件,其可靠性无法得到保证。该文阐述了应研究形式化程序设计方法的意见,以及目前在这一领域尚存在的困难和解决的途径。     

应用不可满足子式的解码电路综合优化方法

解释布尔公式不可满足的原因在很多领域都具有实际的应用需求,而最小不可满足子式能够为诸如电路的自动综合等应用领域中的不可满足原因提供最精确的解释。因此,将两种能够高效求解最小不可满足子式的算法——分支-限界算法与贪心遗传算法,集成到解码电路的自动综合工具中。采用通信领域的标准编码电路作为测试集,将两种算法进行对比。实验结果表明,在运行时间与每秒剔除的短句数方面,贪心遗传算法优于分支-限界算法;不可满足子式在解码电路的自动综合过程中发挥重要作用。