MaC Monitoring and Checking at RuntimeWhat is MaC?Software Development ProcessSlide 4Slide 5VerificationSlide 7Model CheckingSlide 9Model Checking - GOODModel Checking - PROBLEMSlide 12TestingTesting – PROBLEMSlide 15Runtime VerificationSlide 17Slide 18Slide 19Slide 20MaC Verifier and LanguageAbstract InformationEventsConditionsMaC LanguagePEDL and MEDLInstrumentationMaC Language - PEDLMEDL – Property LanguageMaC Language - MEDLCurrent WorkQuantitative PropertiesExampleMaCMonitoring and Checking at RuntimePresented ByUsa SammapunCIS 700 Oct 10, 2005What is MaC?►A verification technique–Goal: Ensure a software program runs correctly►To understand software verification–Know how software is developed–Know how software is verifiedSoftware Development Process►Requirement and Properties•What program should do –When AIBO dog walks, it must not fall•Informal (English)  Formal (Logic, FSM)RequirementDesign ImplementWalk  !(Fall)Software Development Process►Design Specification and Analysis•How program fulfill requirements –AIBO dog coordinates his 4 legs•Formal modeling (UML, FSM, Control theory)•Analysis–Simulation–Verification (Model checking)RequirementDesignImplementSoftware Development Process►Implementation•Actual program (AIBO dog walking program in C++)•Varification & Validation–Testing–Runtime verificationRequirementImplementDesign AIBO.c++main() { int leg1,leg2; int leg3, leg4; …}Verification►Design–Model Checking►Implementation–Testing–Runtime VerificationMaCMonitoring and CheckingAt RuntimeVerification►Design–Model Checking►Implementation–Testing–Runtime VerificationModel Checking►Given–Requirement & Properties–Model ►Verify–Explore all paths–Violate requirement ??Walk  !(Fall)leg1leg2leg4leg3all-leg-down!walkleg1-up, leg4-upwalk & !fallleg2-up, leg3-upwalk & !fallleg1-up, leg2-upwalk & fallModel Checking►Given–Requirement & Properties–Model ►Verify–Explore all paths–Violate requirement ??Walk  !(Fall)leg1leg2leg4leg3all-leg-down!walkleg1-up, leg4-upwalk & !fallleg2-up, leg3-upwalk & !fallleg1-up, leg2-upwalk & fallModel Checking - GOOD►Rigorous and Formal–Based on Mathematics►Complete–Explore all pathsModel Checking - PROBLEM►Check Design, not implementation–What if implementation does not follow model?►Not scalable–What if the program is HUGH?•Explore all paths might not be feasibleVerification►Design–Model Checking►Implementation–Testing–Runtime VerificationTesting►We’ve seen it–Run actual program with different inputs–See if outputs are what we want►Ex. AIBO–Run AIBO dog–See whether or not AIBO dog falls►Good–Check directly the implementationTesting – PROBLEM►Not rigorous, Not formal–Possibly random inputs►Not complete–What if bugs never show up during test ??–What if it’s not AIBO, but a heart device !?!Verification►Design–Model Checking►Implementation–Testing–Runtime VerificationMaCMonitoring and CheckingAt RuntimeRuntime Verification►Given–Requirement & Properties–Implementation►Ensures the current program execution follows its formal requirementsWalk  !(Fall)Runtime VerificationProgram (ex. AIBO) Verifier (MaC)2. ExecutionInformation3. Check4. Sat / Unsat4. FeedbackUser1. Specify formal requirements (Walk  !Fall)Runtime Verification►Rigorous and Formal►Done at implementation►Not complete–Guarantee for current executionRuntime Verification►MaC–Monitoring and Checking at Runtime–Components•MaC verifier•MaC formal languageMaC VerifierProgramMaC VerifierExecutionInformationCheckSat / UnsatFeedbackUserEvent RecognizerCheckerInjectorAbstract InfoMaC Verifier and LanguageProgramInstrumentedProgramMaC CompilerPEDL MEDLMaC SpecificationEventRecognizerChecker InjectorMaC VerifierSADL1. Which program info to probe2. How to map info to propertiesSystem Properties Where / when to steerAbstract Information►To capture roughly and abstractly what the program is doing►Events–Instantaneous incidents –such as variable updates update(position)►Conditions–Proposition about the program that may be true/false/undefined for a duration of time –such as position < 50trueposition = 40 position = 55position = 60Time position < 50position < 50falseposition = 55position = 60s1s2s3s4position = 55 position = 40 position = 55position < 50Events►e - variable update, start/end method►e1 || e2 - or►e1 && e2 - and►start(c) - instant when condition c becomes true►end(c) - instant when condition c becomes false►e when c - e occurs when condition c is trueConditions►Conditions interpreted over 3 values: true, false and undefined.►c - boolean expression►!c - not c►c1 || c2 - or►c1 && c2 - and►c1 -> c2 - imply►defined(c) - true when c is defined►[e1, e2) - intervale1e2[e1 ,e2) [e1 ,e2)MaC Language►PEDL–How execution information transform into events and conditions►MEDL–Specify properties using events and conditionsPEDL and MEDLJava Program PEDL MEDLAbstraction - When train position is between 30 and 50 - When gate starts/ends being downRailroad Crossing Property: - If train is crossing, then gate must be down- Train is crossing when position is between 30 and 50Abstraction - When gate is downCheck - If train is crossing, then gate must be downposition = 0position = 20position = 40Gate.down()position = 55Gate.up()position = 60startGDendGDcrossViolationgateDowncrossInstrumentationclass Train { int position; main() { position = 0; position = 20; position = 40; position = 55;} }Train.position;class Train { int position; main() { position = 0; send(x,0); position = 20; send(x,20); position = 40; send(x,40); position = 55; send(x,55);} }+=Sent to Event Recognizer:[ (position,0), (position,20), (position,40), (position,55) ]MaC Language - PEDLposition = 0Java Program PEDLAbstraction - When train position is between 30 and 50 - When gate starts/ends being downposition = 20position = 40Gate.down()position = 55Gate.up()position = 60export event startGD, endGD; export condition cross; monobj Train.position; monmeth Gate.up(); monmeth Gate.down(); condition cross = (30 < RRC.position) && (RRC.position < 50); event startGD = endM(Gate.down()); event