第20卷第22期2008年11月系统仿真学报?JournalofSystemSimulationVol.20No.22Nov.,2008HLA联邦形式化校核方法初探杨惠珍，康凤举(西北工业大学航海学院，西安710072)摘要：概述了形式化校核方法在软件工程的应用情况，分析了国内外关于HLA联邦VV&A方法研究的现状，讨论了形式化方法HLA联邦校核与验证中主要解决的问题，提出了一种基于时态逻辑的HLA联邦形式化校核方法，该方法可以用来校核联邦及其成员的交互设计和逻辑行为运行的正确性和逻辑性.最后总结了全文，指出形式化方法虽然有利于提高HLA联邦的可信性、可靠性和一致性，但需要较多的专门知识和自动化工具的辅助。关键词：HLA；VV&A；联邦；形式化校核；时态逻辑中图分类号：TP15;TP391.9文献标识码：A文章编号：1004-731X(2008)22-6039-03PreliminaryStudyonFormalVerificationMethodforHLAFederationYANGHui-zhen,KANGFeng-ju(CollegeofMarineEngineering,NorthwestPolytechnicUniversity,Xi’an710072,China)Abstract:BeginningwithanalysisofresearchworksaboutHLAfederationVV&Atechniquesandapplicationinsoftwareengineeringofformalmethods,aformalmethodbasedontemporallogicwasproposed.Thismethodcouldbeusedtocheckthecorrectnessandlogicalityofinteractionbetweenfederatesduringthestageofdevelopingthefederationconceptualmodelandexecutingthefederation.Atlast,itisindicatedthatformalverificationmethodisinfavorofimprovingthecreditability,reliabilityandconsistencyofHLAfederation,butitsapplicationisrestrictedbecauseofspecialknowledgeandautomaticcomputerassistedtools.Keywords:HLA;VV&A;federation;formalverification;temporallogical引言[1,2,3,4]1一般说来，形式化方法就是用具有形式语义的记号和工CSP、CCS、时态逻辑和自动机等。形式化校核是指基于形式规范使用严格的数学方法来推理验证计算机系统是否符合所期望的特性（如安全性、一致性等）的过程。它又分为模型检验(ModelChecking)和定理证明(TheoremProving)两类。其中，基于时态逻辑和基于自动机的模型检验方法是目前比较实用的形式化方法。形式化方法已在一些软、硬件系统开发中得到了成功应用，例如，AMD公司的AthlonTM芯片浮点运算部件的验证、Eurocopter公司民用直升机自动导航系统以及Vocalis信令控制中间平台等。在软件系统开发过程中使用形式化方法有利于增强系统的可信性和可靠性，更好地控制系统的复杂性。由于应用形式化方法需要较深的数学理论基础，通常需要相应的辅助工具来实现，代表性的工具有：时态逻辑模型检验器SMV和Spin、组合检验器PVS、基于高阶逻辑的定理证明器HOL等。具明确地表述所要设计的计算机系统的设计要求，即给出系统的规范(specification)，并根据系统规范利用上述记号和工具对系统具有的性质和最终实现的正确性进行严格的证明。随着计算机技术的发展，形式化方法的研究也取得了较大的发展，在软件工程方面有了一些成功的应用，出现了一些商业性软件工具。形式化方法虽然在许多文献中被列为VV&A方法之一，但很少见到相关报道，关于HLA联邦的形式化方法研究也不多。本文对联邦概念模型的形式化校核方法进行了初步探索，通过国内外有关联邦VV&A方法和形式化校核方法的研究现状分析，给出了HLA联邦形式化校核方法侧重解决的问题，提出了一种基于时态逻辑的形式化校核方法。[1]1形式化方法及其应用2联邦形式化校核方法研究关于HLA联邦校核与验证问题，美国颁布了IEEE1278形式