【作者】 邓小妮；

【导师】 罗雪山；

【作者基本信息】 国防科学技术大学 ， 管理科学与工程， 2008， 博士

【摘要】 信息技术的发展以及战争形态的变化,对一体化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系统的需求开发质量提供了一定的研究基础,具有理论和实践意义。更多还原

【Abstract】 With developments of information technology and changes in the form of war, the need for integrated C~4ISR system is urgent, and it is suggested that C~4ISR system development be guided and surpported by top-level design techniques including requirements engineering (RE) and architecture technology. As the first phase of the process, RE is the foundation for the following phase of the process. To identify the requirements correctly is the key to the successful development of C~4ISR systems. Good requirements can reduce mistakes and avoid the emergent cost for correcting them. Requirments Verification&Validation (RV), as an important phase and basic activity in the RE, its purpose as well as result is just to get high-quality requirements.Aiming at the issue of RV, a model-based requirements validation methodology for C~4ISR system (MERVY) is proposed and studied in this thesis. Besides, the body of C~4ISR requirements specification and the body of C~4ISR RV tasks are studied as the two basic issues of MERVY at the beginning. And the application of the proposed model-based RV methodology is studied with the case of field operations aerial defense C~4ISR system as the background at the last. The primary work and contributions of the thesis are as follows:(1) The body of C~4ISR requirements specification and the body of C~4ISR RV tasks are studied.First, the connotation and denotation of the ’System Requirements’ are analyzed and a series of conceptions are given. Considering the charicteristics of C~4ISR system, the contants of the problem domain requirements, solution domain requirements and project requirements are analyzed. Based on these work, a fairly clear and comprehensive body of the C~4ISR requirements specification is given. Second, the level, purpose and essence of RV activity are analyzed. With the consideration of different input of C~4ISR requirements specification, the corresponding RV tasks are analyzed. Then, a fairly clear and comprehensive body of the C~4ISR RV tasks is given.(2) The general framework of MERVY methodology is presented, in which the core model PMEIS is proposed and formally defined.Clearing the above two fundamental issues, the origin and orientation of MERVY are discussed, and then the general framework of MERVY is presented, in which PMEIS is the core model, and PMEIS-model-checking-based feature requiements feasibility validation method and PMEIS-model-simulation-based behavior requirements correctness validation method are the two main paths. The core model PMEIS is proposed based on OPDL. PMEIS is consist of PMEIS1 and PMEIS2. PMEIS2 is the OPDL’s entity object modeling part, while OPDL’s functional object modeling part is refined as PMEIS1. PMEIS1 is formall defined for the following detail discuss. (3) PMEIS1 model checking based feasibility validation method for C~4ISR property requirements is studied.According to the application research, the transition-base model-checking method is chosen to study. PMEIS1 is translated into timed automata(TA), and TA-based model checker UPPAAL is used to check the model. PMEIS1 to TA is the key, so the correspondence between the two models is analyzed and the detailed translation steps are given. Then, by analyzing and adjusting the reference point and verefication point of the two inputs(the model and the property formula) of model checker, the concrete steps of PMEIS1-model-checking-based feasibility validation method for C~4ISR property requirements is given.(4) PMEIS2 model simulaiton based correctness validation method for C~4ISR behavior requirements is studied.The differences between requirements description models and requirements validation models are analyzed. And then it is pointed that behavior requirements description models being translated into executable validation model is proved to be an effective means for behavior requirements’ progmatic level correctness validation. UML Sequence Diagrms(SD) based behavior requirements description model being translated into executable PMEIS2 model is detailed with several translation algorithms including individual SD to PMEIS2 translation algorithm and combined SDs to PMEIS2 translation algorithms. And based on these work, the concrete steps of PMEIS2 model simulaiton based correctness validation method for C~4ISR behavior requirements is given.(5) Application of PMEIS-model-based requirements validation methods is studied.The application of the above proposed PMEIS-model-based RV methods is studied and detailed with the case of some kind of field operations aerial defense C~4ISR system as the background. Firstly the application of PMEIS2 model simulation based correctness validation method for behavior requirements is studied with the aerial defense command information system. Secondly its subsystem - radar jammer system.is used as an example to illustrate the application of PMEIS1 model checking based feasibility validation method for property requirements. Case studies show the PMEIS model based requirements validation methodology (MERVY) proposed in this thesis feasible and effective.The research and achievements of this dissertation will enhance the foundations of further studies of requirements verification&validation technologies and realization of high-quality requirements development for C~4ISR system from both theoretical and practical perspectives.更多还原