advertisement

VMCAI04

50 %
50 %
advertisement
Information about VMCAI04
Education

Published on January 16, 2008

Author: Manlio

Source: authorstream.com

advertisement

Rule-Based Runtime Verification:  Rule-Based Runtime Verification Howard Barringer Allen Goldberg Klaus Havelund Koushik Sen Overview:  Overview Run-time Monitoring About EAGLE Enhanced Formal Testing Summary NASA Mars Missions:  NASA Mars Missions Missions are becoming frequent MER1 (landed) and MER2 (24 Jan) By 2009: mobile science lab to land on / near polar icecap. Long-range and long-duration Demonstrate hazard avoidance “Smart” system Autonomous for long periods Mustn’t die! Motivation for Runtime Verification:  Motivation for Runtime Verification Model checking and Theorem Proving are rigorous, but: Not fully automated: model creation is often manual Abstraction is often manual in the case of model checking Lemma discovery is often manual in the case of theorem proving Therefore: not very scalable Applied Testing is scalable and widely used, but is ad hoc: Lack of formal coverage Lack of formal conformance checking Combine Formal Methods and Testing Run-time Verification:  Run-time Verification Combine temporal logic specification and testing: Specify properties in some temporal logic. Instrument program to generate events. Monitor properties against a trace of events emitted by the running program. Pros: Formal conformance checking Automated Scalable Cons: Formulation of properties is hard: To quote NASA software engineer: “I have absolutely no idea what this system should satisfy”. Lack of Coverage A Model-Based Verification Architecture:  test & property generation event stream Implemented system under test instrumentation dispatch Observer Model test inputs behavioural properties reports A Model-Based Verification Architecture Rqmts Deadlock Dataraces instrumentation Other Work on Monitoring Logics:  Other Work on Monitoring Logics Our own previous work: propositional future and past time LTL MaC Tool (UPenn): past time interval logic + state Temporal Rover (commercial tool) (future and past time LTL + real-time and some data handling). Finkbeiner and Sipma: statistical future time LTL. Simmons et al. (CMU): interval logic. … See ENTCS online-proceedings for the three previous runtime verification workshops: RV’01, RV’02, RV’03. RV’04: Barcelona, Spain (satellite workshop to ETAPS 2004): http://ase.arc.nasa.gov/rv2004 So many logics …:  So many logics … What is the most basic, yet, general specification language suitable for monitoring? EAGLE is our answer. Based on recursive rules over three “temporal connectives”: next, previous and concatenation. Can encode future time temporal logic, past-time logic, ERE, µ-calculus, real-time, data-binding, statistics…. Introducing EAGLE:  Introducing EAGLE Rule-based finite trace monitoring logic User defines a set of combinators a set of monitoring formulas Monitoring formulas are evaluated over a given input trace, on a state by state basis Evaluation proceeds by checking facts about the past and generating obligations about the future. EAGLE by example: LTL:  EAGLE by example: LTL max Always(Form F) = F /\ ⃝ Always(F) . min Eventually(Form F) = F \/ ⃝ Eventually(F) . min EventuallyP(Form F) = F \/ ⊙ EventuallyP(F) . To monitor the LTL formula ⃞(x>0 → ⃟ y=3), write mon M = Always(x > 0 -> Eventually(y=3)) . EAGLE by example: data binding :  EAGLE by example: data binding ⃞(x > 0 → Ǝk. k = x /\ ⃟ y = k) or written as: ⃞(x > 0 → let k = x in ⃟ y = k) is expressed in Eagle as: min R(int k) = Eventually(y=k) . mon M = Always(x>0 → R(x)) . EAGLE by example: metric LTL:  EAGLE by example: metric LTL Timed operators, such as: ⃟[t1,t2] assume events are time-stamped – state variable clock min EventuallyAbs(Form F, float t1, float t2) = clock <= t2 /\ (F → t1 <= clock) /\ ( ~ F → ⃝ EventuallyAbs(F, t1, t2)) . min EventuallyRel(Form F, float t1, float t2) = EventuallyAbs(F, t1+clock, t2+clock) . EAGLE by example: timed automata:  EAGLE by example: timed automata max N0(double x) = label == “in” /\ clock <= x+5 /\ ⃝ N1(x,clock) . max N1(double x,y) = label == “out” /\ clock <= y+12 /\ clock <= x+15 /\ ⃝ N0(clock) . in out x := 0 x<=5 x<=15 y<=12 N0 N1 x := 0 y := 0 EAGLE by example: statistical logics:  EAGLE by example: statistical logics Monitor that state property F holds with at least probability p: max Empty() = false . min Last() = ⃝Empty() . min A(Form F, float p, int f, int t) = ( Last() /\ (( F /\ (1 – f/t) >= p) \/ (¬F /\ (1 – (f+1)/t) >= p)) ) \/ (¬Last() /\ (( F → ⃝A(F, p, f, t+1)) /\ (¬F → ⃝A(F, p, f+1, t+1))) . min AtLeast (Form F, float p) = A(F, p, 0, 1) . EAGLE by example: beyond regular:  EAGLE by example: beyond regular Monitor a sequence of login and logout events – at no point should there be more logouts than logins and they should match at the end of the trace. min Match (Form F1, Form F2) = Empty() \/ F1  Match(F1, F2)  F2  Match(F1, F2) mon M1 = Match(login, logout) Syntax:  Syntax Semantics:  Semantics Some EAGLE facts:  Some EAGLE facts EAGLE-LTL (past and future). Monitoring formula of size m has space complexity bounded by m2 2m log m EAGLE with data binding has worst case dependent on length of input trace EAGLE without data is at least Context Free EAGLE logic currently implemented by rewriting as a Java application EAGLE: Internal Calculus:  EAGLE: Internal Calculus Uses four functions init: Form X Form X Form -> Form transforms a monitor formula (1st arg) for evaluation, in particular the primitive ⃝ and ⊙ are replaced by rules Next and Previous with history parameters introduced to past-time rules eval: Form X State -> Form applies the given state to the formula yielding the obligation for the future update: Form X State X Form X Form -> Form updates the past time components in the formula (1st arg) value: Form -> Bool yields the value of the given formula at the end of monitoring EAGLE: Internal Calculus – eval - II:  EAGLE: Internal Calculus – eval - II eval«Next(F), s» = update «F, s, null, null» Evaluation of a next time formula Next(F) yields the obligation to evaluate F in the next state. Note that any past time args are updated by application of update eval«Previous(F, past), s» = eval«past, s» Since past is the (possibly partial) evaluation of F from the previous state, the evaluation of a previous time formula must just re-evaluate past in the current state The cases of eval for rule definitions are synthesised from the rules Correctness of EAGLE calculus:  Correctness of EAGLE calculus Theorem: s1,s2,…sn, 1 ╞D F iff value(eval(…eval(eval(init(F,null, null), s1), s2)…, sn)) = true for all state sequences s1..sn and formulas F EAGLE: Simplification rules:  EAGLE: Simplification rules For efficiency, we use the propositional decision of Hsiang, where formulas are represented in Exclusive Or normal form. We use the following rewrite rules: F /\ F = F . false /\ F = false . true /\ F = F . ¬ F = true ⊕ F . false ⊕ F = F . F1 /\ (F2 ⊕ F3) = (F1 /\ F2) ⊕ (F1 /\ F3) . F1 \/ F2 = (F1 /\ F2) ⊕ F1 ⊕ F2 . Example Execution:  Example Execution Specification: max A(Term f) = f /\ @ A(f) . min E(Term f) = f \/ @ E(f) . mon M = A( x > 0 → E(x == 0)). Trace: x=1 x=2 x=0 x=3 ⃞(x > 0 → ⃟ x = 0) Trace Evaluation :  Trace Evaluation ⃞(x > 0 → ⃟ x = 0) Formulas: [A(((x > 0) /\ E(((x == 0) ++ (x == 0) /\ Next(E(rec)) ++ Next(E(rec)))) /\ Next(A(rec)) ++ (x > 0) /\ Next(A(rec)) ++ Next(A(rec))))] state = {x=1} ⃟ x = 0 ∧⃞(x > 0 → ⃟ x = 0) E(((x == 0) ++ (x == 0) /\ Next(E(rec)) ++ Next(E(rec)))) /\ A(((x > 0) /\ E(((x == 0) ++ (x == 0) /\ Next(E(rec)) ++ Next(E(rec)))) /\ Next(A(rec)) ++ (x > 0) /\ Next(A(rec)) ++ Next(A(rec)))) state = {x=2} ⃟ x = 0 ∧⃞(x > 0 → ⃟ x = 0) A(((x > 0) /\ E(((x == 0) ++ (x == 0) /\ Next(E(rec)) ++ Next(E(rec)))) /\ Next(A(rec)) ++ (x > 0) /\ Next(A(rec)) ++ Next(A(rec)))) /\ E(((x == 0) ++ (x == 0) /\ Next(E(rec)) ++ Next(E(rec)))) state = {x=0} ⃞(x > 0 → ⃟ x = 0) A(((x > 0) /\ E(((x == 0) ++ (x == 0) /\ Next(E(rec)) ++ Next(E(rec)))) /\ Next(A(rec)) ++ (x > 0) /\ Next(A(rec)) ++ Next(A(rec)))) state = {x=3} ⃟ x = 0 ∧⃞(x > 0 → ⃟ x = 0) E(((x == 0) ++ (x == 0) /\ Next(E(rec)) ++ Next(E(rec)))) /\ A(((x > 0) /\ E(((x == 0) ++ (x == 0) /\ Next(E(rec)) ++ Next(E(rec)))) /\ Next(A(rec)) ++ (x > 0) /\ Next(A(rec)) ++ Next(A(rec)))) Warning: Property M violated. EAGLE: Implementation:  EAGLE: Implementation Initial implementation as a Java application Two phases: System compiles the rule and monitor specification file to generate a set of Java classes, one for each rule and monitor System then compiles the generated class files to Java bytecode and runs the monitoring engine on a given input trace EAGLE interface:  EAGLE interface class Observer { Monitors mons; State state; eventHandler(Event e){ state.update(e); mons.apply(state); } } class State { int x,y; update(Event e){ x = e.x; y = e.y; } } class Monitors { Formula M1, M2; apply(State s){ M1.apply(s); M2.apply(s); } } class Event { int x,y; } e1 e2 e3 … User defines these classes K9 Planetary Rover Executive:  K9 Planetary Rover Executive Executive receives flexible plans from a planner for direct execution Plan is a hierarchical structure of actions Branching based on dynamic conditions – flexible start and stop times Multi-threaded system (35K lines of C++) Excellent vehicle for case studies on validation/verification technology – essential for autonomy insertion Running X9 Generates Web-Based Output:  Running X9 Generates Web-Based Output K9-Rover Executive plan & property generation event stream EAGLE engine instrumentation filter Observer Model of Plans plan inputs behavioural properties reports Manual Instrumentation Future Work:  Future Work Implementation: Optimisation of implementation – especially regarding partial evaluation (past time logic + data bindings). Specification: Support user-defined surface syntax. Consider integration of EAGLE with algebraic specs, or other spec language, such as ASM, SpecWare, …, Java. Better means for associating actions with formulas – towards aspect oriented programming, fault-tolerance. Experiment with different logics in Eagle: real-time, statistics, ERE, …. Instrumentation: Incorporate automated program instrumentation. Other Case studies: Analyze log files generated during tests from planning tool (NASA) Hardware monitoring for Rainbow (Manchester University) Summary:  Summary EAGLE is a succinct but highly expressive finite trace monitoring logic. Can elegantly encode any monitoring logic we have investigated. EAGLE can be efficiently implemented, but users must remain aware of expensive features. EAGLE demonstrated once by integration within a formal test environment, showing the benefit of novel combinations of formal methods and test. EAGLE can handle very limited form of action in current version. Other EAGLE papers:  Other EAGLE papers Barringer, Goldberg, Havelund, Sen: EAGLE does Space Efficient LTL Monitoring Submitted for publication (also http://www.cs.man.ac.uk/cspreprints/PrePrints/cspp25.pdf) EAGLE Monitors by Collecting Facts and Generating Obligations (also http://www.cs.man.ac.uk/cspreprints/PrePrints/cspp26.pdf) EAGLE for Real (Real-Time and Data Handling) – in preparation. If you’re interested in flying with EAGLE: Ask us

