Research On The Validation Methods Of The C~4ISR System Requirements Based On Model Checking And Simulation

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.