System Validation and Verification Using SDL Ron Henry Class Project Report ENSE 623 December 5, 2004i 12/7/04 6:19 PM Table of Contents 1 Introduction..........................................................................................................................1-1 1.1 Abstract........................................................................................................................1-1 1.2 Organization.................................................................................................................1-1 1.3 Terminology.................................................................................................................1-1 1.4 Motivation....................................................................................................................1-2 2 Conceptual Framework........................................................................................................2-1 2.1 Formal Methods...........................................................................................................2-1 2.2 Logic-Based V&V Approaches...................................................................................2-1 2.3 Standard Notations for Formal Modeling....................................................................2-3 2.3.1 Specification and Description Language (SDL)..................................................2-3 2.3.2 Message Sequence Charts (MSCs)......................................................................2-5 2.3.3 Test and Test Control Notation (TTCN)..............................................................2-6 2.4 SDL Tools....................................................................................................................2-6 2.5 Proposed Methodology................................................................................................2-7 3 Project Formulation .............................................................................................................3-1 3.1 Remote Astronomy Case Study...................................................................................3-1 3.2 Tau/SDL Configuration ...............................................................................................3-1 4 System Definition ................................................................................................................4-1 4.1 System Context............................................................................................................4-1 4.2 Use Case Definitions....................................................................................................4-1 4.3 Domain Model .............................................................................................................4-6 4.4 SDL Architecture.........................................................................................................4-8 4.5 SDL Process-Level Design........................................................................................4-20 4.6 Bugs and Limitations.................................................................................................4-42 5 Validation and Verification Using Executable Model.........................................................5-1 5.1 System Simulation .......................................................................................................5-1 5.2 Architecture Validation................................................................................................5-3 5.3 Test Case Generation.................................................................................................5-11 6 Future Work.........................................................................................................................6-1 Appendix A. Execution Trace for Observe Simulation........................................................A-1 Appendix B. Observatory TTCN Test Suite ........................................................................ B-1 7 References and Web Resources...........................................................................................7-1ii 12/7/04 6:19 PM List of Figures Figure 2-1: Automated V&V Methodology ................................................................................2-7 Figure 4-1: Observatory System Context ....................................................................................4-1 Figure 4-2: TurnOnInstrument.....................................................................................................4-2 Figure 4-3: TurnOffInstrument....................................................................................................4-3 Figure 4-4: Observe .....................................................................................................................4-4 Figure 4-5: Observatory Class Diagram ......................................................................................4-7 Figure 4-6: Observatory (Level 1).............................................................................................4-10 Figure 4-7: SupportModule (Level 2).......................................................................................4-11 Figure 4-8: TelescopeBlock (Level 2).......................................................................................4-12 Figure 4-9: InstrumentModule (Level 2)...................................................................................4-13 Figure 4-10: InstrumentManager (Level 3) ...............................................................................4-16 Figure 4-11: GuiderBlock (Level 3) ..........................................................................................4-16 Figure 4-12: CAM1 (Level 3)....................................................................................................4-20 Figure 4-13: DataRecorder ........................................................................................................4-21 Figure 4-14: AttitudeControl .....................................................................................................4-22 Figure 4-15: OpticalAssembly...................................................................................................4-23 Figure 4-16: Guider....................................................................................................................4-26 Figure 4-17: