基于模型检验与仿真的C~4ISR系统需求验证方法研究
|
摘要
信息技术的发展以及战争形态的变化,对一体化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系统的需求开发质量提供了一定的研究基础,具有理论和实践意义。
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.
本文针对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系统的需求开发质量提供了一定的研究基础,具有理论和实践意义。
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.
引文
[1]卢梅,软件需求工程方法与工具评述[J],计算机研究与发展,vol.36(11),1999.
[2]于云程,罗雪山,C3I系统分析与设计[M],长沙:国防科技大学出版社,1996.
[3]竺南直,指挥自动化系统工程[M],电子工业出版社,2001.
[4]RADC,System/Software Requirements Engineering Testbed Research &development Program,AD-A 197858,1988.
[5]U.S.,Joint Chiefs of Staff,Joint Vision 2010[EB/OL],http://www.dtic.mil/jv2010,1996.
[6]U.S.,Joint Chiefs of Staff,Joint Vision 2020[EB/OL],http://www.dtic.mil/jv2020,2000.
[7]C4ISR Architecture Working Group,C4ISR Architecture Framework Version 1.0[R],U.S.:Department of Defense,1996.
[8]C4ISR Architecture Working Group,C4ISR Architecture Framework Version 2.0[R],U.S.:Department of Defense,1997.
[9]DoD Architecture Framework Working Group,DoD Architecture Framework Version 1.0 Volume Ⅰ:Definitions and Guidelines[R],U.S.:Department of Defense,2003.
[10]国防科技大学C3I中心,指挥信息系统需求工程[R],长沙:国防科技大学,2006.2.
[11]Richardson,K.A.,Mathieson,G.and Cilliers,P.,The Theory and Practice of Complexity Science - Epistemological Considerations for Military Operational Analysis,SysteMexico,1:25-66,2000.
[12]军事科学院战役战术研究部,高技术条件下作战对区域综合电子信息系统的需求分析论证报告[R],北京:军事科学院,1997.
[13]空军第三研究所,空军本级基本指挥所指挥自动化系统需求分析报告[R],北京:空军第三研究所,2001.
[14]空军第八研究所,空军武器装备体系对抗论证仿真系统指挥自动化仿真分系统软件需求规格说明[R],北京:空军第八研究所,2002.
[15]空军第三研究所,“长空-3J”系统需求分析过程说明报告[R],中国国防科学技术报告,空军第三研究所需求工程技术应用研究课题组,2003.
[16]中国国防科学技术报告,需求分析方法总结报告[R],空军第三研究所需求工程技术应用研究课题组,2003.
[17]IEEE,IEEE Std 610.12-1997,IEEE Standard Glossary of Software Engineering Terminology[EB/OL],http://www.ieee.com/,2003.
[18]OMG,Requirements Analysis for UML for Systems Engineering(Draft V0.4)[EB/OL],http://www.omg.com/rw/euml,2003.
[19]Alan M.Davis,Software Requirements:Objects,Functions,and States,Englewood Cliffs,NJ:PTR Prentice Hall,1993.
[20]Karl E.Wiegers著,陆丽娜等译,软件需求[M],北京:机械工业出版社,2000.
[21]Jones Capers,Assessment and Control of Software Risks,Englewood Cliffs,NJ:PTR Prentice Hall,1994.
[22]Suzanne Robertson,James Robertson著,王海鹏译,掌握需求过程[M],北京:人民邮电出版社,2003.
[23]Ralph R.Young著,韩柯等译,有效需求实践[M],北京:机械工业出版社,2002.
[24]Telelogic,Rational Unified Process:Best Practices for Software Development Teams,A Rational Software Corporation White Paper[EB/OL],http://www.uml.org.cn/SoftWareProcess/ pdf/RUP_BestPractics_Chinese.pdf,2003.
[25]李明树,王青,需求工程研究现状[J],中国计算机用户,395(47),1999.
[26]Siddiqi J,Shekaran MC.Requirements engineering:The emerging wisdom[J],IEEE Software,23(3):15-19,1996.
[27]Jarke M,Pohl K.,Requirements engineering:Managing a changing reality,Software Engineering,20(11):257-266,2001.
[28]Thayer,Richard H.,Merlin Dorfman,eds,Software Requirements Engineering[M],Los Alamitos,CA:IEEE Computer Society Press,1997.
[29]IEEE,Terms,Acronyms and Abbreviations[EB/OL],http://www.ieee.com/,2004.
[30]Suzanne Robertson,and James Robertson,Mastering the Requirements Process[M],Harlow,England:Addison-Wesley,1999.
[31]IEEE Std 830-1998,IEEE Recommended Practice for Software Requirements SpeciPcations[EB/OL],http://www.ieee.com/,2003.
[32]IEEE Std-1233-1998,IEEE Guide for Developing System Requirements SpeciPcations[EB/OL],http://www.ieee.com/,2003.
[33]M.Elizabeth C.Hull,Ken Jackson,A.Jeremy J.Dick著,韩柯译,需求工程[M],北京:机械电子出版社,2002.
[34]Karl E.Wiegers著,刘伟琴,刘洪涛译,软件需求(第2版)[M],北京:清华大学出版社,2004.
[35]Hooks,I.,Writing Good Requirements[C],Proceedings of the Third International Symposium ofNCOSE,Vol 2,1993.
[36]唐纳德.高斯,杰拉尔德.温伯格著,章柏幸等译,探索需求:设计前的质量[M],北京:清华大学出版社,2004.
[37]Ian K.Bray著,舒忠梅等译,需求工程导引[M],北京:人民邮电出版社,2003.
[38]Daniel R.Windel,L.Rene Abreo,Software Requiements Using the Unified Process:aPractical Approach[M],软件需求:基于统一过程的实践方法(影印版) [M],北京:中国电力出版社,2003.
[39]Soren Lauesen著,刘晓晖译,软件需求[M],北京:电子工业出版社,2002.
[40]OMG,Unified Modelling Language[EB/OL],http://www.omg.org/,2002.
[41]BjoernerD,On the use of formal methods in software development[C],9th International Conference on Software Engineering,1989.
[42]Norries MZ,A formal specification method[C],In:Thayer RH,Dorfman Meds.Tutorial:System and Software Requirements Engineering.LosAlamitos,CA:IEEE Computer Society Press,345-369,1990.
[43]http://www.incose.org/rwg/
[44]Richard Harwell,Erik Aslaksen,Ivy Hooks,What is a requirement?[C],Proceedings of the 3rd Annual International Symposium,NCOSE,1996.
[45]Pradip Kar,Michelle Bailey,Characteristics of Good Requirements[C],INCOSE Symposium,1996.
[46]INCOSE,Requiements body of Knowledge[EB/OL],http://www.incose.com/BOK/,2002.
[47]OMG,Requirements Analysis for UML for Systems Engineering(Draft V0.4)[EB/OL],http://www.omg.com/se/sysuml.htm,2003.
[48]邵全琴等,迭代演进式GIS需求分析模型研究[J],遥感学报,Vol.5(5):358-366,2001.
[49]Mary Frances Theofanos,Shair Lawrence Pfleeger,Wave front:A Goal-driven Requirements Process Model[J],Information on Software Technology,38:507-519,1996.
[50]N.A.M.Maiden,S.V.Jones,S.Manning,J.Greenwoodl,L.Renou,Model-Driven Requirements Engineering:Synchronising Models in an Air Traffic Management Case[C],CASE'2004,2004.
[51]Ivar Jacobson,Grady Booch,James Rumbaugh著,周伯生等译,统一软件开发过程,北京:机械工业出版社,2002.
[52]James & Suzanne Robertson,Volere Requirements Specification Template(Edition 9),http://www.volere.co.uk,2003.
[53]Chairman of the Joint Chiefs of Staff Instruction,CJCSI 3170.01B[I],April 2001.
[54]Chairman of the Joint Chiefs of Staff Instruction,CJCSI 3170.01C[I],August 2002.
[55]Chairman of the Joint Chiefs of Staff Instruction,CJCSI 3170.01D[I],October 2004.
[56]Chairman of the Joint Chiefs of Staff Instruction,CJCSI 3170.01E[I],March 2005.
[57]Svoboda C P,Structured analysis[J],In:Thayer R H,Dorfmaneds.Tutorial:System and Software Requirements Engineering.Los Alamitos,CA:IEEE Computer Society Press,218-237,1990.
[58]Ross DT,Structured analysis(SA):A language for communication ideas[J],IEEE Transition on Software Engineering,1(1):16-34,1977.
[59]Zave P,An insider's evaluation of PAISLey[J],IEEE Transition on Software Engineering,17(3):212-225,1991.
[60]Urban JE,The Descartes specification language[C].In:ThayerRH,Dorfmaneds.Tutorial:System and Software Requirements Engineering,LosAlamitos,CA:IEEE Computer Society Press,331-344,1990.
[61]Chen P.,Entity-relationship approach to data modeling[C],In:Thayer RH,Dorfman Meds.Tutorial:System and Software Requirements Engineering,Los Alamitos,CA:IEEE Computer Society Press,238-243:1990.
[62]Cameron JR,A over view of JSD,IEEE Transaction on Software Engineering 12(2):43-46,1986.
[63]Yourdon E.,Coad P.,Object-Oriented Analysis(2nd Edition)[M],NewJersey:Yourdon Press,1991.
[64]Booch Getal,Software Engineering with Ada(3rd Edition)[M],Edwood City,Calif:Benjamin/Cummings,1994.
[65]Jacobson I.,Object-Oriented Software Engineering:A Use Case Driven Approach [M],Reading,MA:ACMPress,1992.
[66]Rumbaugh Jetal,Object-Oriented Modeling and Design[M],NewJersey:Yourdon Press,1991.
[67]周之英编,现代软件工程[M],北京:科学出版社,2000.
[68]Chen P.,The Entity-Relationship Model:Towards a Unified View of Data[J],ACM Transactions on Database System,1(1),1976.
[69]陈禹六,IDEFx建模分析和设计方法[M],北京:清华大学出版社,1999.
[70]James Rumbaugh,Ivar Jacobson,Grady Booch著,姚淑珍,唐发根译,UML参考手册[M],北京:机械工业出版社,2001.
[71]Matthew Hause,Matthew Hause,Modelling High Level Requirements in UML/SysML[C],INCOSE Symposium 2005,2005.
[72]Object Management Group(OMG)'2005,UML for Systems Modeling Language [EB/OL],http://www.sysml.org,2005.
[73]Yu,E.and Liu,L.,Modelling Trust for System Design Using the i* Strategic Actors Framework[C].In:Trust in CyberoSocieties-Integrating the Human and Artificial Perspectives,LNAI-2246,175-194,Springer,2001.
[74]Yu,E.and Cysneiros,L.M.Privacy,Security and Other Competing Requirements[C],Symposium on Requirements Engineering for Information Security(SREIS'02),Raleigh,North Carolina,Oct.,2002.
[75]Axel van Lamsweerde,From System Goals to Software Architecture[C],Proc.IEEE Symp.On Engineering of Computer-Based Systems 2002,2002.
[76]Axel van Lamsweerde and Emmanuel Letie,From Object Orientation to Goal Orientation:A Paradigm Shift for Requirements Engineering[C],Proc.IEEE Symp.On Engineering of Computer-Based Systems 2003,2003.
[77]Axel van Lamsweerde,Goal-oriented requirements engineering:From system objectives to UML models to precise software specifications[C],In ICSE 2003,744-745,2003.
[78]Steven J.Ring,An Activity-Based Methodology for Development and Analysis of Integrated DoD Architectures -'The Art of Architecture'[C],Command and Control Research and Technology Symposium 2004,2004.
[79]周婷,基于场景的需求工程[D],国防科技大学硕士学位论文,2003.3.
[80]ITU,Message Sequence Charts,Recommendation Z.120,International Telecommunications Union.Telecommunication Standardisation Sector,1996.
[81]Harel,D.,From play-in scenarios to code:An achievable dream[J],IEEE Computer,34(1):53-60,2001.
[82]吴宏,LSC模型检验研究与实现[D],国防科技大学硕士学位论文,2005.3.
[83]Amyot,D.,Andrade,R.,Logrippo,L.,Sincennes,J.,Yi,Z.,Formal Methods for Mobility Standards[EB/OL],IEEE 1999 Emerging Technology Symposium on Wireless Communication & Systems,Dallas,USA,http://www.UseCaseMaps.org/UseCaseMaps/pub/ets99.pdf,1999.
[84]Buhr,R.J.A.,Casselman,R.S.,Use Case Maps for Object-Oriented Systems[R],Prentice Hall Inc.,1996.
[85]金芝,基于本体的需求自动获取[J],计算机学报,23(5),2000.5.
[86]刘静,基于本体的C4ISR系统需求获取方法研究[J],军事运筹与指挥,24(2),2004.
[87]周伟,邓小妮,陈洪辉,罗雪山,基于本体的C4ISR系统需求描述框架研究[C],C3I系统与理论专业委员会第十二届学术年会论文集,2005年11月.
[88]Jackson M A.,Problem Frames:Analyzing and Structuring Software Development Problems[M],Harlow,Addison-Wesley,2001.
[89]吴永波,军事任务空间概念模型开发方法研究[D],国防科技大学博士学位论文,2005.10.
[90]Lt Col C W Bailey,Maj R M Garbutt,Developing Coherent,Concise And Comprehensive User Requirements Using The MoD Architectural Framework (MODAF)[C],2005 Command and Control Research and Technology Symposium,2005.
[91]邓小妮,陈洪辉,罗雪山,基于系统工程观点的C4ISR系统需求分析研究[C],C3I系统与理论专业委员会第十二届学术年会论文集,2005年11月.
[92]CMU/SEI:Camegie Mellon University/Software Engineering Insititute,The Capability Maturity Model:Guidelines for Improving the Software Process[R],Reading,MA:Addison-Wesley,1995.
[93]卡耐基梅隆大学软件工程研究所,能力成熟度模型(CMM):软件过程改进指南[M],北京:电子工业出版社,2001.7.
[94]田田,面向武警后勤信息化建设的军事需求统一管理模式研究[D],国防科技 大学硕士学位论文,2004.12.
[95]吕翔,军事需求变更影响分析方法及其在武警后勤信息化建设中的应用研究[D],国防科技大学硕士学位论文,2004.12.
[96]丹尼尔·弗里德曼,杰拉尔德·温伯格著,唐云深,胡庆培译,走查、审查与技术复审手册(第三版)[M],2003.
[97]董威,面向UML的模型检验研究[D],国防科技大学博士学位论文,2002.4.
[98]舒风笛,嵌入式实时软件系统的需求规约与验证[D],武汉大学博士学位论文,2003.12
[99]E.M.Clarke and E.A.Emerson,Design and Synthisis of Sysnchronization Skeletons Using Branching Time Temporal Logic[C],In Logic of Programs:Workshop,Yorktown Heights,NY,May 1981.
[100]J.P.Quielle and J.Sifakis,Specification and Verification of Concurrent Systems in CESAR[C],In Proceeding of the 5th International Symposium on Programming,LNCS 207,Springer-Verlag,337-350,1982.
[101]Kenneth L.McMillan,Sumbolic Model Checking[M],Kluwer Academic Publishers,American,1993.
[102]Patrice Godefroid,Using Partial Orders to Improve Automatic Verification Methods[C],In Proceedings of the 2nd Workshop on Computer-Aided Verification,LNSC 531,Springer,1990,176-185.
[103]Patrice Godefroid,Pierre Wolper.A Partial Approach to Model Checking[J].Information and Computation,110(2),305-326,1994.
[104]Y.Kesten,Z.Manna,H.McGuire,A.Pnueli,A Decision Algorithm for Full Propositional Temporal Logic[C],CAV'93,Elounda,Greece,LNCS 697,Springer-Verlag,97-109,1993.
[105]R.Gerth,D.Peled,M.Y.Vardi,P.Wolper,Simple On-the-fly Automatic Verification of Linear Temporal Logic.In Protocol Specification Testing and Verification,Chapman&Hall,London,3-18,1995.
[106]Zonghua Gu,Kang G.Shin,Analysis of Event-Driven Real-Time System with Time Petri Nets[C],Proceedings of the IFIP 17th World Computer Congress,31-40,2002.
[107]陆公正,戎玫,张广泉,基于稠密汗死简单实时系统模型检测的一个应用[J],苏州大学学报,25(2),2005.
[108]Rajeev Alur,David Dill,Automata-theoretic Verification of Real-Time Systems[C],Formal Methods for Real-Time Computing,Trends in Software Series,John Wiley & Sons Publishers,55-82,1996.
[109]K.L.McMillan,Getting Started with SMV[R],Cadence Berkeley Labs,1999.
[110]Gerard J.Holzmann and Doron Peled,The State of Spin[C],Proceedings of the 1997 Workshop on Computer-Aided Verification,385-389,1997.
[111]Paul Pettersson,Modelling and Verification of Real-Time Systems Using Timed Automata:Theory and Practice[D].PH.D.Dissertation,Uppsala University,February 1999.
[112]Marius Bozga,Conrado Daws,Oded Maler,Alfredo Olivero,Stavros Tdpakis,Sergio Yovine,Kronos:A Model-Checking Tool for Real-Time Systems[C],Proceedings of the 1998 Workshop on Computer-Aided Verification,546-550,1998.
[113]Ronald Lutje Spelberg,Hans Toetenel,Marcel Ammerlaan,Partition Refinement In Real-time Model Checking[C],In Formal Techniques in Real-Time and Fault-Tolerant Systems,5th International Symposium,mumber 1486 in Lecture Notes in Computer Science,143-157,Springer-Verlag.Lyngby,Denmark,1998.
[114]T.A.Henzinger,P.H.Ho,and H.Wong-Toi,HyTech:A Model Checker for Hybrid Systems[J],Software Tools for Technology Transer 1:110-122,1997.
[115]Erich Mikk,MOCES User's Guide[R].November1998.
[116]Levis A H,Wagenhals L W,C4ISR Architectures:Ⅰ.Developing a Process for C4ISR Architecture Design[J],Systems Engineering,3(4):225-247,2000.
[117]Wagenhals L W,Shin I,Kim D,Levis A H,C4ISR Architectures:Ⅱ.A Structured Analysis Approach for Architecture Design[J],Systems Engineering,3(4):248-287,2000.
[118]P.C.Barr,A.R.Bernstein,Executable Architecture for the First Digitized Division[C],Conference on Digitization of the Battlespace Ⅴ and Battlefield Biomedical Technologies Ⅱ24,Proceedings of SPIE,2000.
[119]黄力,基于StateChart图的C4ISR系统体系结构验证研究[D],国防科技大学博士学位论文,2004.4.
[120]Wagenhals L W,Haider S,Levis A H,Synthesizing Executable Models of Object Oriented Architectures[C],Workshop on Formal Methods Applied to Defence Systems,Adelaide,Australia,2002.
[121]李新强,C3I系统的功能需求分析与需求仿真研究[D],国防科技大学硕士学位论文,2001.12.
[122]修胜龙,C4ISR体系结构产品一致性开发及验证方法研究[D],国防科技大学博士学位论文,2004.10.
[123]http://www.telelogic.com/corp/products/tau/dodaf/automate-consistency-correctnes s-and-completeness.cfm
[124]朱雪峰,金芝,关于软件需求中的不一致性管理,软件学报[J],16(7),1221-1231,2005.
[125]Spanoudakis G,Finkelstein A,Till D,Overlaps in requirements engineering.Automated Software Engineering,6(2):171-198,1999.
[126]张家重,徐家福,需求工程研究新进展[J],计算机研究与发展,35(1):1-5,1998.
[127]张家重,吕建,王志坚,徐家福,一种图形化对象式需求定义语言的设计[J],软件学报,7(11):645-655,1996.
[128]丁俊华,孙圣强,杨大军,吕建,一种多视角的需求定义及其一致性验证方法[J],计算机研究与发展,35(3):229-233,1998.
[129]罗爱民,基于框架的C4ISR体系结构语法、语义设计与分析方法研究[D],国防科技大学博士学位论文,2006.10.
[130]陈洪辉,基于多视图的C4ISR系统需求一致性验证方法研究[D],国防科技大学博士学位论文,2007.10.
[131]MINISTRY OF DEFENCE,MOD Architectural Framework Viewpoint Overview Version 1.0,MINISTRY OF DEFENCE[R/OL].http://www.modaf.com/files/MODAF%20Viewpoint%20Overview%20vl.0.pdf,2005.8.
[132]B.Paech,A.Von Knethen,An Experience-Based Approach for Integrating Architecture and Requirements Engineering,2003
[133]Popkin 公,SA Simulator Ⅱ Training Materials[R],2003.
[134]Mayer,R.J.,IDEF3 process description capture method[J],Knowledge based systems,College Station,TX,1994.
[135]邓小妮,罗爱民等,军事电子信息系统效能分析与需求评价研究[R],中国国防技术报告,国防科技大学C3I研究中心,2005年9月.
[136]金芝,再论软件需求的含义[J],计算机科学技术学报(英文刊),17(1),2006.
[137]刘俊先,指挥自动化系统效能评价的概念与方法研究[D],国防科技大学博士学位论文,2003.12.
[138]IEEE,IEEE Std 1471-2000,IEEE Recommended Practice for Architectural Description of Software-Intensive Systems[S],2000.
[139]姜志平,基于CADM的C4ISR系统体系结构验证方法及关键技术研究[D],国防科技大学博士学位论文,2007.10.
[140]David Harel,From Play-In Scenarios to Code:An Achievable Dream[J],Computer Magazine,January 2001.
[141]Rajeev Alur and Mihalis Yannakakis,Model Checking of Message Sequence Charts[C],Proceedings of the 10th International Conference on Concurrency 114-129,1999.
[142]Jun Sun;Jin Song Dong;Model checking live sequence charts[C],Engineering of Complex Computer Systems 2005,529- 538,2005.
[143]罗雪山,张维明等,C3I系统理论基础--C3I系统建模方法与技术[M],国防科技大学出版社,2000。
[144]国防科技大学C3I研究中心,基于对象的Petri网建模仿真环境技术报告[R],长沙:国防科技大学,1999.
[145]袁崇义,Petri网原理[M],北京:电子工业出版社,1998.
[146]蒋昌俊,Petri网的行为理论及其应用,北京:高等教育出版社,2003.1.
[147]国防科技大学C3I研究中心,基于OPDL语言的C3I系统建模方法[R],长沙: 国防科技大学,1999.
[148]国防科技大学C3I研究中心,基于对象的Petri网建模仿真环境用户手册[R],长沙:国防科技大学,1999.
[149]E.M.Clarke,E.A.Emerson,Design and Synthesis of Sysnchronization Skeletons Using Branching Time Temporal Logic[C],Logic of Programs:Workshop,Yorktown Heights,NY,May 1981,LNCS131,Springer,1981.
[150]J.P.Quielle,J.Sifakis,Specification and Verification of Concurrent Systems in CESAR,Proceeding of the 5th International Symposium on Programing,LNCS 207,Springer-Verlag,337-350,1982.
[151]E.M.Clarke,E.A.Emerson,and A.P.Sistla,Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications[J],ACM Trans.on Programming Languages and Systems,vol.8,244-263,April 1986.
[152]蒋屹新,林闯等,基于Petri网的模型检测研究[J],软件学报,15(9),2005.
[153]R.Alur,C.Courcoubetis,and D.L.Dill,Model Checking for Real-Time Systems[C],In Proc.Symposium on Logic in Computer Science,414-425,1990.
[154]蒋宗礼,姜守旭,形式语言与自动机理论[M],北京:清华大学出版社,2003.
[155]R.Alur,Timed Automata[J],In D.A.Peled and N.Halbwachs,editors,Computer-Aided Verification,LNCS(1633):8-22,Berlin,1999.
[156]Rajeev Alur,David L.Dill,A theory of timed automata[J].Theoretical Computer Science,126(2):183-235,1994.
[157]Jonathan Lee,Jiann Pan,Jong Yih Kuo.Verifying scenarios with time Petri-nets.Information and Software Technology[J],43(2001):769-781,2001.
[158]OMG,Unified Modelling Language[EB/OL],http://www.omg.org/,2002.
[159]ITU.Message Sequence Charts,Recommendation Z.120[S],International Telecommunications Union.Telecommunication Standardisation Sector,1996.
[160]Reniers,M.A.,Message Sequence Chart.Syntax and Semantics[D],Ph.D.Thesis,Eindhoven University of Technology,1999.
[161]Heymer,S,A semantics for MSCs based on Petri net components[C],in proceedings of the 2nd Workshop on SDL and MSC(SAM'00),Grenoble,2000.
[162]王璐珍,董威,陈火旺,UML顺序图的自动验证[J],计算机工程与应用,29(2),2003.
[163]Aliki Tsiolakis,Semantic Analysis and Consistency Checking of UML Sequence Diagrams[R],Diplomarbeit,Technische Universit(a｜¨)t Berlin,Technical Report No.2001-06,April 2001.
[164]颜炯,基于UML的软件统计测试研究[D],国防科技大学博士学位论文,2005.4.
[165]I.Krtiger,R.Grosu,P.Scholz,and M.Broy,From MSCs to Statecharts[J],Distributed and Parallel Embedded Systems,F.J.Rammig,ed.,Kluwer Academic Publishers,61-71,1999.
[166]马骥桥等,EK-301系统工程实践论文集[R],太原:火力与指挥控制编辑部, 1996.
[167] P. Lind and S, Kvist, Jammer Model Description[R], Saab Bofors Dynamics AB,Link¨oping, April 2001.
[168] Ribeiro et al, Some Rules to Transform Sequence Diagrams into Coloured Petri Nets[C], In 7th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools (CPN 2006), 237-56,2006.
[169] Amorim et al, A methodology for mapping live sequence chart to coloured Petri net[C], IEEE International Conference on Systems, Man and Cybernetics, volume4,2999-3004,2005.
[2]于云程,罗雪山,C3I系统分析与设计[M],长沙:国防科技大学出版社,1996.
[3]竺南直,指挥自动化系统工程[M],电子工业出版社,2001.
[4]RADC,System/Software Requirements Engineering Testbed Research &development Program,AD-A 197858,1988.
[5]U.S.,Joint Chiefs of Staff,Joint Vision 2010[EB/OL],http://www.dtic.mil/jv2010,1996.
[6]U.S.,Joint Chiefs of Staff,Joint Vision 2020[EB/OL],http://www.dtic.mil/jv2020,2000.
[7]C4ISR Architecture Working Group,C4ISR Architecture Framework Version 1.0[R],U.S.:Department of Defense,1996.
[8]C4ISR Architecture Working Group,C4ISR Architecture Framework Version 2.0[R],U.S.:Department of Defense,1997.
[9]DoD Architecture Framework Working Group,DoD Architecture Framework Version 1.0 Volume Ⅰ:Definitions and Guidelines[R],U.S.:Department of Defense,2003.
[10]国防科技大学C3I中心,指挥信息系统需求工程[R],长沙:国防科技大学,2006.2.
[11]Richardson,K.A.,Mathieson,G.and Cilliers,P.,The Theory and Practice of Complexity Science - Epistemological Considerations for Military Operational Analysis,SysteMexico,1:25-66,2000.
[12]军事科学院战役战术研究部,高技术条件下作战对区域综合电子信息系统的需求分析论证报告[R],北京:军事科学院,1997.
[13]空军第三研究所,空军本级基本指挥所指挥自动化系统需求分析报告[R],北京:空军第三研究所,2001.
[14]空军第八研究所,空军武器装备体系对抗论证仿真系统指挥自动化仿真分系统软件需求规格说明[R],北京:空军第八研究所,2002.
[15]空军第三研究所,“长空-3J”系统需求分析过程说明报告[R],中国国防科学技术报告,空军第三研究所需求工程技术应用研究课题组,2003.
[16]中国国防科学技术报告,需求分析方法总结报告[R],空军第三研究所需求工程技术应用研究课题组,2003.
[17]IEEE,IEEE Std 610.12-1997,IEEE Standard Glossary of Software Engineering Terminology[EB/OL],http://www.ieee.com/,2003.
[18]OMG,Requirements Analysis for UML for Systems Engineering(Draft V0.4)[EB/OL],http://www.omg.com/rw/euml,2003.
[19]Alan M.Davis,Software Requirements:Objects,Functions,and States,Englewood Cliffs,NJ:PTR Prentice Hall,1993.
[20]Karl E.Wiegers著,陆丽娜等译,软件需求[M],北京:机械工业出版社,2000.
[21]Jones Capers,Assessment and Control of Software Risks,Englewood Cliffs,NJ:PTR Prentice Hall,1994.
[22]Suzanne Robertson,James Robertson著,王海鹏译,掌握需求过程[M],北京:人民邮电出版社,2003.
[23]Ralph R.Young著,韩柯等译,有效需求实践[M],北京:机械工业出版社,2002.
[24]Telelogic,Rational Unified Process:Best Practices for Software Development Teams,A Rational Software Corporation White Paper[EB/OL],http://www.uml.org.cn/SoftWareProcess/ pdf/RUP_BestPractics_Chinese.pdf,2003.
[25]李明树,王青,需求工程研究现状[J],中国计算机用户,395(47),1999.
[26]Siddiqi J,Shekaran MC.Requirements engineering:The emerging wisdom[J],IEEE Software,23(3):15-19,1996.
[27]Jarke M,Pohl K.,Requirements engineering:Managing a changing reality,Software Engineering,20(11):257-266,2001.
[28]Thayer,Richard H.,Merlin Dorfman,eds,Software Requirements Engineering[M],Los Alamitos,CA:IEEE Computer Society Press,1997.
[29]IEEE,Terms,Acronyms and Abbreviations[EB/OL],http://www.ieee.com/,2004.
[30]Suzanne Robertson,and James Robertson,Mastering the Requirements Process[M],Harlow,England:Addison-Wesley,1999.
[31]IEEE Std 830-1998,IEEE Recommended Practice for Software Requirements SpeciPcations[EB/OL],http://www.ieee.com/,2003.
[32]IEEE Std-1233-1998,IEEE Guide for Developing System Requirements SpeciPcations[EB/OL],http://www.ieee.com/,2003.
[33]M.Elizabeth C.Hull,Ken Jackson,A.Jeremy J.Dick著,韩柯译,需求工程[M],北京:机械电子出版社,2002.
[34]Karl E.Wiegers著,刘伟琴,刘洪涛译,软件需求(第2版)[M],北京:清华大学出版社,2004.
[35]Hooks,I.,Writing Good Requirements[C],Proceedings of the Third International Symposium ofNCOSE,Vol 2,1993.
[36]唐纳德.高斯,杰拉尔德.温伯格著,章柏幸等译,探索需求:设计前的质量[M],北京:清华大学出版社,2004.
[37]Ian K.Bray著,舒忠梅等译,需求工程导引[M],北京:人民邮电出版社,2003.
[38]Daniel R.Windel,L.Rene Abreo,Software Requiements Using the Unified Process:aPractical Approach[M],软件需求:基于统一过程的实践方法(影印版) [M],北京:中国电力出版社,2003.
[39]Soren Lauesen著,刘晓晖译,软件需求[M],北京:电子工业出版社,2002.
[40]OMG,Unified Modelling Language[EB/OL],http://www.omg.org/,2002.
[41]BjoernerD,On the use of formal methods in software development[C],9th International Conference on Software Engineering,1989.
[42]Norries MZ,A formal specification method[C],In:Thayer RH,Dorfman Meds.Tutorial:System and Software Requirements Engineering.LosAlamitos,CA:IEEE Computer Society Press,345-369,1990.
[43]http://www.incose.org/rwg/
[44]Richard Harwell,Erik Aslaksen,Ivy Hooks,What is a requirement?[C],Proceedings of the 3rd Annual International Symposium,NCOSE,1996.
[45]Pradip Kar,Michelle Bailey,Characteristics of Good Requirements[C],INCOSE Symposium,1996.
[46]INCOSE,Requiements body of Knowledge[EB/OL],http://www.incose.com/BOK/,2002.
[47]OMG,Requirements Analysis for UML for Systems Engineering(Draft V0.4)[EB/OL],http://www.omg.com/se/sysuml.htm,2003.
[48]邵全琴等,迭代演进式GIS需求分析模型研究[J],遥感学报,Vol.5(5):358-366,2001.
[49]Mary Frances Theofanos,Shair Lawrence Pfleeger,Wave front:A Goal-driven Requirements Process Model[J],Information on Software Technology,38:507-519,1996.
[50]N.A.M.Maiden,S.V.Jones,S.Manning,J.Greenwoodl,L.Renou,Model-Driven Requirements Engineering:Synchronising Models in an Air Traffic Management Case[C],CASE'2004,2004.
[51]Ivar Jacobson,Grady Booch,James Rumbaugh著,周伯生等译,统一软件开发过程,北京:机械工业出版社,2002.
[52]James & Suzanne Robertson,Volere Requirements Specification Template(Edition 9),http://www.volere.co.uk,2003.
[53]Chairman of the Joint Chiefs of Staff Instruction,CJCSI 3170.01B[I],April 2001.
[54]Chairman of the Joint Chiefs of Staff Instruction,CJCSI 3170.01C[I],August 2002.
[55]Chairman of the Joint Chiefs of Staff Instruction,CJCSI 3170.01D[I],October 2004.
[56]Chairman of the Joint Chiefs of Staff Instruction,CJCSI 3170.01E[I],March 2005.
[57]Svoboda C P,Structured analysis[J],In:Thayer R H,Dorfmaneds.Tutorial:System and Software Requirements Engineering.Los Alamitos,CA:IEEE Computer Society Press,218-237,1990.
[58]Ross DT,Structured analysis(SA):A language for communication ideas[J],IEEE Transition on Software Engineering,1(1):16-34,1977.
[59]Zave P,An insider's evaluation of PAISLey[J],IEEE Transition on Software Engineering,17(3):212-225,1991.
[60]Urban JE,The Descartes specification language[C].In:ThayerRH,Dorfmaneds.Tutorial:System and Software Requirements Engineering,LosAlamitos,CA:IEEE Computer Society Press,331-344,1990.
[61]Chen P.,Entity-relationship approach to data modeling[C],In:Thayer RH,Dorfman Meds.Tutorial:System and Software Requirements Engineering,Los Alamitos,CA:IEEE Computer Society Press,238-243:1990.
[62]Cameron JR,A over view of JSD,IEEE Transaction on Software Engineering 12(2):43-46,1986.
[63]Yourdon E.,Coad P.,Object-Oriented Analysis(2nd Edition)[M],NewJersey:Yourdon Press,1991.
[64]Booch Getal,Software Engineering with Ada(3rd Edition)[M],Edwood City,Calif:Benjamin/Cummings,1994.
[65]Jacobson I.,Object-Oriented Software Engineering:A Use Case Driven Approach [M],Reading,MA:ACMPress,1992.
[66]Rumbaugh Jetal,Object-Oriented Modeling and Design[M],NewJersey:Yourdon Press,1991.
[67]周之英编,现代软件工程[M],北京:科学出版社,2000.
[68]Chen P.,The Entity-Relationship Model:Towards a Unified View of Data[J],ACM Transactions on Database System,1(1),1976.
[69]陈禹六,IDEFx建模分析和设计方法[M],北京:清华大学出版社,1999.
[70]James Rumbaugh,Ivar Jacobson,Grady Booch著,姚淑珍,唐发根译,UML参考手册[M],北京:机械工业出版社,2001.
[71]Matthew Hause,Matthew Hause,Modelling High Level Requirements in UML/SysML[C],INCOSE Symposium 2005,2005.
[72]Object Management Group(OMG)'2005,UML for Systems Modeling Language [EB/OL],http://www.sysml.org,2005.
[73]Yu,E.and Liu,L.,Modelling Trust for System Design Using the i* Strategic Actors Framework[C].In:Trust in CyberoSocieties-Integrating the Human and Artificial Perspectives,LNAI-2246,175-194,Springer,2001.
[74]Yu,E.and Cysneiros,L.M.Privacy,Security and Other Competing Requirements[C],Symposium on Requirements Engineering for Information Security(SREIS'02),Raleigh,North Carolina,Oct.,2002.
[75]Axel van Lamsweerde,From System Goals to Software Architecture[C],Proc.IEEE Symp.On Engineering of Computer-Based Systems 2002,2002.
[76]Axel van Lamsweerde and Emmanuel Letie,From Object Orientation to Goal Orientation:A Paradigm Shift for Requirements Engineering[C],Proc.IEEE Symp.On Engineering of Computer-Based Systems 2003,2003.
[77]Axel van Lamsweerde,Goal-oriented requirements engineering:From system objectives to UML models to precise software specifications[C],In ICSE 2003,744-745,2003.
[78]Steven J.Ring,An Activity-Based Methodology for Development and Analysis of Integrated DoD Architectures -'The Art of Architecture'[C],Command and Control Research and Technology Symposium 2004,2004.
[79]周婷,基于场景的需求工程[D],国防科技大学硕士学位论文,2003.3.
[80]ITU,Message Sequence Charts,Recommendation Z.120,International Telecommunications Union.Telecommunication Standardisation Sector,1996.
[81]Harel,D.,From play-in scenarios to code:An achievable dream[J],IEEE Computer,34(1):53-60,2001.
[82]吴宏,LSC模型检验研究与实现[D],国防科技大学硕士学位论文,2005.3.
[83]Amyot,D.,Andrade,R.,Logrippo,L.,Sincennes,J.,Yi,Z.,Formal Methods for Mobility Standards[EB/OL],IEEE 1999 Emerging Technology Symposium on Wireless Communication & Systems,Dallas,USA,http://www.UseCaseMaps.org/UseCaseMaps/pub/ets99.pdf,1999.
[84]Buhr,R.J.A.,Casselman,R.S.,Use Case Maps for Object-Oriented Systems[R],Prentice Hall Inc.,1996.
[85]金芝,基于本体的需求自动获取[J],计算机学报,23(5),2000.5.
[86]刘静,基于本体的C4ISR系统需求获取方法研究[J],军事运筹与指挥,24(2),2004.
[87]周伟,邓小妮,陈洪辉,罗雪山,基于本体的C4ISR系统需求描述框架研究[C],C3I系统与理论专业委员会第十二届学术年会论文集,2005年11月.
[88]Jackson M A.,Problem Frames:Analyzing and Structuring Software Development Problems[M],Harlow,Addison-Wesley,2001.
[89]吴永波,军事任务空间概念模型开发方法研究[D],国防科技大学博士学位论文,2005.10.
[90]Lt Col C W Bailey,Maj R M Garbutt,Developing Coherent,Concise And Comprehensive User Requirements Using The MoD Architectural Framework (MODAF)[C],2005 Command and Control Research and Technology Symposium,2005.
[91]邓小妮,陈洪辉,罗雪山,基于系统工程观点的C4ISR系统需求分析研究[C],C3I系统与理论专业委员会第十二届学术年会论文集,2005年11月.
[92]CMU/SEI:Camegie Mellon University/Software Engineering Insititute,The Capability Maturity Model:Guidelines for Improving the Software Process[R],Reading,MA:Addison-Wesley,1995.
[93]卡耐基梅隆大学软件工程研究所,能力成熟度模型(CMM):软件过程改进指南[M],北京:电子工业出版社,2001.7.
[94]田田,面向武警后勤信息化建设的军事需求统一管理模式研究[D],国防科技 大学硕士学位论文,2004.12.
[95]吕翔,军事需求变更影响分析方法及其在武警后勤信息化建设中的应用研究[D],国防科技大学硕士学位论文,2004.12.
[96]丹尼尔·弗里德曼,杰拉尔德·温伯格著,唐云深,胡庆培译,走查、审查与技术复审手册(第三版)[M],2003.
[97]董威,面向UML的模型检验研究[D],国防科技大学博士学位论文,2002.4.
[98]舒风笛,嵌入式实时软件系统的需求规约与验证[D],武汉大学博士学位论文,2003.12
[99]E.M.Clarke and E.A.Emerson,Design and Synthisis of Sysnchronization Skeletons Using Branching Time Temporal Logic[C],In Logic of Programs:Workshop,Yorktown Heights,NY,May 1981.
[100]J.P.Quielle and J.Sifakis,Specification and Verification of Concurrent Systems in CESAR[C],In Proceeding of the 5th International Symposium on Programming,LNCS 207,Springer-Verlag,337-350,1982.
[101]Kenneth L.McMillan,Sumbolic Model Checking[M],Kluwer Academic Publishers,American,1993.
[102]Patrice Godefroid,Using Partial Orders to Improve Automatic Verification Methods[C],In Proceedings of the 2nd Workshop on Computer-Aided Verification,LNSC 531,Springer,1990,176-185.
[103]Patrice Godefroid,Pierre Wolper.A Partial Approach to Model Checking[J].Information and Computation,110(2),305-326,1994.
[104]Y.Kesten,Z.Manna,H.McGuire,A.Pnueli,A Decision Algorithm for Full Propositional Temporal Logic[C],CAV'93,Elounda,Greece,LNCS 697,Springer-Verlag,97-109,1993.
[105]R.Gerth,D.Peled,M.Y.Vardi,P.Wolper,Simple On-the-fly Automatic Verification of Linear Temporal Logic.In Protocol Specification Testing and Verification,Chapman&Hall,London,3-18,1995.
[106]Zonghua Gu,Kang G.Shin,Analysis of Event-Driven Real-Time System with Time Petri Nets[C],Proceedings of the IFIP 17th World Computer Congress,31-40,2002.
[107]陆公正,戎玫,张广泉,基于稠密汗死简单实时系统模型检测的一个应用[J],苏州大学学报,25(2),2005.
[108]Rajeev Alur,David Dill,Automata-theoretic Verification of Real-Time Systems[C],Formal Methods for Real-Time Computing,Trends in Software Series,John Wiley & Sons Publishers,55-82,1996.
[109]K.L.McMillan,Getting Started with SMV[R],Cadence Berkeley Labs,1999.
[110]Gerard J.Holzmann and Doron Peled,The State of Spin[C],Proceedings of the 1997 Workshop on Computer-Aided Verification,385-389,1997.
[111]Paul Pettersson,Modelling and Verification of Real-Time Systems Using Timed Automata:Theory and Practice[D].PH.D.Dissertation,Uppsala University,February 1999.
[112]Marius Bozga,Conrado Daws,Oded Maler,Alfredo Olivero,Stavros Tdpakis,Sergio Yovine,Kronos:A Model-Checking Tool for Real-Time Systems[C],Proceedings of the 1998 Workshop on Computer-Aided Verification,546-550,1998.
[113]Ronald Lutje Spelberg,Hans Toetenel,Marcel Ammerlaan,Partition Refinement In Real-time Model Checking[C],In Formal Techniques in Real-Time and Fault-Tolerant Systems,5th International Symposium,mumber 1486 in Lecture Notes in Computer Science,143-157,Springer-Verlag.Lyngby,Denmark,1998.
[114]T.A.Henzinger,P.H.Ho,and H.Wong-Toi,HyTech:A Model Checker for Hybrid Systems[J],Software Tools for Technology Transer 1:110-122,1997.
[115]Erich Mikk,MOCES User's Guide[R].November1998.
[116]Levis A H,Wagenhals L W,C4ISR Architectures:Ⅰ.Developing a Process for C4ISR Architecture Design[J],Systems Engineering,3(4):225-247,2000.
[117]Wagenhals L W,Shin I,Kim D,Levis A H,C4ISR Architectures:Ⅱ.A Structured Analysis Approach for Architecture Design[J],Systems Engineering,3(4):248-287,2000.
[118]P.C.Barr,A.R.Bernstein,Executable Architecture for the First Digitized Division[C],Conference on Digitization of the Battlespace Ⅴ and Battlefield Biomedical Technologies Ⅱ24,Proceedings of SPIE,2000.
[119]黄力,基于StateChart图的C4ISR系统体系结构验证研究[D],国防科技大学博士学位论文,2004.4.
[120]Wagenhals L W,Haider S,Levis A H,Synthesizing Executable Models of Object Oriented Architectures[C],Workshop on Formal Methods Applied to Defence Systems,Adelaide,Australia,2002.
[121]李新强,C3I系统的功能需求分析与需求仿真研究[D],国防科技大学硕士学位论文,2001.12.
[122]修胜龙,C4ISR体系结构产品一致性开发及验证方法研究[D],国防科技大学博士学位论文,2004.10.
[123]http://www.telelogic.com/corp/products/tau/dodaf/automate-consistency-correctnes s-and-completeness.cfm
[124]朱雪峰,金芝,关于软件需求中的不一致性管理,软件学报[J],16(7),1221-1231,2005.
[125]Spanoudakis G,Finkelstein A,Till D,Overlaps in requirements engineering.Automated Software Engineering,6(2):171-198,1999.
[126]张家重,徐家福,需求工程研究新进展[J],计算机研究与发展,35(1):1-5,1998.
[127]张家重,吕建,王志坚,徐家福,一种图形化对象式需求定义语言的设计[J],软件学报,7(11):645-655,1996.
[128]丁俊华,孙圣强,杨大军,吕建,一种多视角的需求定义及其一致性验证方法[J],计算机研究与发展,35(3):229-233,1998.
[129]罗爱民,基于框架的C4ISR体系结构语法、语义设计与分析方法研究[D],国防科技大学博士学位论文,2006.10.
[130]陈洪辉,基于多视图的C4ISR系统需求一致性验证方法研究[D],国防科技大学博士学位论文,2007.10.
[131]MINISTRY OF DEFENCE,MOD Architectural Framework Viewpoint Overview Version 1.0,MINISTRY OF DEFENCE[R/OL].http://www.modaf.com/files/MODAF%20Viewpoint%20Overview%20vl.0.pdf,2005.8.
[132]B.Paech,A.Von Knethen,An Experience-Based Approach for Integrating Architecture and Requirements Engineering,2003
[133]Popkin 公,SA Simulator Ⅱ Training Materials[R],2003.
[134]Mayer,R.J.,IDEF3 process description capture method[J],Knowledge based systems,College Station,TX,1994.
[135]邓小妮,罗爱民等,军事电子信息系统效能分析与需求评价研究[R],中国国防技术报告,国防科技大学C3I研究中心,2005年9月.
[136]金芝,再论软件需求的含义[J],计算机科学技术学报(英文刊),17(1),2006.
[137]刘俊先,指挥自动化系统效能评价的概念与方法研究[D],国防科技大学博士学位论文,2003.12.
[138]IEEE,IEEE Std 1471-2000,IEEE Recommended Practice for Architectural Description of Software-Intensive Systems[S],2000.
[139]姜志平,基于CADM的C4ISR系统体系结构验证方法及关键技术研究[D],国防科技大学博士学位论文,2007.10.
[140]David Harel,From Play-In Scenarios to Code:An Achievable Dream[J],Computer Magazine,January 2001.
[141]Rajeev Alur and Mihalis Yannakakis,Model Checking of Message Sequence Charts[C],Proceedings of the 10th International Conference on Concurrency 114-129,1999.
[142]Jun Sun;Jin Song Dong;Model checking live sequence charts[C],Engineering of Complex Computer Systems 2005,529- 538,2005.
[143]罗雪山,张维明等,C3I系统理论基础--C3I系统建模方法与技术[M],国防科技大学出版社,2000。
[144]国防科技大学C3I研究中心,基于对象的Petri网建模仿真环境技术报告[R],长沙:国防科技大学,1999.
[145]袁崇义,Petri网原理[M],北京:电子工业出版社,1998.
[146]蒋昌俊,Petri网的行为理论及其应用,北京:高等教育出版社,2003.1.
[147]国防科技大学C3I研究中心,基于OPDL语言的C3I系统建模方法[R],长沙: 国防科技大学,1999.
[148]国防科技大学C3I研究中心,基于对象的Petri网建模仿真环境用户手册[R],长沙:国防科技大学,1999.
[149]E.M.Clarke,E.A.Emerson,Design and Synthesis of Sysnchronization Skeletons Using Branching Time Temporal Logic[C],Logic of Programs:Workshop,Yorktown Heights,NY,May 1981,LNCS131,Springer,1981.
[150]J.P.Quielle,J.Sifakis,Specification and Verification of Concurrent Systems in CESAR,Proceeding of the 5th International Symposium on Programing,LNCS 207,Springer-Verlag,337-350,1982.
[151]E.M.Clarke,E.A.Emerson,and A.P.Sistla,Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications[J],ACM Trans.on Programming Languages and Systems,vol.8,244-263,April 1986.
[152]蒋屹新,林闯等,基于Petri网的模型检测研究[J],软件学报,15(9),2005.
[153]R.Alur,C.Courcoubetis,and D.L.Dill,Model Checking for Real-Time Systems[C],In Proc.Symposium on Logic in Computer Science,414-425,1990.
[154]蒋宗礼,姜守旭,形式语言与自动机理论[M],北京:清华大学出版社,2003.
[155]R.Alur,Timed Automata[J],In D.A.Peled and N.Halbwachs,editors,Computer-Aided Verification,LNCS(1633):8-22,Berlin,1999.
[156]Rajeev Alur,David L.Dill,A theory of timed automata[J].Theoretical Computer Science,126(2):183-235,1994.
[157]Jonathan Lee,Jiann Pan,Jong Yih Kuo.Verifying scenarios with time Petri-nets.Information and Software Technology[J],43(2001):769-781,2001.
[158]OMG,Unified Modelling Language[EB/OL],http://www.omg.org/,2002.
[159]ITU.Message Sequence Charts,Recommendation Z.120[S],International Telecommunications Union.Telecommunication Standardisation Sector,1996.
[160]Reniers,M.A.,Message Sequence Chart.Syntax and Semantics[D],Ph.D.Thesis,Eindhoven University of Technology,1999.
[161]Heymer,S,A semantics for MSCs based on Petri net components[C],in proceedings of the 2nd Workshop on SDL and MSC(SAM'00),Grenoble,2000.
[162]王璐珍,董威,陈火旺,UML顺序图的自动验证[J],计算机工程与应用,29(2),2003.
[163]Aliki Tsiolakis,Semantic Analysis and Consistency Checking of UML Sequence Diagrams[R],Diplomarbeit,Technische Universit(a｜¨)t Berlin,Technical Report No.2001-06,April 2001.
[164]颜炯,基于UML的软件统计测试研究[D],国防科技大学博士学位论文,2005.4.
[165]I.Krtiger,R.Grosu,P.Scholz,and M.Broy,From MSCs to Statecharts[J],Distributed and Parallel Embedded Systems,F.J.Rammig,ed.,Kluwer Academic Publishers,61-71,1999.
[166]马骥桥等,EK-301系统工程实践论文集[R],太原:火力与指挥控制编辑部, 1996.
[167] P. Lind and S, Kvist, Jammer Model Description[R], Saab Bofors Dynamics AB,Link¨oping, April 2001.
[168] Ribeiro et al, Some Rules to Transform Sequence Diagrams into Coloured Petri Nets[C], In 7th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools (CPN 2006), 237-56,2006.
[169] Amorim et al, A methodology for mapping live sequence chart to coloured Petri net[C], IEEE International Conference on Systems, Man and Cybernetics, volume4,2999-3004,2005.
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |