Methods and Tools for Validation
时间:2025-07-11
时间:2025-07-11
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字,全部文档内容请下载后查看。喜欢就下载吧 ……
上一篇:毕业论文 餐厅VI设计
下一篇:农电工管理问题与对策 2