Methods and Tools for Validation

Methods and Tools for Validation

Methods and Tools for ValidationModelling and AnalysisKim G. LarsenResearch ProfileDistributed Systems & Semantics UnitSemantic Models concurrency, mobility, objects real-time, hybrid systemsValidation & Verification algorithms & tools Construction real-time & network systemsTOV 2002Kim G. Larsen21

Methods and Tools for Validation

BRICS Machine30+40+40 MillkrBasic Research in Computer Science100100 ToolsAalborgTOV 2002AarhusKim G. LarsenOther revelvant projects UPPAAL, VHS, VVS, WOODDES3Tools and BRICSApplicationsvisualSTATEPVS HOLSPINTLPUPPAALALFLogic Temporal Logic Modal Logic MSOL AlgorithmicSemantics Concurrency Theory Abstract Interpretation Compositionality Models for real-time & hybrid systems (Timed) Automata Theory Graph Theory BDDs Polyhedra Manipulation TOV 2002Kim G. Larsen42

Methods and Tools for Validation

Indlejret software ?80% af al software er indlejret i interagerende apparater. Krav om stigende funktionalitet med minimale resourcer Udvikler skal ideelt set have adskillige kvalifikationersofwarekonstr. og –udvikl. hardware platforme, kommunikatíon & protokoller, validering (test og verifikation),……….TOV 2002 Kim G. Larsen 5A very complex systemKlaus Havelund, NASATOV 2002Kim G. Larsen63

Methods and Tools for Validation

Rotterdam Storm Surge BarrierTOV 2002Kim G. Larsen7Spectacular BugsARIANE-5 INTEL Pentium II floating-point division 470 Mill US $ Baggage handling system, Denver 1.1 Mill US $/day for 9 months Mars Pathfinder Radiation theraphy, Therac-25 ……. More in JPK, CWTOV 2002 Kim G. Larsen 84

Methods and Tools for Validation

Embedded SystemsSyncMaster 17GLsiMobile Phone Telephone Digital Watch TamagotchiTOV 2002Kim G. Larsen9A simple programInt xx Int Process INC Process INC do do :: x<200 --> x:=x+1 :: x<200 --> x:=x+1 od od Process DEC Process DEC do do :: x>0 --> x:=x-1 :: x>0 --> x:=x-1 od od Process RESET Process RESET do do :: x=200 --> x:=0 :: x=200 --> x:=0 od od fork INC; fork DEC; fork RESET fork INC; fork DEC; fork RESETAlwaysTOV 2002 Kim G. Larsen 10Which values may x take ?Questions/Properties: E<>(x>1000) E<>(x>2000) A[](x<=2000) E<>(x<0) A[](x>=0) Possibly5

Methods and Tools for Validation

Introducing, Detecting and Repairing Errors Liggesmeyer 98TOV 2002Kim G. Larsen11Introducing, Detecting and Repairing Errors Liggesmeyer 98TOV 2002Kim G. Larsen126

Methods and Tools for Validation

Suggested Solution?Model based validation, verfication and testing of software and hardwareTOV 2002Kim G. Larsen13Verification & ValidationAnalysis Design Model SpecificationImplementation TestingTOV 2002 Kim G. Larsen 147

Methods and Tools for Validation

Verification & ValidationAnalysisValidationDesign ModelL UM L SDSpecificationVerification & RefusalImplementation TestingTOV 2002 Kim G. Larsen 15Verification & ValidationAnalysisValidationDesign ModelUM L SD LModel ExtractionSpecificationVerification & RefusalAutomatic Code generationImplementation TestingTOV 2002 Kim G. Larsen 168

Methods and Tools for Validation

Verification & ValidationAnalysisValidationDesign ModelL UM L SDModel ExtractionSpecificationVerification & RefusalAutomatic Code generationAutomatic Test generationImplementation TestingTOV 2002 Kim G. Larsen 17How?Unified Model = State Machine!b? b? b x! a? y y! x Output portsa Input portsControl statesTOV 2002Kim G. Larsen189

Methods and Tools for Validation

TamagotchiALIVEPassive A Feeding Meal B A Health:= B Health-1 Snack A Clean LightABCCare AHealth=0 or Age=2.000 TickA Medicine A Discipline PlayDEADAAHealth:=Health-1; Age:=Age+1 TOV 2002 Kim G. Larsen 19SYNCmasterTOV 2002Kim G. Larsen2010

Methods and Tools for Validation

Digital WatchTOV 2002Kim G. Larsen21The SDL Editor The SDL EditorThe SDL EditorProcess level Process levelTOV 2002Kim G. Larsen2211

Methods and Tools for Validation

SPIN, Gerald Holzmann AT&TTOV 2002Kim G. Larsen23visualSTATEVVSw Baan Visualstate, DTU (CIT project)Hierarchical state systems Flat state systems Multiple and interrelated state machines Supports UML notation Device driver accessTOV 2002Kim G. Larsen2412

Methods and Tools for Validation

ESTERELTOV 2002Kim G. Larsen25UPPAALTOV 2002Kim G. Larsen2613

Methods and Tools for Validation

‘State Explosion’ problemM1a 1 2M2bc34M1 x M21,a 4,a 1,b 2,b 1,c 2,c3,a4,a3,b4,b3,c4,cAll combinations = exponential in no. ofTOV 2002 Kim G. Larsenca eti eor e h ly t bl components rovab tracta P in27lTrain Simulator1421 machines 11102 transitions 2981 inputs 2667 outputs 3204 local states Declare state sp.: 10^476VVS visualSTATEBUGS ?tion fica de i ver nitu ced mag u of red as rders sec) h o 6 es l iuq era s to chn h sev 4 day r te it 1 Ou e w (ex im tTOV 2002 Kim G. Larsen 2814

Methods and Tools for Validation

Modelling and AnalysisSoftware Model A No!AnalysisRequirement F YesTOV 2002Kim G. Larsen29Modelling and AnalysisSoftware Model A No! Debugging InformationTOOLRequirement FYes, Prototypes Executable Code Test sequencesTools: UPPAAL, visualSTATE, ESTEREL, SPIN, Statemate, FormalCheck, VeriSoft, Java Pathfinder,…TOV 2002 Kim G. Larsen 3015

Methods and Tools for Validation

Modelling and AnalysisSoftware Model A Se ma nti csBRICSNo! Debugging InformationTOOLRequirement F Lo g icAlg orithm icsYes, Prototypes Executable Code Test sequencesTools: UPPAAL, visualSTATE, ESTEREL, SPIN, Statemate, FormalCheck, VeriSoft, Java Pathfinder,…TOV 2002 Kim G. Larsen 31Tool Support (model checking)System Description ANo! Debugging InformationTOOLRequirement FYes, Prototypes Executable Code Test sequencesTools: U …… 此处隐藏：3593字，全部文档内容请下载后查看。喜欢就下载吧 ……