信息技术的发展以及战争形态的变化,对一体化C~4ISR系统的需求日益迫切;C~4ISR系统的开发和建设,更加重视以需求工程和体系结构技术为核心的C~4ISR系统顶层设计技术的指导和应用。需求工程作为系统开发的第一步,是后续开发阶段的基础和依据;正确确认系统的需求是成功开发C~4ISR系统的关键,优质的需求可以减少和尽量避免系统开发后期错误的出现及其给系统造成的高昂修正代价。需求验证,作为需求工程单独列出的一个重要阶段和基本活动,其目的和结果正是为了得到优质的需求。本文针对C~4ISR系统需求验证问题,提出了基于模型检验与仿真的C~4ISR系统需求正确性验证方法(MERVY)并对其进行了深入研究。同时,围绕这个核心问题,深入分析了C~4ISR系统需求规格体系、C~4ISR系统需求验证任务体系这两个前导性的基础问题,并通过旅防空指挥信息系统的综合案例研究了方法的具体应用。本文的主要工作和成果包括以下几个方面:1.分析了C~4ISR系统需求规格体系、C~4ISR系统需求验证任务体系深入分析针对大规模信息系统的“系统需求”的内涵与外延,给出了一套明确的定义;结合C~4ISR系统的特点,全面分析C~4ISR系统问题域需求、解系统需求以及项目需求应该包含的规格内容,并在描述形式上找出与C~4ISR/DoD体系结构框架产品的可能的对应关系,给出了一套完备的C~4ISR系统需求规格体系。剖析需求验证活动的层次、目的、实质及特点,给出需求验证活动模型;分析不同C~4ISR需求规格进入到需求验证活动模型中的情况,得到了C~4ISR系统需求验证任务所包含的具体子任务项,亦即C~4ISR需求验证任务体系。2.建立了MERVY框图,提出了PMEIS模型并进行了形式定义在明确了以上两个基本问题之后,建立了MERVY方法的总体框图,并形式定义了PMEIS模型:分析基于模型的验证方法在C~4ISR系统需求验证任务体系中的定位和出发点;确定了以PMEIS模型为核心、以基于PMEIS模型检验和基于PMEIS模型仿真两条路径为支柱的、分别针对C~4ISR系统性质需求的可行性以及行为需求的正确性进行验证的MERVY框图。基于本实验室OPDL模型,保留它对实体对象建模的部分(PMEIS2),并对其对功能对象建模部分的语义进行精简和提取,提出PMEIS1模型;PMEIS1和PMEIS2共同构成PMEIS模型。对PMEIS1进行了形式定义,为后续模型检验做好准备。3.研究了基于PMEIS1模型检验的C~4ISR性质需求可行性验证方法基于应用研究考虑,选择基于转换的PMEIS1模型检验方法:将PMEIS1模型转换为时间自动机网模型,利用已有较成熟的基于时间自动机的模型检验器UPPAAL对模型进行性质验证。PMEIS1模型到时间自动机的转换是其中的关键:研究了两种模型之间的对应关系,给出了详细的转换过程和步骤。然后通过分析并调整模型检验器的两个输入(模型与性质需求公式)的基点和验证点,将模型检验用于性质需求的可行性验证,给出了基于PMEIS1模型检验的C~4ISR系统性质需求的验证方法的具体步骤。4.研究了基于PMEIS2模型仿真的C~4ISR行为需求正确性验证方法分析了需求描述模型和需求验证模型的区别,进而指出,将行为需求描述模型转换为可执行的行为需求验证模型,并通过对验证模型的执行和仿真来实现对描述模型的验证与分析,是行为需求语用层次正确性验证的一种有效手段。具体研究了基于序列图描述的C~4ISR系统行为需求的语用层次正确性验证,其中主要研究了序列图到PMEIS2模型的转换:分析了两种模型的对应关系以及转换思路,给出了具体的转换算法,包括简单序列图转换算法和复合序列图转换算法两部分。在此基础上,总结了基于PMEIS2模型仿真的行为需求验证方法的过程与步骤。5.研究了基于PMEIS模型的需求验证方法的应用通过旅防空指挥信息系统的综合案例详细阐述了如何运用基于PMEIS的模型检验和模型仿真来验证系统的性质需求和行为需求:首先用旅防空指挥信息系统的例子,说明了场景及其组合表示的作战层次的行为需求,如何运用基于PMEIS2模型仿真的方法进行正确性验证;然后,以旅防空指挥信息系统的子系统——雷达干扰机系统为例,说明了如何利用基于PMEIS1模型检验的方法来验证系统层次的性质需求。案例研究证实了本文所提基于PMEIS模型检验与仿真的需求验证方法(MERVY)的可用性和有效性。本文的研究工作对于深入研究C~4ISR系统的需求验证技术、提高C~4ISR系统的需求开发质量提供了一定的研究基础,具有理论和实践意义。