Add a comment

Related presentations

Related pages

Fifth International Conference on Verification, Model ...

The Fifth International Conference on Verification, Model Checking and Abstract Interpretation follows the successful events held in Port Jefferson (1997 ...
Read more

§q®Å§ >1QNRÒ¬¶F QSRD>hID=9½`=?QS;PQSTG¦';1@J;jEG ...

§q®Å§ >1qnrÒ¬¶f qsrd>hid=9½`=?qs;pqstg¦';1@j;jeg®h=?tv=¶tv= ¦ egf9;1hneg®×¬¶>1hsf'=?m ¦/¦ fx=n=?ªÁmdeu»+t©q&qn>x>a­)egf9=s=oqntg¬of
Read more

Complete - Max Planck Institute for Software Systems

A Complete Metho d for the Syn thesis of Linear Ranking F unctions Andreas P o delski and Andrey Rybalc henk o Max-Planc k-Institut f ur Informatik Saarbr ...
Read more

Database Group — LFCS - University of Edinburgh

The School of Informatics at the University of Edinburgh has a growing database group. It is part of the Laboratory for the Foundations of Computer Science ...
Read more

Applying Jlint to Space Exploration Software - Staff

Applying Jlint to Space Exploration Software Cyrille Artho1 and Klaus Havelund2 1 Computer Systems Institute, ETH Zurich, Switzerland 2 Kestrel Technology ...
Read more

) ˇ ˘ - Stanford University

+ f ˙ ˆ ˚˚ ˙ ˘ + , ˚ ˘ + ,˝ ˚ ˆ i ˙ ˙ ’ .>#j$5"j+ˇj$2**/1 ! > :ˇ2 j",.+j+ˇ/1k˘
Read more

Symposium on Operating Systems Principles - Wikipedia, the ...

The Symposium on Operating Systems Principles (SOSP), organized by the Association for Computing Machinery (ACM), is one of the most prestigious [1] [2] [3 ...
Read more

Fifth International Conference on V Model C A I VMCAI

VMCAI2004 Fifth International Conference on Verification,Model Checking, and Abstract Interpretation Università Ca’Foscari,Venice,January 11–13,2004
Read more

Symbolic Implementation of the Best Transformer

Symbolic Implementation of the Best Transformer Thomas Reps , Mooly Sagiv , and Greta Yorsh Comp. Sci. Dept., University of Wisconsin; reps@cs.wisc.edu
Read more