VMCAI04

Information about VMCAI04

Published on January 16, 2008

Author: Manlio

Source: authorstream.com

Content

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

Related presentations


Other presentations created by Manlio

gp SCM 1005
09. 01. 2008
0 views

gp SCM 1005

Product Information File
10. 01. 2008
0 views

Product Information File

Interviewing with the Ps
14. 01. 2008
0 views

Interviewing with the Ps

migraine
14. 01. 2008
0 views

migraine

finalwinkelman
15. 01. 2008
0 views

finalwinkelman

p2 4
04. 02. 2008
0 views

p2 4

Biomass use Kenya
11. 02. 2008
0 views

Biomass use Kenya

AdvancedPropulsion
16. 01. 2008
0 views

AdvancedPropulsion

Reading Word List 1 4
17. 01. 2008
0 views

Reading Word List 1 4

imrb
25. 01. 2008
0 views

imrb

emergency shelters
14. 02. 2008
0 views

emergency shelters

gek politicalecology
20. 02. 2008
0 views

gek politicalecology

sbodn prezo 040507
21. 01. 2008
0 views

sbodn prezo 040507

dinahsweet0108anon
05. 03. 2008
0 views

dinahsweet0108anon

culture
17. 01. 2008
0 views

culture

Armstrong Base Knowledge
18. 01. 2008
0 views

Armstrong Base Knowledge

Rhetorical Images
11. 03. 2008
0 views

Rhetorical Images

SONORA MEXICO2006
15. 03. 2008
0 views

SONORA MEXICO2006

LaPedis
19. 03. 2008
0 views

LaPedis

hw1
21. 03. 2008
0 views

hw1

TOPIC VII 6 Alex1
03. 04. 2008
0 views

TOPIC VII 6 Alex1

boyd
16. 04. 2008
0 views

boyd

s1350 nambiar
06. 02. 2008
0 views

s1350 nambiar

2 5 SVEDBERG PP Presentation
08. 05. 2008
0 views

2 5 SVEDBERG PP Presentation

P2007112912571112025 23783
02. 05. 2008
0 views

P2007112912571112025 23783

Good Night Mr 1
07. 02. 2008
0 views

Good Night Mr 1

MTCLGTrainingPart3
04. 02. 2008
0 views

MTCLGTrainingPart3

mideastpresentation
24. 01. 2008
0 views

mideastpresentation

SATZ Handout
23. 01. 2008
0 views

SATZ Handout

felon voting presentation
11. 01. 2008
0 views

felon voting presentation