指控与仿真系统互操作性语言的形式化语法

在部队模拟训练系统中,实装指控系统与基于仿真的训练支撑环境的互操作性问题是一个亟待解决的问题。为此,提出指控与仿真系统互操作性语言,建立用于指挥控制的形式化语法。语法示例表明,该语法有助于实装指控系统与基于仿真的训练支撑环境间命令、报告和请求等交互信息的准确表达,形成严谨、可解析和文档化的互操作信息。

UML顺序图的一种形式化描述方法

统一建模语言UML是一种通用的图形化建模语言,在面向对象系统的分析和设计中,它已成为了事实上的工业标准。但UML不是形式化的建模语言,缺乏精确的、形式化的语义,因此阻碍了它的进一步发展。线性时序逻辑是并发或反应式程序动态语义的一种形式化描述语言,它适合用来精确地表示模型的动态语义。本文定义了顺序图的形式化语法,采用线性时序逻辑给出了顺序图的语义描述,并通过实例分析,对模型的某条性质进行了证明,为模型做进一步分析和验证提供了基础。

刍议面向航天器星载软件的形式化验证方法

随着星载软件在航天器上实现的功能比重越来越高,星载软件可靠性和可信性的指标要求越来越严格。传统软件测试方法的局限性难以确保万无一失,形式化方法以其高度数学化和严谨性的特点,常被应用于安全关键软件的验证。本文针对星载软件的高可靠性和充分性验证需求,初步提出了相应的形式化验证方案和需求建模实施过程,对于后续整星级的软件验证或者其他单机组件的验证具有一定的参考和借鉴意义。

基于时序逻辑的UML2．0通信图语义研究

UML2.0通信图可以表示对象之间的交互,很适合用于对系统的交互行为建模,但由于UML缺乏精确语义,使得难以对其所表示的系统行为进行分析和验证。XYZ/E是可执行线性时序逻辑语言,既可描述系统的静态语义和动态语义。在定义UML2.0通信图的形式化语法的基础上,给出了通信图的XYZ/E时序逻辑语义,为进一步的系统分析和验证提供了形式化基础。

XBRL技术体系结构的语言学分析与改进研究

为了深化XBRL技术结构的研究,本文依据现代语言学的基本原理,从语法形式化和语义形式化两个维度对XBRL的现行技术体系结构进行了分析,指出了其在语法形式化方面存在元素和规则定义不足,在语义形式化方面存在对句子的语义表达功能重视不够、语音意义未被利用和语境意义不足、修辞分化缺失等问题,并基于未来的发展需求提出了扩展技术规范、重构分类标准以及规范实例文档等改进策略,旨在拓展XBRL技术结构的研究视角,提高XBRL的技术品质,推动XBRL标准的应用。