HLA联邦形式化校核方法初探

Preliminary Study on Formal Verification Method for HLA Federation

概述了形式化校核方法在软件工程的应用情况,分析了国内外关于HLA联邦VV&A方法研究的现状,讨论了形式化方法HLA联邦校核与验证中主要解决的问题,提出了一种基于时态逻辑的HLA联邦形式化校核方法,该方法可以用来校核联邦及其成员的交互设计和逻辑行为运行的正确性和逻辑性.最后总结了全文,指出形式化方法虽然有利于提高HLA联邦的可信性、可靠性和一致性,但需要较多的专门知识和自动化工具的辅助。

Beginning with analysis of research works about HLA federation VV＆A techniques and application in software engineering of formal methods, a formal method based on temporal logic was proposed. This method could be used to check the correctness and logicality of interaction between federates during the stage of developing the federation conceptual model and executing the federation. At last, it is indicated that formal verification method is in favor of improving the creditability, reliability and consistency of HLA federation, but its application is restricted because of special knowledge and automatic computer assisted tools.