复杂信息系统模型的形式化验证方法研究
|
摘要
软件的质量和可靠性问题由来己久。目前，虽然软件分析、设计和测试技术仍是保障软件可靠性的主要手段，但是由于人们对软件系统分布式处理，并发处理，实时处理等能力要求的日益增强，使软件系统正日益趋向高度的复杂化，导致上述方法仍然不能完全满足开发高可靠软件系统的需要。模型检测作为一种形式化验证技术因其严格的数学基础、全自动的验证过程，以及早期在硬件系统和协议验证中的成功应用而倍受学术界和产业界的关注。但是在软件工程各阶段中结合模型检测，全面、自动的分析和验证复杂信息系统的需求、设计及性能模型、提高软件的安全性和可靠性尚处于探索阶段。针对上述问题，论文在软件工程中结合形式化方法与模型检测技术，分别从需求分析层面、模型设计层面以及性能设计层面研究具有分布式、并发和实时行为特性的复杂信息系统形式化建模及验证技术：
首先，对形式化方法及模型检测技术的相关研究进行了综述，阐述了复杂信息系统的行为特征，分析了复杂信息系统形式化建模及验证工作的重点与难点，总结了该领域存在的问题以及未来的研究方向。
其次，为验证复杂信息系统需求模型设计的正确性，将复杂信息系统的软件需求划分为顶层需求和技术层面需求，使用面向行为的抽象方法将领域政策建模为系统的顶层需求模型，并用RSL对其进行形式化规约。为验证及细化顶层需求模型，本文通过定义RSL语法及语义的转换规则将顶层需求模型的RSL规约转换为Promela模型，将顶层需求的性质规约描述为时态逻辑公式，最后使用模型检测器SPIN自动验证顶层需求模型对性质规约的可满足性。
再次，为验证复杂信息系统技术层面需求模型设计的正确性，首先用UML顺序图建模复杂信息系统的动态交互场景；针对UML顺序图模型缺乏精确的动态语义以及不能自动验证模型动态性质的问题，为UML顺序图定义迁移系统操作语义及其到Promela模型的转换规则，将顺序图模型的XMI描述文件的解析信息自动转换为Promela程序；最后，将建模系统需求的Promela程序和描述系统性质规约的线性时序逻辑公式作为模型检测器SPIN的输入，自动验证系统技术层面需求模型设计的正确性。
第四，为验证复杂信息系统设计模型的正确性，以UML状态图为系统建模的主要工具，使用元组定义UML状态图的主要元素，从而给出一种状态图模型的中间表示形式将层次状态图转化为平面状态图；基于该中间表示形式定义状态图模型的操作语义，设计复杂信息系统设计模型到NuSMV输入模型的语义转换规则；基于转换规则以及设计模型的XMI文档解析信息实现设计模型到NuSMV输入模型的自动转换过程，并通过证明状态图的操作语义与转换得到的NuSMV输入模块的操作语义为互模拟等价关系证明转换过程的正确性；最后使用模型检测器NuSMV验证复杂信息系统设计模型对其性质规范的可满足性。
最后，研究复杂信息系统实时性能设计的形式化验证技术，在需求分析过程中使用UML协作图建模系统的任务体系结构，描述当外部事件到达时系统内部事件和任务的激活顺序；用事件顺序分析方法为并发任务分配执行时间预算，将UML协作图扩展为实时协作图；基于实时协作图模型构建并发系统的时间自动机网络，并将其输入到模型检测工具UPPAAL执行自动验证。
最后，总结论文工作，并提出了下一步的研究方向。
Some problems on software quality and reliability have been existing for a long time.Although requirement analysis, design and test techniques are still the major means whichguarantee high reliability of software engineering, they can’t fully meet the requirement of thedevelopment of highly reliable software systems. Because people’s requirements for theability such as distributed processing, parallel processing, real-time processing of softwaresystem is increasingly improving, which makes software systems growing more and morecomplex. Model checking as a formal verification technique gets much attention fromacademia and industry, because of its strict mathematical basis, fully automated validationprocess and early successful application in the hardware system and protocol verification.However, applying model checking in various stages of software engineering is still in theexploratory stage, which can make a comprehensive and automated analysis and verify thecomplicated information system’s requirements, design and performance to improve softwaresecurity and reliability. According to the above problems, this dissertation combines formalmethods and model checking technique to make a research on modeling and formalverification technique of complicated information system whose behavior has distributed,concurrent and real-time characteristics from the perspective of requirement analysis level,model design level and performance design level.
First, formal methods and model checking techniques have been reviewed in thisresearch. The behavior characteristics of complicated information system are illustrated andthe emphasis and difficulty of formal model and verification is analyzied. Then someproblems in this field and the future research are concluded.
Second, to validate the correctness of the requirements design of complicatedinformation system, this research divides the software requirements into top-level andtechnical-level requirements, and uses behavior-oriented abstract modeling approach to modeldomain policies as top-level requirements of system, and specifies the requirement modelwith RSL. To validate and refine the top-level requirements model, this dissertation translatesthe RSL specification of the top-level requirements model into a Promela model by definingthe transformation rules of syntax and semantics of RSL. The property specification oftop-level requirements model is encoded to temporal logic formula. Finally, using the modelchecker SPIN automatically verifies whether the top-level requirements model can satisfy thetemporal logic formula.
Third, to validate the correctness of technical-level requirements design, UML sequencediagrams are used to model the interactive scenes of complicated information system.Because UML sequence diagrams model lacks of accurate dynamic semantics, and can notautomatically validate the dynamic nature of the model, this dissertation defines operationalsemantics of transition system for UML sequence diagram and defines its transformation rulesfrom UML sequence diagram to promela model. The parse result of XML file of sequencediagrams is converted to promela program. At last, the promela program which describes thesystem requirements and linear temporal logic which describes the specification of system areused to be the input of model checker SPIN automatically validating the correctness oftechnical-level requirements design of systems.
Forth, to validate the correctness of design model of complicated information system,UML statecharts are used to be the major modeling tool. The middle representation of theUML statecharts which transform hierarchical statecharts to flat statecharts is given bydefining the major elements of UML statecharts with tuple. On the basis of middlerepresentation, the operational semantics of UML statecharts is defined, the transformationrules from complicated information system’s design model to NuSMV input model aredesigned. Based on this transformation rules and the parse result of XML file of UMLstatecharts, the automatic transformation process from design model to NuSMV input modelis realized. The correctness of the transformation process is illustrated by proving thebisimulation equivalence relation between the operational semantics of UML statecharts andNuSMV input model which is generated by transformation rules. Finally, the model checkerNuSMV is used to verify whether the design model of complicated information system cansatisfy the property specification.
Furthermore, this dissertation makes a research on fomal verification technique ofreal-time performance design of complicated information system. The task architecture whichdescribes the activating order of internal event and task when external event arrives is createdby UML collaboration diagram in the requirement process. Then the execution time budget ofconcurrent task is allocated by events order analysis method and the UML collaborationdiagram is extend to real-time collaboration diagram. Ultimately, the timed automata networkis established on the basis of real-time collaboration diagram, and is input into the modelchecker UPPAAL for automated verification.
In the end, the work of the dissertation is concluded and the further research direction isput forward
首先，对形式化方法及模型检测技术的相关研究进行了综述，阐述了复杂信息系统的行为特征，分析了复杂信息系统形式化建模及验证工作的重点与难点，总结了该领域存在的问题以及未来的研究方向。
其次，为验证复杂信息系统需求模型设计的正确性，将复杂信息系统的软件需求划分为顶层需求和技术层面需求，使用面向行为的抽象方法将领域政策建模为系统的顶层需求模型，并用RSL对其进行形式化规约。为验证及细化顶层需求模型，本文通过定义RSL语法及语义的转换规则将顶层需求模型的RSL规约转换为Promela模型，将顶层需求的性质规约描述为时态逻辑公式，最后使用模型检测器SPIN自动验证顶层需求模型对性质规约的可满足性。
再次，为验证复杂信息系统技术层面需求模型设计的正确性，首先用UML顺序图建模复杂信息系统的动态交互场景；针对UML顺序图模型缺乏精确的动态语义以及不能自动验证模型动态性质的问题，为UML顺序图定义迁移系统操作语义及其到Promela模型的转换规则，将顺序图模型的XMI描述文件的解析信息自动转换为Promela程序；最后，将建模系统需求的Promela程序和描述系统性质规约的线性时序逻辑公式作为模型检测器SPIN的输入，自动验证系统技术层面需求模型设计的正确性。
第四，为验证复杂信息系统设计模型的正确性，以UML状态图为系统建模的主要工具，使用元组定义UML状态图的主要元素，从而给出一种状态图模型的中间表示形式将层次状态图转化为平面状态图；基于该中间表示形式定义状态图模型的操作语义，设计复杂信息系统设计模型到NuSMV输入模型的语义转换规则；基于转换规则以及设计模型的XMI文档解析信息实现设计模型到NuSMV输入模型的自动转换过程，并通过证明状态图的操作语义与转换得到的NuSMV输入模块的操作语义为互模拟等价关系证明转换过程的正确性；最后使用模型检测器NuSMV验证复杂信息系统设计模型对其性质规范的可满足性。
最后，研究复杂信息系统实时性能设计的形式化验证技术，在需求分析过程中使用UML协作图建模系统的任务体系结构，描述当外部事件到达时系统内部事件和任务的激活顺序；用事件顺序分析方法为并发任务分配执行时间预算，将UML协作图扩展为实时协作图；基于实时协作图模型构建并发系统的时间自动机网络，并将其输入到模型检测工具UPPAAL执行自动验证。
最后，总结论文工作，并提出了下一步的研究方向。
Some problems on software quality and reliability have been existing for a long time.Although requirement analysis, design and test techniques are still the major means whichguarantee high reliability of software engineering, they can’t fully meet the requirement of thedevelopment of highly reliable software systems. Because people’s requirements for theability such as distributed processing, parallel processing, real-time processing of softwaresystem is increasingly improving, which makes software systems growing more and morecomplex. Model checking as a formal verification technique gets much attention fromacademia and industry, because of its strict mathematical basis, fully automated validationprocess and early successful application in the hardware system and protocol verification.However, applying model checking in various stages of software engineering is still in theexploratory stage, which can make a comprehensive and automated analysis and verify thecomplicated information system’s requirements, design and performance to improve softwaresecurity and reliability. According to the above problems, this dissertation combines formalmethods and model checking technique to make a research on modeling and formalverification technique of complicated information system whose behavior has distributed,concurrent and real-time characteristics from the perspective of requirement analysis level,model design level and performance design level.
First, formal methods and model checking techniques have been reviewed in thisresearch. The behavior characteristics of complicated information system are illustrated andthe emphasis and difficulty of formal model and verification is analyzied. Then someproblems in this field and the future research are concluded.
Second, to validate the correctness of the requirements design of complicatedinformation system, this research divides the software requirements into top-level andtechnical-level requirements, and uses behavior-oriented abstract modeling approach to modeldomain policies as top-level requirements of system, and specifies the requirement modelwith RSL. To validate and refine the top-level requirements model, this dissertation translatesthe RSL specification of the top-level requirements model into a Promela model by definingthe transformation rules of syntax and semantics of RSL. The property specification oftop-level requirements model is encoded to temporal logic formula. Finally, using the modelchecker SPIN automatically verifies whether the top-level requirements model can satisfy thetemporal logic formula.
Third, to validate the correctness of technical-level requirements design, UML sequencediagrams are used to model the interactive scenes of complicated information system.Because UML sequence diagrams model lacks of accurate dynamic semantics, and can notautomatically validate the dynamic nature of the model, this dissertation defines operationalsemantics of transition system for UML sequence diagram and defines its transformation rulesfrom UML sequence diagram to promela model. The parse result of XML file of sequencediagrams is converted to promela program. At last, the promela program which describes thesystem requirements and linear temporal logic which describes the specification of system areused to be the input of model checker SPIN automatically validating the correctness oftechnical-level requirements design of systems.
Forth, to validate the correctness of design model of complicated information system,UML statecharts are used to be the major modeling tool. The middle representation of theUML statecharts which transform hierarchical statecharts to flat statecharts is given bydefining the major elements of UML statecharts with tuple. On the basis of middlerepresentation, the operational semantics of UML statecharts is defined, the transformationrules from complicated information system’s design model to NuSMV input model aredesigned. Based on this transformation rules and the parse result of XML file of UMLstatecharts, the automatic transformation process from design model to NuSMV input modelis realized. The correctness of the transformation process is illustrated by proving thebisimulation equivalence relation between the operational semantics of UML statecharts andNuSMV input model which is generated by transformation rules. Finally, the model checkerNuSMV is used to verify whether the design model of complicated information system cansatisfy the property specification.
Furthermore, this dissertation makes a research on fomal verification technique ofreal-time performance design of complicated information system. The task architecture whichdescribes the activating order of internal event and task when external event arrives is createdby UML collaboration diagram in the requirement process. Then the execution time budget ofconcurrent task is allocated by events order analysis method and the UML collaborationdiagram is extend to real-time collaboration diagram. Ultimately, the timed automata networkis established on the basis of real-time collaboration diagram, and is input into the modelchecker UPPAAL for automated verification.
In the end, the work of the dissertation is concluded and the further research direction isput forward
引文
[1] Bjorkman, Colonel Eileen A., Zeis Jr., Colonel Joseph E..Testing2020: Evaluatingweapons systems and capabilities in a joint environment. U.S. Air Force T and E Days,2007(Test and Evaluation), Destin, FL, United states,2007,2:18-24P.
[2] Watanabe K., Uesugi M., Komatsu M.. Verification and analysis for small signalstability of Electric Power Systems for the international space station/JEM.31stInternational Conference on Telecommunications Energy,2009,12:1-6P.
[3] Cheon S.W., Park G.Y., et al. The software V&V tasks for a safety-critical softwarebased protection system in nuclear power plants. IEEE International Conference onIndustrial Technology (ICIT2005), Hong Kong,2005,12:305-307P.
[4]孙志安,裴晓黎等.软件可靠性工程.北京:北京航空航天大学出版社,2009.3,1-2页.
[5] Christel Baier, Joost-Pieter Katoen, Kim Guldstrand Larsen. Principles of ModelChecking. The MIT Press. May31,2008,2-3P.
[6] E.M.Clarke,O.Grumberg, D.A. Peled. Model Checking. Cambridge, MA: MIT Press.1999,3-5P.
[7] J. R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge UniversityPress,1996,3-4P.
[8] C. Hoare, H. Jifeng. Unifying Theories of Programming. Prentice Hall, Europe,1998,10-12P.
[9]翟健,杨秋松,肖俊超,李明树.一种形式化的组件化软件过程建模方法.软件学报,2011,22(01):1-16页.
[10] C.A.R Hoare. An axiomatic basis for computer programming. Communications of theACM,1969,12(10):576-580P.
[11] Edmund Clarke, Bernd-Holger Schlingloff. Model checking. Handbook of AutomatedReasoning. Edited by Alan Robinson and Andrei Voronkov, Boston: MIT Press,2001,1635-1790P.
[12] E. Dijikstra, C. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag,1990.6-7P.
[13] Edmund M. C., Jeannette M. W. Foxmal methods: state of the art and future directions.ACM Computing Surveys,1996,28(4):626-643P.
[14] Peled D A. Software Reliability Methods. Springer-Verlag,2001,9-11P.
[15] OMG Unified Modeling Language Specification (Version1.5), Object ManagementGroup, Framingham, Massachusetts, March2003.
[16] UML2.0Specification, OMG, http://www.uml.org/#UML2.0.
[17]李留英,王戟,齐治昌. UML Statechart图的操作语义.软件学报,2001,12(12):1864-1873页.
[18]周颖,郑国梁,李宣东.面向模型检验的UML状态机语义.电子学报,2003,12A:2091-2095页.
[19]程亮,张阳.基于UML和模型检测的安全模型验证方法.计算机学报,2009,32(4):699-708页.
[20]王聪,王智学. UML活动图的操作语义.计算机研究与发展,2007,44(10):1801-1807页.
[21]朱雪阳.双重软件体系结构描述框架XYZ/ADL.计算机研究与发展,2007,44(9):1485-1494页.
[22]胡军,于笑丰,张岩,李宣东,郑国梁.基于场景构件式实时软件设计的一致性检查.软件学报,2006,17(1):48-58页.
[23]周立,陈湘萍,黄罡,孙艳春,梅宏.支持协商的网构软件体系结构行为建模与验证.软件学报,2008,19(5):1099-1112页.
[24] Erich Mikk, Michael Siegel, Gerard J Holzmann, et al. Implementing Statechart inPROMELA/Spin. Proceedings of the2nd IEEE Workshop on Industrial-StrengthFormal Specification Techniques IEEE Computer Society,1998,1(2):90–101P.
[25]董威,王戟,齐治昌. UML Statecharts的切片模型检验方法.电子学报,2002,30(12):2084-2089页.
[26]董威,王戟,齐治昌. UML Statecharts的模型检验方法.软件学报,2003,14(4):750-756页.
[27] George, C., Haxthausen, A., Hughes, S., Milne, R., Prehn, S. and Pedersen, J. TheRAISE Development Method. BCS Practitioner Series, Denmark, Prentice Hall,1995,1-3P.
[28] C. B. Jones. Systematic Software Development using VDM. In Prentice Hall,1990,1-4P.
[29] C.A.R. Hoare, Communication Sequential Processes. Communications of the ACM,1978,21(8):666-677P.
[30] J. Davies and J. Woodcock. Using Z: Specification, Refinement, and Proof. In PrenticeHall,1996,3-5P.
[31] R. Milner.Communication and Concurrency. New York: Prentice Hall,1989,1-3P.
[32]赖祥伟,张为群,邱玉辉,周彦晖.形式化的软件测试模型研究.计算机科学,2004,31(11):169-173页.
[33]孙猛,张乃孝, Bernhard K Aichernig等. UML状态机视图的RSL形式描述.北京大学学报（自然科学版）,2005,41(3):344-357页.
[34]顾翔,邱建林.基于CSP和RSL的协议形式化描述技术研究.微电子学与计算机,2009,26(3):93-96页.
[35]顾翔,邱建林,邵浩然等.基于RSL的协议形式化描述与验证方法.计算机工程,2009,35(23):41-43页.
[36]顾翔,邱建林.基于时态逻辑的协议RSL形式化描述.计算机工程,2011,37(5):7-9页.
[37] LI Li, HE Ji feng. A Denotational Semantics of Timed RSL Using Duration Calculus.Journal of Software,2001,12(6):802-815P.
[38] Mohammad Reza Nami, Abbas Malekpour. Formal Specification of a ParticularBanking Domain with RAISE Specification Language. IEEE Symposium onComputers and Communications, Marrakech Morocco,2008, Page(s):695–699P.
[39] Mar′a Virginia Mauco, Mar′a Carmen Leonardi, etc. Formalising a DerivationStrategy for Formal Specifications from Natural Language Requirements Models.2005IEEE International Symposium on Signal Processing and Information Technology.Athens Greece,2005, Page(s):646-651P.
[40] Narayan Debnath, Ana Funes, etc. Integrating OCL Expressions into RSLSpecifications.2007IEEE International Conference on Electro/InformationTechnology,2007, Page(s):158-162P.
[41] R.Alur, D.L.Dill. A Theory of Timed Automata. Theoretical Computer Seience.1994，126(2):183-235P.
[42]李广元,唐稚松.带有时钟变量的线性时序逻辑与实时系统验证.软件学报,2002,13(1):33-41页.
[43]晏荣杰,李广元,徐雨波等.有限精度时间自动机的可达性检测.软件学报,2006,17(1):1-10页.
[44] Eugene Asarin,Paul Caspi,Oded Maler et al.Timed Regular Expressions.Journal of theAssociation for Computing Machinery,2002,49(2):172-206P.
[45] Jerome Durand-Lose.A Kleene theorem for splitable signals Information ProcessingLetters,2004,89(5):237-245P.
[46] Catalin Dima.Regular Expressions with Timed Dominoes. Discrete Mathematics andTheoretical Computer Science.2003:141-154P.
[47]侯建民,李宣东,郑国梁等.离散时段演算的符号模型验证.计算机学报,1998,21(2):103-110页.
[48] Geist, S,Gromov, D,Raisch, J et al.Timed discrete event control of parallel productionlines with continuous outputs. Discrete event dynamic systems,2008,18(2):241-262P.
[49] Lanotte, Ruggero.Time and Probability-Based Information Flow Analysis.IEEETransactions on Software Engineering,2010,36(5):719-727P.
[50] Jeremy Sproston.Strict Divergence for Probabilistic Timed Automata.CONCUR2009-Concurrency Theory,2009. Page(s)::620-636P.
[51] Bohnenkamp, H.,D'Argenio, P.R.,Hermanns, H. et al. MODEST: A CompositionalModeling Formalism for Hard and Softly Timed Systems.IEEE Transactions onSoftware Engineering,2006,32(10):812-830P.
[52] P. Mateus,M. Morais,C. Nunes et al.Categorical foundations for randomly timedautomata.Theoretical Computer Science,2003,308(1/3):393-427P.
[53]陈伟,薛云志,赵琛等.一种基于时间自动机的实时系统测试方法.软件学报,2007,18(1):62-73页.
[54] Colvin, R,Grunske, L,Winter, K et al.Timed Behavior Trees for Failure Mode andEffects Analysis of time-critical systems.The Journal of Systems andSoftware,2008,81(12):2163-2182P.
[55] Fei Yan, Tao Tang. A formal modeling and verification approach for real-time system.7th World Congress on Intelligent Control and Automation, chongqing china,2008,Page(s):204-208P.
[56] Yigui Luo. Transform Dual Transition Timed Petri Net into Timed Automaton forModel Checking with UPPAAL.2010International Conference on ComputationalIntelligence and Software Engineering, Wuhan China,2010, Page(s):1-4P.
[57]许何,赵建华,李宣东等.自动验证并发实时系统的线性时段性质.计算机研究与发展,2001,38(9):1097-1104页.
[58]晏荣杰,李广元,徐雨波等.有限精度时间自动机的可达性检测.软件学报,2006,17(1):1-10页.
[59]张君华,黄志球,曹子宁等.模型检测基于概率时间自动机的反例产生研究.计算机研究与发展,2008,45(10):1638-1645页.
[60]徐亮.改进的以SMT为基础的实时系统限界模型检测.软件学报,2010,21(7):1491-1502页.
[61]黄锡滋.软件可靠性、安全性与质量保证.北京:电子工业出版社,2002.
[62] IEEE Standard Glossary, IEEE Std729-1983.
[63]马良荔,金松,刘杰生等.软件测试及关键技术探讨.舰船电子工程,2004,24(3):30-31,92页.
[64]顾庆,陈宗岳,陈道蓄等. E-CSPE约束的一致性判定.计算机学报,2003,26(11):1568-1574页.
[65]陆文,徐锋,吕建等.一种开放环境下的软件可靠性评估方法.计算机学报,2010,33(3):452-462页.
[66]杨芙清.面向对象软件回归测试技术研究.软件学报,2001,12(3):372-376页.
[67]兰毓华,毛法尧,曹化工等.基于Z规格说明的软件测试用例自动生成.计算机学报,1999,22(9):963-969页.
[68]孙昌爱,金茂忠,刘超等.程序执行时间的静态预估与可视化分析方法.软件学报,2003,14(1):68-75页.
[69]陈锦富,卢炎生,谢晓东等.软件错误注入测试技术研究.软件学报,2009,20(6):1425-1443页.
[70] Godefroid P, Klarlund N, Sen K. et al. DART: Directed automated random testing.SIGPLAN Notices,2005,40(6):213-223P.
[71] S.G.K. Murthy, K. Raja Sekharam. Software Reliability through Theorem Proving.Defence science journal,2009,59(3):205-214P.
[72] Ning ZHANG, Hong-bo LI. Affine bracket algebra theory and algorithms and theirapplications in mechanical theorem proving. Science in China. Series A, Mathematics,physics, astronomy,2007,50(7):941-950P.
[73] Geoff Sutcliffe.The4th IJCAR Automated Theorem Proving System Competition-CASC-J4.AI communications,2009,22(1):59-72P.
[74] A. Church. A note on the Entscheidungsproblem. The Journal of Symbolic Logic,1936,1(1):40-41P.
[75] A. M. Turing. On computable numbers, with an application to theEntscheidungsproblem. Procedings of the London Mathematical Society,1936,42:230-265.
[76]陈钢,宋晓宇,顾明等. COQ定理证明器辅助PLC程序验证和分析.北京大学学报(自然科学版),2010,46(1):30-34页.
[77]舒新峰,段振华.有穷时间投影时序逻辑的完备公理系统.软件学报,2011,22(3):366-380页.
[78] Medina-Bulo I, Palomo-Lozano F, Ruiz-Reina JL. A verified COMMON LISPimplementation of Buchberger's algorithm in ACL2. Journal of Symbolic Computation,2010,45(1):96-123P.
[79] Umeno S, Lynch N. Proving safety properties of an aircraft landing protocol using I/Oautomata and the PVS theorem prover: A case study. Fm2006: Formal Methods,Proceedings,2006, Page(s):64-80P.
[80] Choi BD, Lee Y, Choi DL. Geo(x1), Geo(x2)/D/c HOL priority queueing system withrandom order selection within each priority class. Probability in the Engineering andInformational Sciences,1998,12(1):125-139P.
[81] Clarke E, Emerson E. Design and Synthesis of Synchronization Skeletons UsingBranching-Time Temporal Logic. In Proceedings of the Workshop on Logic ofPrograms, LNCS, Springer-Verlag,1981,131:52-71P.
[82] Queille P, Sifakia J. Specification and verification of concurrent systems in CESAR. InInternational Symposium on Programming, LNCS, Springer-Verlag,1982,137:337-351P.
[83] A. Pnueli. The temporal logic of programs. In18th IEEE Symposium on Foundationsof Computer Science (FOCS), IEEE Computer Society Press,1977, Page(s):46-67P.
[84]林惠民,张文辉.模型检测:理论、方法与应用.电子学报,2002,30(z1):1907-1912页.
[85]梁爱丽,朱嘉奇,王捍贫等.一种新的时段演算及其验证.计算机研究与发展,2008,45(z1):169-174页.
[86]刘万伟,王戟,王昭飞等. ETL的符号化模型检验.软件学报,2009,20(8):2015-2025页.
[87] Cindy Eisner, Doron Peled. Comparing symbolic and explicit model checking of asoftware system. In Proceedings of the9th International SPIN Workshop on ModelChecking of Software.2002, Page(s):230-239P.
[88] McMillan L. Symbolic model checking [Ph.D. Thesis]. Carnegie Mellon University,1992
[89] J.R Burch, Edmund M.Clarke, K.L McMillan, D.L. Dill, L.J. Hwang. Symbolicmodelchecking:1020states and beyond. In Proceedings of the5th Annual IEEESymposium Logic in Computer Science.1990, Page(s):428-439P.
[90] M. Musuvathi, D. Engler. Model checking large network protocol implementation.InProceedings of the1st Symposium on Networked Systems Design andImplementation, USENIX Association.2004, Page(s):155-168P.
[91] Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice-HallEnglewood Cliffs, New Jersey.1991.
[92] C. Courcoubets, M.P. Wolper, M. Yannakakis. Memory-efficient algorithms for theverification of temporal properties. Formal Methods in System Design.1992,Page(s):275-288P.
[93] S Katz, D Peled. Verification of distributed programs using representative interleavingsequences. Distributed Computing.1992, Page(s):107-120P.
[94] Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, and Sriram K.Rajamani. Partial-order reduction in symbolic state-space exploration. FormalMethodsin System Design.2001, Page(s):97-116P.
[95]骆翔宇,苏开乐,杨晋吉等.有界模型检测同步多智体系统的时态认知逻辑.软件学报,2006,17(12):2485-2498页。
[96]杨晋吉,苏开乐,骆翔宇等.有界模型检测的优化.软件学报,2009,20(8):2005-2014页.
[97] Jiff Barnat,Lubos Brim,Jakub Chaloupka et al.Parallel Breadth-First Search LTLModel-Checking.18th IEEE International Conference on Automated SoftwareEngineering (ASE2003).2003:106-115P.
[98] M. Bourahla.Distributed CTL model checking.IEE Proceedings. Part L, Software,2005,152(6):297-308P.
[99] E. Allen Emersion, A. Prasad Sistla. Symmetry and model checking. Formal Methodsin System Design.1996, Page(s):105-131P.
[100] A. Prasad Siatla, viktor Gyuris, E. Allen Emerson. Smc: a synunetry-based modelchecker for verification of safety and liveness properties. ACM Transaction onSoftware Engineering Methodology.2000, Page(s):133-166P.
[101] Edmund M. Clarke, O David E. Long. Model checking and abstraction. ACMTransaction on Programming Languages and Systems:1994, Page(s):1512-1542P.
[102] Karsten Stahl, Kai Baukus, Yassine Lakhnech, Martin Steffen. Divide, abstract, andmodel-check. In SPIN.1999, Page(s):57-76P.
[103] Holzmann J. The model checker SPIN. IEEE Trans. on Software Engineering,1997,23(5):279295P.
[104] Holzmann J. Algorithms for Automated Protocol Verification. Prentice Hall, NewJersey,1991.
[105]徐蔚文,陆鑫达.身份认证协议的模型检测分析.计算机学报,2003,26(2):195-201页.
[106]邵晨曦,胡香冬,熊焰等.密码协议的SPIN建模和验证.电子学报,2002,30(z1):2099-2101页.
[107] NUSMV: a new symbolic model checker [EB/OL]. http://nusmv.irst.itc.it/NuSMV/papers/sttt.j/html/index.html.2007,.
[108] VITUS S., LAM W..A FORMALISM FOR REASONING ABOUT UML ACTIVITYDIAGRAMS[J].Nordic journal of computing,2007,14(1/2):43-64P.
[109]陈圣标,吴剑峰,张广泉等.基于NuSMV的Web服务失配限界模型检测.苏州大学学报,2011,27(1):32-38页.
[110] Marco Bozzano,Adolfo Villafiorita.The Fsap/nusmv-sa Safety Analysis Platform.International Journal on Software Tools for Technology Transfer,2007,9(1):5-24P.
[111] G. Behrmann, A. David, and K.G. Larsen.“A tutorial on uppaal,” Formal methods forthe design of real-time systems,2004, Page(s):200–236P.
[112] N.C.W.M. Braspenning,E.M. Bortnik,J.M. van de Mortel-Fronczak et al.Model-basedsystem analysis using Chi and Uppaal: An industrial case study.Computers inIndustry,2008,59(1):41-54P.
[113] Andre L. N. Muniz,Aline M. S. Andrade,George Lima et al.Integrating UML andUPPAAL for designing, specifying and verifying component-based real-timesystems.Innovations in Systems and Software Engineering,2010,6(1/2):29-37P.
[114] Rong Mei, Li Zhonghui, Zhang Guangquan et al. Model Checking ofNeedham-Schroeder Protocol Using UPPAAL.20106th International Conference onWireless Communications, Networking and Mobile Computing,2010, Page(s):1-4P.
[115]钱军,冯玉琳.系统动态行为语义模型及其形式描述.计算机研究与发展,1999,24(8):907-914页.
[116] Autili, M,Mostarda, L,Navarra, A et al.Synthesis of decentralized and concurrentadaptors for correctly assembling distributed component-based systems.The Journal ofSystems and Software,2008,81(12):2210-2236P.
[117] Dijkstra E W. Displine of programming. New Jersey:Prentice Hall,1976.
[118] Kozen D. Results on the propositionalmu-calculus. Theoretical Computer Science,1985,27(3):333-354P.
[119] Lamport L. The temporal logic of actions. ACM Transactions on ProgrammingLanguages and System s,1994,16(3):872-923P.
[120] BART JACOBS, FRANK PIESSENS, JAN SMANS et al. A Programming Model ForConcurrent Object-oriented Programs.ACM Transactions on Programming Languagesand Systems,2009,31(1):1-48P.
[121]刘刚.面向领域的软件需求一致性验证方法研究.哈尔滨工程大学博士学位论文,2008.
[122] WANG Qian-xiang, WU Qiong, LI Ke-qin, YANG Fu-qing. An Object-OrientedMethod for Domain Engineering. Journal of Software,2002,13(10):1977-1844P.
[123] Univan Ahn and Chris George. C++Translator for RAISE Specification Language.Technical Report220, UNU-IIST, P.O. Box3058, Macau, November2000.
[124] Friedrich Wilhelm Schr¨oer. The GENTLE Compiler Construction System. Metarga,Berlin,2005.http://www.gentle.compilertools.net/GENTLE97.pdf.
[125] Sutcliffer A. Scenario-Based Requirements Engineering. In: Proceedings of the11thIEEE International Requirements Engineering Conference. Los Alamitos: IEEEComputer Society Press,2003. Page(s):320-329P.
[126] K. Korenblat, C. Priami. Extraction of Pi-calculus specifications from a UMLsequenceand state diagrams. Technical Report,2003.
[127] V.S.W. Lam, J. Padget. Consistency checking of sequence diagrams and statechartdiagrams using the pi-Calculus. In Proceedings of IFM2005, LNCS3771, BerlinHeidelberg: Springer-Verlag,2005.
[128]赵也非.动态UML子图的形式语义研究.华东师范大学博士学位论文,2010.
[129]陈栋. UML交互图的模型验证方法研究.华东师范大学硕士学位论文,2009.
[130]王璐珍.UML顺序图的自动分析技术研究.国防科学技术大学硕士学位论文,2002.
[131]张岩,胡军,于笑丰等.场景驱动的构件行为抽取.软件学报,2007,18(1):50-61页.
[132] Gomaa H著,吕庆中等译.用UML设计并发、分布式、实时应用.北京:北京航空航天大学出版社,2004,450-460页.
[133]顾兵主编. XML实用技术教程.北京:清华大学出版社,2007.
[134] Timothy J.Grose, Gary C. Noney, Stephen A. Brodsky.徐强,金艳红等译.精通XMI----使用XMI, XML和UML进行Java编程.北京:电子工业出版社,2004.
[135] Poseidon-for-UML. http://www.gentleware.com/.
[136] William Chan, Richard J Anderson, Paul Beame, et al. Model checking large softwarespecifications. IEEE Transactions on Software Engineering,1998,24(7):34-48P.
[137] E. M. Clarke, W. Heinle. Modular translation of statecharts to SMV. Technical ReportCMU-CS-00-XXX Carnegie-Mellon University School of Computer Science,2000,12(1):102-120P.
[138] T. Firley, M. Huhn, K. Diethers, T. Gehrke, and U. Goltz. Timed sequence diagramsand tool-based analysis: a case study. Proceedings of the2nd international conferenceon The unified modeling language: beyond the standard,1999, pp.645–660P.
[139] F. Yan and T. Tang,“A formal modeling and verification approach for real-timesystem,”7th World Congress on Intelligent Control and Automation,2008, Page(s):204–208P.
[140]赵丽芳.基于UPPAAL和UML的实时系统形式化分析与应用.苏州大学硕士学位论文,2008.
[141]崔康乐. UML时序图模型到UPPAAL时间自动机模型转换方法研究和工具实现.华东师范大学硕士学位论文,2010.
[2] Watanabe K., Uesugi M., Komatsu M.. Verification and analysis for small signalstability of Electric Power Systems for the international space station/JEM.31stInternational Conference on Telecommunications Energy,2009,12:1-6P.
[3] Cheon S.W., Park G.Y., et al. The software V&V tasks for a safety-critical softwarebased protection system in nuclear power plants. IEEE International Conference onIndustrial Technology (ICIT2005), Hong Kong,2005,12:305-307P.
[4]孙志安,裴晓黎等.软件可靠性工程.北京:北京航空航天大学出版社,2009.3,1-2页.
[5] Christel Baier, Joost-Pieter Katoen, Kim Guldstrand Larsen. Principles of ModelChecking. The MIT Press. May31,2008,2-3P.
[6] E.M.Clarke,O.Grumberg, D.A. Peled. Model Checking. Cambridge, MA: MIT Press.1999,3-5P.
[7] J. R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge UniversityPress,1996,3-4P.
[8] C. Hoare, H. Jifeng. Unifying Theories of Programming. Prentice Hall, Europe,1998,10-12P.
[9]翟健,杨秋松,肖俊超,李明树.一种形式化的组件化软件过程建模方法.软件学报,2011,22(01):1-16页.
[10] C.A.R Hoare. An axiomatic basis for computer programming. Communications of theACM,1969,12(10):576-580P.
[11] Edmund Clarke, Bernd-Holger Schlingloff. Model checking. Handbook of AutomatedReasoning. Edited by Alan Robinson and Andrei Voronkov, Boston: MIT Press,2001,1635-1790P.
[12] E. Dijikstra, C. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag,1990.6-7P.
[13] Edmund M. C., Jeannette M. W. Foxmal methods: state of the art and future directions.ACM Computing Surveys,1996,28(4):626-643P.
[14] Peled D A. Software Reliability Methods. Springer-Verlag,2001,9-11P.
[15] OMG Unified Modeling Language Specification (Version1.5), Object ManagementGroup, Framingham, Massachusetts, March2003.
[16] UML2.0Specification, OMG, http://www.uml.org/#UML2.0.
[17]李留英,王戟,齐治昌. UML Statechart图的操作语义.软件学报,2001,12(12):1864-1873页.
[18]周颖,郑国梁,李宣东.面向模型检验的UML状态机语义.电子学报,2003,12A:2091-2095页.
[19]程亮,张阳.基于UML和模型检测的安全模型验证方法.计算机学报,2009,32(4):699-708页.
[20]王聪,王智学. UML活动图的操作语义.计算机研究与发展,2007,44(10):1801-1807页.
[21]朱雪阳.双重软件体系结构描述框架XYZ/ADL.计算机研究与发展,2007,44(9):1485-1494页.
[22]胡军,于笑丰,张岩,李宣东,郑国梁.基于场景构件式实时软件设计的一致性检查.软件学报,2006,17(1):48-58页.
[23]周立,陈湘萍,黄罡,孙艳春,梅宏.支持协商的网构软件体系结构行为建模与验证.软件学报,2008,19(5):1099-1112页.
[24] Erich Mikk, Michael Siegel, Gerard J Holzmann, et al. Implementing Statechart inPROMELA/Spin. Proceedings of the2nd IEEE Workshop on Industrial-StrengthFormal Specification Techniques IEEE Computer Society,1998,1(2):90–101P.
[25]董威,王戟,齐治昌. UML Statecharts的切片模型检验方法.电子学报,2002,30(12):2084-2089页.
[26]董威,王戟,齐治昌. UML Statecharts的模型检验方法.软件学报,2003,14(4):750-756页.
[27] George, C., Haxthausen, A., Hughes, S., Milne, R., Prehn, S. and Pedersen, J. TheRAISE Development Method. BCS Practitioner Series, Denmark, Prentice Hall,1995,1-3P.
[28] C. B. Jones. Systematic Software Development using VDM. In Prentice Hall,1990,1-4P.
[29] C.A.R. Hoare, Communication Sequential Processes. Communications of the ACM,1978,21(8):666-677P.
[30] J. Davies and J. Woodcock. Using Z: Specification, Refinement, and Proof. In PrenticeHall,1996,3-5P.
[31] R. Milner.Communication and Concurrency. New York: Prentice Hall,1989,1-3P.
[32]赖祥伟,张为群,邱玉辉,周彦晖.形式化的软件测试模型研究.计算机科学,2004,31(11):169-173页.
[33]孙猛,张乃孝, Bernhard K Aichernig等. UML状态机视图的RSL形式描述.北京大学学报（自然科学版）,2005,41(3):344-357页.
[34]顾翔,邱建林.基于CSP和RSL的协议形式化描述技术研究.微电子学与计算机,2009,26(3):93-96页.
[35]顾翔,邱建林,邵浩然等.基于RSL的协议形式化描述与验证方法.计算机工程,2009,35(23):41-43页.
[36]顾翔,邱建林.基于时态逻辑的协议RSL形式化描述.计算机工程,2011,37(5):7-9页.
[37] LI Li, HE Ji feng. A Denotational Semantics of Timed RSL Using Duration Calculus.Journal of Software,2001,12(6):802-815P.
[38] Mohammad Reza Nami, Abbas Malekpour. Formal Specification of a ParticularBanking Domain with RAISE Specification Language. IEEE Symposium onComputers and Communications, Marrakech Morocco,2008, Page(s):695–699P.
[39] Mar′a Virginia Mauco, Mar′a Carmen Leonardi, etc. Formalising a DerivationStrategy for Formal Specifications from Natural Language Requirements Models.2005IEEE International Symposium on Signal Processing and Information Technology.Athens Greece,2005, Page(s):646-651P.
[40] Narayan Debnath, Ana Funes, etc. Integrating OCL Expressions into RSLSpecifications.2007IEEE International Conference on Electro/InformationTechnology,2007, Page(s):158-162P.
[41] R.Alur, D.L.Dill. A Theory of Timed Automata. Theoretical Computer Seience.1994，126(2):183-235P.
[42]李广元,唐稚松.带有时钟变量的线性时序逻辑与实时系统验证.软件学报,2002,13(1):33-41页.
[43]晏荣杰,李广元,徐雨波等.有限精度时间自动机的可达性检测.软件学报,2006,17(1):1-10页.
[44] Eugene Asarin,Paul Caspi,Oded Maler et al.Timed Regular Expressions.Journal of theAssociation for Computing Machinery,2002,49(2):172-206P.
[45] Jerome Durand-Lose.A Kleene theorem for splitable signals Information ProcessingLetters,2004,89(5):237-245P.
[46] Catalin Dima.Regular Expressions with Timed Dominoes. Discrete Mathematics andTheoretical Computer Science.2003:141-154P.
[47]侯建民,李宣东,郑国梁等.离散时段演算的符号模型验证.计算机学报,1998,21(2):103-110页.
[48] Geist, S,Gromov, D,Raisch, J et al.Timed discrete event control of parallel productionlines with continuous outputs. Discrete event dynamic systems,2008,18(2):241-262P.
[49] Lanotte, Ruggero.Time and Probability-Based Information Flow Analysis.IEEETransactions on Software Engineering,2010,36(5):719-727P.
[50] Jeremy Sproston.Strict Divergence for Probabilistic Timed Automata.CONCUR2009-Concurrency Theory,2009. Page(s)::620-636P.
[51] Bohnenkamp, H.,D'Argenio, P.R.,Hermanns, H. et al. MODEST: A CompositionalModeling Formalism for Hard and Softly Timed Systems.IEEE Transactions onSoftware Engineering,2006,32(10):812-830P.
[52] P. Mateus,M. Morais,C. Nunes et al.Categorical foundations for randomly timedautomata.Theoretical Computer Science,2003,308(1/3):393-427P.
[53]陈伟,薛云志,赵琛等.一种基于时间自动机的实时系统测试方法.软件学报,2007,18(1):62-73页.
[54] Colvin, R,Grunske, L,Winter, K et al.Timed Behavior Trees for Failure Mode andEffects Analysis of time-critical systems.The Journal of Systems andSoftware,2008,81(12):2163-2182P.
[55] Fei Yan, Tao Tang. A formal modeling and verification approach for real-time system.7th World Congress on Intelligent Control and Automation, chongqing china,2008,Page(s):204-208P.
[56] Yigui Luo. Transform Dual Transition Timed Petri Net into Timed Automaton forModel Checking with UPPAAL.2010International Conference on ComputationalIntelligence and Software Engineering, Wuhan China,2010, Page(s):1-4P.
[57]许何,赵建华,李宣东等.自动验证并发实时系统的线性时段性质.计算机研究与发展,2001,38(9):1097-1104页.
[58]晏荣杰,李广元,徐雨波等.有限精度时间自动机的可达性检测.软件学报,2006,17(1):1-10页.
[59]张君华,黄志球,曹子宁等.模型检测基于概率时间自动机的反例产生研究.计算机研究与发展,2008,45(10):1638-1645页.
[60]徐亮.改进的以SMT为基础的实时系统限界模型检测.软件学报,2010,21(7):1491-1502页.
[61]黄锡滋.软件可靠性、安全性与质量保证.北京:电子工业出版社,2002.
[62] IEEE Standard Glossary, IEEE Std729-1983.
[63]马良荔,金松,刘杰生等.软件测试及关键技术探讨.舰船电子工程,2004,24(3):30-31,92页.
[64]顾庆,陈宗岳,陈道蓄等. E-CSPE约束的一致性判定.计算机学报,2003,26(11):1568-1574页.
[65]陆文,徐锋,吕建等.一种开放环境下的软件可靠性评估方法.计算机学报,2010,33(3):452-462页.
[66]杨芙清.面向对象软件回归测试技术研究.软件学报,2001,12(3):372-376页.
[67]兰毓华,毛法尧,曹化工等.基于Z规格说明的软件测试用例自动生成.计算机学报,1999,22(9):963-969页.
[68]孙昌爱,金茂忠,刘超等.程序执行时间的静态预估与可视化分析方法.软件学报,2003,14(1):68-75页.
[69]陈锦富,卢炎生,谢晓东等.软件错误注入测试技术研究.软件学报,2009,20(6):1425-1443页.
[70] Godefroid P, Klarlund N, Sen K. et al. DART: Directed automated random testing.SIGPLAN Notices,2005,40(6):213-223P.
[71] S.G.K. Murthy, K. Raja Sekharam. Software Reliability through Theorem Proving.Defence science journal,2009,59(3):205-214P.
[72] Ning ZHANG, Hong-bo LI. Affine bracket algebra theory and algorithms and theirapplications in mechanical theorem proving. Science in China. Series A, Mathematics,physics, astronomy,2007,50(7):941-950P.
[73] Geoff Sutcliffe.The4th IJCAR Automated Theorem Proving System Competition-CASC-J4.AI communications,2009,22(1):59-72P.
[74] A. Church. A note on the Entscheidungsproblem. The Journal of Symbolic Logic,1936,1(1):40-41P.
[75] A. M. Turing. On computable numbers, with an application to theEntscheidungsproblem. Procedings of the London Mathematical Society,1936,42:230-265.
[76]陈钢,宋晓宇,顾明等. COQ定理证明器辅助PLC程序验证和分析.北京大学学报(自然科学版),2010,46(1):30-34页.
[77]舒新峰,段振华.有穷时间投影时序逻辑的完备公理系统.软件学报,2011,22(3):366-380页.
[78] Medina-Bulo I, Palomo-Lozano F, Ruiz-Reina JL. A verified COMMON LISPimplementation of Buchberger's algorithm in ACL2. Journal of Symbolic Computation,2010,45(1):96-123P.
[79] Umeno S, Lynch N. Proving safety properties of an aircraft landing protocol using I/Oautomata and the PVS theorem prover: A case study. Fm2006: Formal Methods,Proceedings,2006, Page(s):64-80P.
[80] Choi BD, Lee Y, Choi DL. Geo(x1), Geo(x2)/D/c HOL priority queueing system withrandom order selection within each priority class. Probability in the Engineering andInformational Sciences,1998,12(1):125-139P.
[81] Clarke E, Emerson E. Design and Synthesis of Synchronization Skeletons UsingBranching-Time Temporal Logic. In Proceedings of the Workshop on Logic ofPrograms, LNCS, Springer-Verlag,1981,131:52-71P.
[82] Queille P, Sifakia J. Specification and verification of concurrent systems in CESAR. InInternational Symposium on Programming, LNCS, Springer-Verlag,1982,137:337-351P.
[83] A. Pnueli. The temporal logic of programs. In18th IEEE Symposium on Foundationsof Computer Science (FOCS), IEEE Computer Society Press,1977, Page(s):46-67P.
[84]林惠民,张文辉.模型检测:理论、方法与应用.电子学报,2002,30(z1):1907-1912页.
[85]梁爱丽,朱嘉奇,王捍贫等.一种新的时段演算及其验证.计算机研究与发展,2008,45(z1):169-174页.
[86]刘万伟,王戟,王昭飞等. ETL的符号化模型检验.软件学报,2009,20(8):2015-2025页.
[87] Cindy Eisner, Doron Peled. Comparing symbolic and explicit model checking of asoftware system. In Proceedings of the9th International SPIN Workshop on ModelChecking of Software.2002, Page(s):230-239P.
[88] McMillan L. Symbolic model checking [Ph.D. Thesis]. Carnegie Mellon University,1992
[89] J.R Burch, Edmund M.Clarke, K.L McMillan, D.L. Dill, L.J. Hwang. Symbolicmodelchecking:1020states and beyond. In Proceedings of the5th Annual IEEESymposium Logic in Computer Science.1990, Page(s):428-439P.
[90] M. Musuvathi, D. Engler. Model checking large network protocol implementation.InProceedings of the1st Symposium on Networked Systems Design andImplementation, USENIX Association.2004, Page(s):155-168P.
[91] Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice-HallEnglewood Cliffs, New Jersey.1991.
[92] C. Courcoubets, M.P. Wolper, M. Yannakakis. Memory-efficient algorithms for theverification of temporal properties. Formal Methods in System Design.1992,Page(s):275-288P.
[93] S Katz, D Peled. Verification of distributed programs using representative interleavingsequences. Distributed Computing.1992, Page(s):107-120P.
[94] Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, and Sriram K.Rajamani. Partial-order reduction in symbolic state-space exploration. FormalMethodsin System Design.2001, Page(s):97-116P.
[95]骆翔宇,苏开乐,杨晋吉等.有界模型检测同步多智体系统的时态认知逻辑.软件学报,2006,17(12):2485-2498页。
[96]杨晋吉,苏开乐,骆翔宇等.有界模型检测的优化.软件学报,2009,20(8):2005-2014页.
[97] Jiff Barnat,Lubos Brim,Jakub Chaloupka et al.Parallel Breadth-First Search LTLModel-Checking.18th IEEE International Conference on Automated SoftwareEngineering (ASE2003).2003:106-115P.
[98] M. Bourahla.Distributed CTL model checking.IEE Proceedings. Part L, Software,2005,152(6):297-308P.
[99] E. Allen Emersion, A. Prasad Sistla. Symmetry and model checking. Formal Methodsin System Design.1996, Page(s):105-131P.
[100] A. Prasad Siatla, viktor Gyuris, E. Allen Emerson. Smc: a synunetry-based modelchecker for verification of safety and liveness properties. ACM Transaction onSoftware Engineering Methodology.2000, Page(s):133-166P.
[101] Edmund M. Clarke, O David E. Long. Model checking and abstraction. ACMTransaction on Programming Languages and Systems:1994, Page(s):1512-1542P.
[102] Karsten Stahl, Kai Baukus, Yassine Lakhnech, Martin Steffen. Divide, abstract, andmodel-check. In SPIN.1999, Page(s):57-76P.
[103] Holzmann J. The model checker SPIN. IEEE Trans. on Software Engineering,1997,23(5):279295P.
[104] Holzmann J. Algorithms for Automated Protocol Verification. Prentice Hall, NewJersey,1991.
[105]徐蔚文,陆鑫达.身份认证协议的模型检测分析.计算机学报,2003,26(2):195-201页.
[106]邵晨曦,胡香冬,熊焰等.密码协议的SPIN建模和验证.电子学报,2002,30(z1):2099-2101页.
[107] NUSMV: a new symbolic model checker [EB/OL]. http://nusmv.irst.itc.it/NuSMV/papers/sttt.j/html/index.html.2007,.
[108] VITUS S., LAM W..A FORMALISM FOR REASONING ABOUT UML ACTIVITYDIAGRAMS[J].Nordic journal of computing,2007,14(1/2):43-64P.
[109]陈圣标,吴剑峰,张广泉等.基于NuSMV的Web服务失配限界模型检测.苏州大学学报,2011,27(1):32-38页.
[110] Marco Bozzano,Adolfo Villafiorita.The Fsap/nusmv-sa Safety Analysis Platform.International Journal on Software Tools for Technology Transfer,2007,9(1):5-24P.
[111] G. Behrmann, A. David, and K.G. Larsen.“A tutorial on uppaal,” Formal methods forthe design of real-time systems,2004, Page(s):200–236P.
[112] N.C.W.M. Braspenning,E.M. Bortnik,J.M. van de Mortel-Fronczak et al.Model-basedsystem analysis using Chi and Uppaal: An industrial case study.Computers inIndustry,2008,59(1):41-54P.
[113] Andre L. N. Muniz,Aline M. S. Andrade,George Lima et al.Integrating UML andUPPAAL for designing, specifying and verifying component-based real-timesystems.Innovations in Systems and Software Engineering,2010,6(1/2):29-37P.
[114] Rong Mei, Li Zhonghui, Zhang Guangquan et al. Model Checking ofNeedham-Schroeder Protocol Using UPPAAL.20106th International Conference onWireless Communications, Networking and Mobile Computing,2010, Page(s):1-4P.
[115]钱军,冯玉琳.系统动态行为语义模型及其形式描述.计算机研究与发展,1999,24(8):907-914页.
[116] Autili, M,Mostarda, L,Navarra, A et al.Synthesis of decentralized and concurrentadaptors for correctly assembling distributed component-based systems.The Journal ofSystems and Software,2008,81(12):2210-2236P.
[117] Dijkstra E W. Displine of programming. New Jersey:Prentice Hall,1976.
[118] Kozen D. Results on the propositionalmu-calculus. Theoretical Computer Science,1985,27(3):333-354P.
[119] Lamport L. The temporal logic of actions. ACM Transactions on ProgrammingLanguages and System s,1994,16(3):872-923P.
[120] BART JACOBS, FRANK PIESSENS, JAN SMANS et al. A Programming Model ForConcurrent Object-oriented Programs.ACM Transactions on Programming Languagesand Systems,2009,31(1):1-48P.
[121]刘刚.面向领域的软件需求一致性验证方法研究.哈尔滨工程大学博士学位论文,2008.
[122] WANG Qian-xiang, WU Qiong, LI Ke-qin, YANG Fu-qing. An Object-OrientedMethod for Domain Engineering. Journal of Software,2002,13(10):1977-1844P.
[123] Univan Ahn and Chris George. C++Translator for RAISE Specification Language.Technical Report220, UNU-IIST, P.O. Box3058, Macau, November2000.
[124] Friedrich Wilhelm Schr¨oer. The GENTLE Compiler Construction System. Metarga,Berlin,2005.http://www.gentle.compilertools.net/GENTLE97.pdf.
[125] Sutcliffer A. Scenario-Based Requirements Engineering. In: Proceedings of the11thIEEE International Requirements Engineering Conference. Los Alamitos: IEEEComputer Society Press,2003. Page(s):320-329P.
[126] K. Korenblat, C. Priami. Extraction of Pi-calculus specifications from a UMLsequenceand state diagrams. Technical Report,2003.
[127] V.S.W. Lam, J. Padget. Consistency checking of sequence diagrams and statechartdiagrams using the pi-Calculus. In Proceedings of IFM2005, LNCS3771, BerlinHeidelberg: Springer-Verlag,2005.
[128]赵也非.动态UML子图的形式语义研究.华东师范大学博士学位论文,2010.
[129]陈栋. UML交互图的模型验证方法研究.华东师范大学硕士学位论文,2009.
[130]王璐珍.UML顺序图的自动分析技术研究.国防科学技术大学硕士学位论文,2002.
[131]张岩,胡军,于笑丰等.场景驱动的构件行为抽取.软件学报,2007,18(1):50-61页.
[132] Gomaa H著,吕庆中等译.用UML设计并发、分布式、实时应用.北京:北京航空航天大学出版社,2004,450-460页.
[133]顾兵主编. XML实用技术教程.北京:清华大学出版社,2007.
[134] Timothy J.Grose, Gary C. Noney, Stephen A. Brodsky.徐强,金艳红等译.精通XMI----使用XMI, XML和UML进行Java编程.北京:电子工业出版社,2004.
[135] Poseidon-for-UML. http://www.gentleware.com/.
[136] William Chan, Richard J Anderson, Paul Beame, et al. Model checking large softwarespecifications. IEEE Transactions on Software Engineering,1998,24(7):34-48P.
[137] E. M. Clarke, W. Heinle. Modular translation of statecharts to SMV. Technical ReportCMU-CS-00-XXX Carnegie-Mellon University School of Computer Science,2000,12(1):102-120P.
[138] T. Firley, M. Huhn, K. Diethers, T. Gehrke, and U. Goltz. Timed sequence diagramsand tool-based analysis: a case study. Proceedings of the2nd international conferenceon The unified modeling language: beyond the standard,1999, pp.645–660P.
[139] F. Yan and T. Tang,“A formal modeling and verification approach for real-timesystem,”7th World Congress on Intelligent Control and Automation,2008, Page(s):204–208P.
[140]赵丽芳.基于UPPAAL和UML的实时系统形式化分析与应用.苏州大学硕士学位论文,2008.
[141]崔康乐. UML时序图模型到UPPAAL时间自动机模型转换方法研究和工具实现.华东师范大学硕士学位论文,2010.