【作者】 张涛；

【导师】 黄少滨；

【作者基本信息】 哈尔滨工程大学 ， 计算机应用技术， 2012， 博士

【摘要】 软件的质量和可靠性问题由来己久。目前，虽然软件分析、设计和测试技术仍是保障软件可靠性的主要手段，但是由于人们对软件系统分布式处理，并发处理，实时处理等能力要求的日益增强，使软件系统正日益趋向高度的复杂化，导致上述方法仍然不能完全满足开发高可靠软件系统的需要。模型检测作为一种形式化验证技术因其严格的数学基础、全自动的验证过程，以及早期在硬件系统和协议验证中的成功应用而倍受学术界和产业界的关注。但是在软件工程各阶段中结合模型检测，全面、自动的分析和验证复杂信息系统的需求、设计及性能模型、提高软件的安全性和可靠性尚处于探索阶段。针对上述问题，论文在软件工程中结合形式化方法与模型检测技术，分别从需求分析层面、模型设计层面以及性能设计层面研究具有分布式、并发和实时行为特性的复杂信息系统形式化建模及验证技术：首先，对形式化方法及模型检测技术的相关研究进行了综述，阐述了复杂信息系统的行为特征，分析了复杂信息系统形式化建模及验证工作的重点与难点，总结了该领域存在的问题以及未来的研究方向。其次，为验证复杂信息系统需求模型设计的正确性，将复杂信息系统的软件需求划分为顶层需求和技术层面需求，使用面向行为的抽象方法将领域政策建模为系统的顶层需求模型，并用RSL对其进行形式化规约。为验证及细化顶层需求模型，本文通过定义RSL语法及语义的转换规则将顶层需求模型的RSL规约转换为Promela模型，将顶层需求的性质规约描述为时态逻辑公式，最后使用模型检测器SPIN自动验证顶层需求模型对性质规约的可满足性。再次，为验证复杂信息系统技术层面需求模型设计的正确性，首先用UML顺序图建模复杂信息系统的动态交互场景；针对UML顺序图模型缺乏精确的动态语义以及不能自动验证模型动态性质的问题，为UML顺序图定义迁移系统操作语义及其到Promela模型的转换规则，将顺序图模型的XMI描述文件的解析信息自动转换为Promela程序；最后，将建模系统需求的Promela程序和描述系统性质规约的线性时序逻辑公式作为模型检测器SPIN的输入，自动验证系统技术层面需求模型设计的正确性。第四，为验证复杂信息系统设计模型的正确性，以UML状态图为系统建模的主要工具，使用元组定义UML状态图的主要元素，从而给出一种状态图模型的中间表示形式将层次状态图转化为平面状态图；基于该中间表示形式定义状态图模型的操作语义，设计复杂信息系统设计模型到NuSMV输入模型的语义转换规则；基于转换规则以及设计模型的XMI文档解析信息实现设计模型到NuSMV输入模型的自动转换过程，并通过证明状态图的操作语义与转换得到的NuSMV输入模块的操作语义为互模拟等价关系证明转换过程的正确性；最后使用模型检测器NuSMV验证复杂信息系统设计模型对其性质规范的可满足性。最后，研究复杂信息系统实时性能设计的形式化验证技术，在需求分析过程中使用UML协作图建模系统的任务体系结构，描述当外部事件到达时系统内部事件和任务的激活顺序；用事件顺序分析方法为并发任务分配执行时间预算，将UML协作图扩展为实时协作图；基于实时协作图模型构建并发系统的时间自动机网络，并将其输入到模型检测工具UPPAAL执行自动验证。最后，总结论文工作，并提出了下一步的研究方向。更多还原

【Abstract】 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更多还原