高新技术企业认定管理办法解读(吉林科技厅)

1、 Contents1Introduction (11.1Model Checking (21.2Computer-Aided Verification of UML Models (31.3UML to SMV Model Checking Process (61.4Main Contribution (92Modeling Reactive Systems Using UML (112.1Requirements Analysis (122.1.1Three-floor Elevator System Problem Statement (122.1.2System Properties (

2、142.2Defining Object Structure using UML (152.2.1UML Class Diagram (152.2.2UML Object Model (212.2.3UML Constraints (232.3Defining Object Behavior using UML (252.3.1UML State Machine Semantics (252.3.2Example Scenarios of Elevator State Machine (302.3.3Inherited State Diagrams (332.3.4UML Operations

3、 (353Translating UML to SMV (393.1Translation Overview (403.2Translating the Elevator Example (433.2.1Translating the Button Class (433.2.2Translating the RequestBn Subclass (483.2.3Translating the External_Event Class (523.2.4Translating Timer Class (553.2.5Translating Door Class (583.2.6Translatin

4、g the Elevator Class (603.2.7Putting it all together:Main SMV Module (653.3Translation Summary (664Verifying System Properties Using SMV (684.1CTL Overview (684.2Verifying the Elevator System Properties (704.2.1Safety Property for Elevator (704.2.2Liveness Properties for Elevator and Hall Buttons (7

5、04.2.3Additional System Properties (724.3Model Checking Partial Specifications (745Effectiveness of Model Checking (775.1Time Spent per Activity (785.2Requirements-level Errors (815.3UML Model Style Defects (845.4Object-oriented Modeling Errors (865.5SMV Errors (885.6Summary (906Conclusions and Futu

6、re Work (92Appendix A:UML Notation Summary (94A1.UML Class Diagram Notation (94A2.UML State Diagram Notation (97Appendix B:Elevator UML Specification (99Appendix C:Elevator SMV Program (107Appendix D.Additional Elevator Features (121References (122List of FiguresFigure1:Finite state model checking (

7、2Figure2:UML to SMV model checking process (7Figure3:Two-passenger scenario sequence diagram (13Figure4:Three-floor elevator main class diagram in UML (16Figure5:Three-floor elevator object model in UML (22Figure6:System properties shown as UML constraints (23Figure7:Elevator state diagram (26Figure

8、8:Door state diagram (28Figure9:Button state diagram and RequestBn state diagram (30Figure10:SMV module program structure (41Figure11:Button SMV module (44Figure12:RequestBn SMV module (49Figure13:External_Event SMV module (52Figure14:Timer state diagram (55Figure15:SET Event SMV module (56Figure16:

9、Partial listing of Timer SMV module (57Figure17:Partial listing of Door SMV module (58Figure18:Partial listing of Elevator SMV module (62Figure19:Partial listing of main SMV module (65Figure20:Main SMV module for Timer class unit verification (75List of TablesTable1:getNextDest operation modeled as

10、a decision table (36Table2:Macros for going to floor1with direction up (37Table3:SMV program structure/rules mapping (66Table4:Naming convention for SMV modules,variables and macros (67Table5:Requirements-level and OO modeling defects summary (801IntroductionObject oriented(OOmodeling started in the

11、 late1980s,modeling the concepts of object oriented programming at a higher level of abstraction.Several OO methodologists,spearheaded by G. Booch,J.Rumbaugh,and I.Jacobson,joined efforts to combine the best practices of various OO modeling approaches into a single method called the Unified Modeling

12、 Language(UML UML99.On November17,1997,the Object Management Group(OMGadopted the UML as a standard for specifying,visualizing,constructing and documenting artifacts of software systems. Since then,UML has gained popularity for providing software practitioners with a set of standard symbols and sema

13、ntics to effectively communicate and produce predictable,repeatable results. The popularity of UML is evidenced in the number of books,conferences,seminars,reports, papers and software tools available in the commercial market today.UML has become the most popular method for OO modeling.Most UML spec

14、ifications are descriptive and easy to understand.However,UML does not provide a standard approach to verify correctness properties of the model.In this thesis,we translate UML object-oriented software models to Symbolic Model Verifier(SMVMcMi93models in order to verify the correctness of the UML mo

15、del.UML has a very rich set of diagrams,notations and well-formedness rules.However,it does not provide guidelines for writing clear and unambiguous object-oriented specifications that are amenable to model checking.In this thesis,we demonstrate that the use of Class Diagram,Object Model and State D

16、iagrams are sufficient to translate into SMV for model checking.We introduce a set of guidelines in constructing well-formed unambiguous UML specifications that makes translation to SMV easy.We use UML constraints to describe the system properties informally. We provide a set of rules to translate t

17、he UML specifications including the UML constraints to SMV.We apply these guidelines to build a UML model for a three-floor elevator and apply these rules to translate the UML model to SMV.To complete the case study,we use SMV to perform model checking automatically.Our aim is to make systematic model checking available for software developers who use UML to