MaCMonitoring and Checking at RuntimeWhat is MaC?Software Development ProcessSoftware Development ProcessSoftware Development ProcessVerificationVerificationModel CheckingModel CheckingModel Checking - GOODModel Checking - PROBLEMVerificationTestingTesting – PROBLEMVerificationRuntime VerificationRuntime VerificationRuntime VerificationRuntime VerificationMaC 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 verificationRequirementImplementDesignAIBO.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 Verificationleg1leg2leg4leg3Model CheckingWalk Æ !(Fall)► Given– Requirement & Properties– Model ► Verify– Explore all paths– Violate requirement ??all-leg-down!walkleg1-up, leg4-upwalk & !fallleg2-up, leg3-upwalk & !fallleg1-up, leg2-upwalk & fallleg1leg2leg4leg3Model CheckingWalk Æ !(Fall)► Given– Requirement & Properties– Model ► Verify– Explore all paths– Violate requirement ??all-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 Verification1. Specify formal requirements (Walk Æ !Fall)Program (ex. AIBO) Verifier (MaC)2. ExecutionInformation3. Check4. Sat / Unsat4. FeedbackUserRuntime Verification► Rigorous and Formal► Done at implementation► Not complete– Guarantee for current executionRuntime Verification► MaC– Monitoring and Checking at Runtime– Components•MaCverifier• MaC formal languageMaC VerifierMaC VerifierProgramExecutionInformationCheckSat / UnsatFeedbackUserEvent RecognizerCheckerInjectorAbstract InfoMaC Verifier and LanguageProgramInstrumentedProgramMaC CompilerPEDL MEDLMaC SpecificationEventRecognizerChecker InjectorMaC VerifierSADL1. Which program info to probe2. How to map info to propertiesSystem Properties Where / whento 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 < 50position = 40 position = 55position = 60trueTime 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 MEDLAbstraction- When train position is between 30 and 50- When gate starts/ends being downJava Program PEDL MEDLRailroad 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 - PEDLAbstraction- When train position is between 30 and 50- When gate starts/ends being downposition = 0position = 20position = 40Gate.down()position = 55Gate.up()position = 60Java Program PEDLexport 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 endGD =
View Full Document