Systems Engineering Project: System Validation and Verification Using SDLFormalisms for Automated V&VCharacteristics of SDLCommercial Tools for SDL-Based V&VGeneral MethodologyRemote Observing Platform: System ContextRemote Observing Platform: Domain ModelMSC TurnOnInstrumentMSC TurnOffInstrumentMSC ObserveTau/SDL Model StructureObservatory System DiagramInstrumentModule Block DiagramCAM1 Block DiagramShutter Process DiagramCameraManager Process DiagramInheritance in SDL: HomingCameraManagerTau/SDL Simulator User InterfaceMSC Observe: Process-Level Simulator TraceTau/SDL Validator User InterfaceTau/SDL Validator Report SummaryTau/SDL Validator Trace: Implicit Signal ConsumptionModel Validation: MSC TurnOnInstrumentModel Validation: MSC ObserveMSC-Based Testing: TTCN StructureTest Case Generated from Observe MSCV&V with SDL: Project SummarySystems Engineering Project:System Validation and VerificationUsing SDLRon HenryENSE 623November 30, 20042Formalisms for Automated V&VSeveral standard notations have evolved in support of automated validation and verification:–Specification and Description Language (SDL)–Message Sequence Charts (MSC)–Test and Test Control Notation (TTCN)These formalisms are considered complementary–MSCs (familiar from UML sequence diagrams) are used both to specify requirements and to trace execution–SDL is used to specify the system architecture and state-machine model–TTCN is an abstract representation for test cases3 Characteristics of SDLMajor language features–Formal, hierarchical data flow diagrams–Extended finite state machines (EFSMs)–Local variables–TimersSDL Evolution–Widely used in telecommunications industry–First ITU Z.100 recommendation in 1980–Updated every 4 years–SDL-92 added support for object-oriented features–SDL-2000 adds support for hierarchical EFSMs (equivalent to Statecharts)4Commercial Tools for SDL-Based V&VTools can provide a variety of functions–Graphical editing & syntax checking–Model checking (static analysis)–Executable simulation & animation of a model–Validation of a model against a use case–Specification-based generation of test casesTelelogic appears to be market leader in this area–Tau/SDL is one of the leading tools–ObjectGeode also acquired by Telelogic–SAFIRE-SDL by SolinetTau/SDL was used for this project–15 licenses available under arrangement with UMD (handled through Prof. Basili in CS dept.)–C compiler (Borland recommended) must be installed in order to generate executables for simulation and validation5General Methodology6Remote Observing Platform: System Context7Remote Observing Platform: Domain Model8MSC TurnOnInstrument9MSC TurnOffInstrument10MSC Observe11Tau/SDL Model Structure12Observatory System Diagramsystem Observatory 1(1)SIGNALBufferDumpComplete(charstring),DataAvailable(integer),DownloadData,DumpDataBuffer(charstring),Expose(charstring, Integer, Integer,Integer, Integer, Duration, charstring),ExposureComplete(charstring),GSLock,InstrumentData(integer),InstrumentOn(charstring),InstrumentOff(charstring),InstrumentReady(charstring),InstrumentPowerOff(charstring),PhotonArrival(integer),Slew (integer, integer),SlewComplete;InstrumentModuleSupportModuleTelescopeBlockC1InstrumentOn,InstrumentOff,Expose,DumpDataBufferC2InstrumentReady,InstrumentPowerOff,ExposureComplete,BufferDumpCompleteC9InstrumentDataC5GSLockC7SlewC3DownloadDataC8PhotonArrival,SlewCompleteC6PhotonArrivalC4DataAvailable13InstrumentModule Block Diagramblock InstrumentModule 1(1)SIGNALAcquireGS,DoExposure (Duration, charstring),DropLock,GSLocated,LocateGS (integer, integer),LockEstablished;InstManagerBlockGuiderBlockCAM1C1IM1InstrumentOn,InstrumentOff,Expose,DumpDataBufferIM7LocateGS,AcquireGS,DropLockIM8GSLocated,LockEstablishedIM2InstrumentReady,InstrumentPowerOff,ExposureComplete,BufferDumpCompleteC2IM3SlewC7IM9InstrumentOn,InstrumentOff,DoExposure,DumpDataBuffer,PhotonArrivalIM10InstrumentReady,InstrumentPowerOff,ExposureComplete,BufferDumpComplete,InstrumentDataIM5InstrumentDataC9C5IM6GSLockC8IM4PhotonArrival,SlewComplete14CAM1 Block Diagramblock CAM1 1(1)SIGNALOpenShutter, CloseShutter, ShutterOpen, ShutterClosed,PositionFilter (charstring), HomeFilter, FilterInPlace,ReadOut, ExpComplete, ROComplete, Integrate (Duration);Shutter(1,1):ShutterCameraManager(1,1):HomingCameraManagerInstElectronics(1,1):InstElectronicsDataBuffer(1,1):DataBufferDetector(1,1):DetectorFilterAssembly(1,1):CAM1FilterSubsystemCameraManager HomingCameraManagerFIlterSubsystem CAM1FilterSubsystemDetectorInstElectronicsDataBuffer ShutterIM10IM9CB17PhotonArrivalSH4CB6ShutterOpen,ShutterClosedSH2CM6CB3InstrumentOn, InstrumentOffCM3IE1CB4InstrumentReadyIE2CM4CB2InstrumentReady, InstrumentPowerOff,ExposureComplete, BufferDumpCompleteCM2CB5OpenShutter, CloseShutterCM5SH1CB14DumpDataBufferCM14DB2CB16InstrumentDataDB4CB15BufferDumpCompleteDB3CM15CB9Integrate,ReadOutCM9DT1CB10ExpComplete,ROCompleteDT2CM10CB13InstrumentDataDT4DB1CB7PositionFilter,HomeFilterCM7FA1CB8FilterInPlaceFA2CM8CB12PhotonArrivalFA4DT3CB11PhotonArrivalSH3FA3CB1InstrumentOn, InstrumentOff, DoExposure,DumpDataBufferCM115Shutter Process Diagramprocess type Shutter 1(1)DCLCounts Integer;VIRTUALClosedVIRTUALOpenShutterShutterOpenOpenOpenVIRTUALPhotonArrival(Counts)PhotonArrival(Counts) via SH3-VIRTUALCloseShutterShutterClosedClosedSH1OpenShutter,CloseShutterSH2ShutterOpen,ShutterClosedSH3PhotonArrivalSH4PhotonArrival16CameraManager Process Diagramprocess type CameraManager 1(1)DCLExpFilter charstring, ExpTime Duration, SelfSI charstring;VIRTUALPoweredOffVIRTUALInstrumentOn(SelfSI)InstrumentOn(SelfSI) via CM3WarmingUpVIRTUALInstrumentReady(selfSI) InstrumentReady(selfSI) via CM2Ready*VIRTUALInstrumentOff(SelfSI)InstrumentOff(SelfSI) via CM3InstrumentPowerOff(SelfSI) via CM2PoweredOffReadyVIRTUALDoExposure(ExpTime,ExpFilter)OpenShutterOpeningShutterVIRTUALShutterOpenPositionFilter(ExpFilter)MovingFilterMovingFilterVIRTUALFilterInPlaceIntegrate (ExpTime)ExposingExposingVIRTUALExpCompleteCloseShutterClosingShutterVIRTUALShutterClosedReadOutReadingOutVIRTUALROCompleteExposureComplete(selfSI)ReadyVIRTUALDumpDataBuffer(selfSI)DumpDataBuffer(selfSI)via CM14DumpingVIRTUALBufferDumpComplete(SelfSI)BufferDumpComplete(selfSI)via