pecheur

Information about pecheur

Published on January 22, 2008

Author: Carla

Source: authorstream.com

Content

Symbolic Model Checking of Domain Models for Autonomous Spacecrafts:  Symbolic Model Checking of Domain Models for Autonomous Spacecrafts Charles Pecheur (RIACS / NASA Ames) Model-Based Autonomy:  Model-Based Autonomy Goal: "intelligent" autonomous spacecrafts cheaper (smaller ground control) more capable (delays, blackouts) General reasoning engine + application-specific model Use model to respond to unanticipated situations For planning, diagnosis Huge state space, reliability is critical model of Livingstone:  Courtesy Autonomous Systems Group, NASA Ames Livingstone Remote Agent's model-based diagnosis sub-system Livingstone Models:  Livingstone Models concurrent transition systems (components) synchronous product enumerated types => finite state Essentially ≈ SMV model + nominal/fault modes, commands/monitors (I/O), probabilities on faults, ... Closed Valve Open Stuck open Stuck closed Open Close inflow = outflow = zero Courtesy Autonomous Systems Group, NASA Ames p=0.001 p=0.01 Diagnosis = find the most likely assumptions (modes) that are consistent with the observations (commands/monitors) inflow = outflow inflow, outflow : {zero,low,high} Large State Space?:  Large State Space? Example: model of ISPP = 7.16·1055 states This is only the Livingstone model – a complete verification model could be Exec driver (10-100 states) x Spacecraft simulator (1055 states) x Livingstone system (keeps history – 10n·55 states) Verify a system that analyzes a large state space! Approach: the model is the program Verify it (using symbolic model checking) Assume Livingstone correct (and complete) MPL2SMV:  MPL2SMV Livingstone Model SMV Model Livingstone Requirement SMV Requirement Livingstone Trace SMV Trace Autonomy Verification Translator from Livingstone to SMV:  Translator from Livingstone to SMV Co-developed with CMU (Reid Simmons) Similar semantics => translation is easy Properties in temporal logic + pre-defined patterns Initially for Livingstone 1 (Lisp), upgraded to Livingstone 2 (C++/Java) Principle of Operations:  (load "mpl2smv.lisp") ;; load the translator ;; Livingstone not needed! (translate "ispp.lisp" "ispp.smv") ;; do the translation (smv "ispp.smv") ;; call SMV ;; (as a sub-process) Principle of Operations (defcomponent heater …) (defmodule valve-mod …) … (defverify :structure (ispp) :specification (all (globally …))) MODULE Mheater … MODULE Mvalve-mod … … MODULE main VAR Xispp:Mispp SPEC AG … Specification AG … is false as shown … State 1.1: … State 1.2: … ispp.lisp ispp.smv SMV output Lisp shell Simple Properties:  Simple Properties Supported by the translator: syntax sugar iterate over model elements (e.g. all component modes) Examples Reachability (no dead code) EF heater.mode = on Path Reachability (scenario) AG (s1 –> EF (s2 & EF (s3 & EF s4))) Probabilistic Properties:  Probabilistic Properties Use probabilities associated to failure transitions Use order of magnitude: -log(p), rounded to a small integer Combine additively, OK for BDD computations Approximate – but so are the proba. values heater.mode = overheat -> heater.proba = 2; (p = 0.01) proba = heater.proba + valve.proba + sensor.proba; SPEC AG (broken & proba < 3 –> EF working) Functional Dependency:  Functional Dependency Check that y=f(x) for some unknown f Use universally quantified variables in CTL = undetermined constants in SMV VAR x0,y0 : {a,b,c}; TRANS next(x0) = x0 TRANS next(y0) = y0 SPEC (EF x=x0 & y=y0) –> (AG x=x0 –> y=y0) Limitation: counter-example needs two traces, SMV gives only one => instantiate second half by hand, re-run SMV ≈  x0, y0 Temporal Queries:  Temporal Queries Temporal Query = CTL formula with a hole: AG (? –> EF working) Search (canonical) condition for ? that satisfies the formula (computable for useful classes of queries) Recent research, interrupted (William Chan, †1999) Problem: visualize solutions (CNF, projections, ...) Core algorithm implemented in NuSMV (Wolfgang Heinle) Deceptive initial results, to probe further SMV with Macro Expansion:  SMV with Macro Expansion Custom version of SMV (Bwolen Yang, CAV 99) Eliminates variables by Macro Expansion: analyzes static constraints of the model (invariants), find dependent variables x=f(x1,...,xn), substitute f(x1,...,xn) for x everywhere, eliminate x from the set of BDD variables. For models with lots of invariants => useful for Livingstone models Full ISPP model in < 1 min, vs. SMV runs out of memory. ISPP Model Statistics:  ISPP Model Statistics In Situ Propellant Production (ISPP) = turn Mars atmosphere into rocket fuel (NASA KSC) Original model state = 530 bits (trans. = 1060 bits) Total BDD vars 588 bits Macro expanded -209 bits Reduced BDD vars 379 bits Reachable state space 7.16·1055 = 2185.5 Total state space 1.06·1081 = 2269.16 Reachability of all modes (163): 29.14" CPU time in 63.6 Mb RAM Diagnosis Properties:  Diagnosis Properties Can fault F always be diagnosed? (assuming perfect diagnosis and accurate model) = is F unambiguously observable?  obs0 . (EF F & obs=obs0) –> (AG F –> obs=obs0) Similar to functional dependency obs = observable variables (many of them) Static variant (ignore transitions): SAT on two states S, S' such that F & ! F' & obs=obs' Diagnosis Properties Revisited:  Very recent (yesterday), with Alessandro Cimatti Can fault F be diagnosed knowing the last n steps? Apply SAT to: Variants are possible (e.g. fork at n-1 intead of 0) Diagnosis Properties Revisited ... Diagnosis Properties (cont'd):  Diagnosis Properties (cont'd) Does it work? Computational cost of extra variables Has it been done? Similar work in hardware testability? Is it useful? It is unrealistic to expect all faults to be immediately observable (e.g. valve closed vs. stuck-closed) What weaker properties? Are they verifiable? To be explored Summary:  Summary Verification of model-based diagnosis: Space flight => safety critical. Huge state space (w.r.t. fixed command sequence). Focus on models (the model is the program) Quite different from executable programs Loose coupling, no threads of control, passive. Huge but shallow state spaces. Symbolic model checking is very appropriate Verify well-formedness + validity w.r.t. hardware Verify suitability for diagnosis: to be explored Slide19:  Thank You

Related presentations


Other presentations created by Carla

notes india
13. 02. 2008
0 views

notes india

PVC and Coroplast Class
09. 01. 2008
0 views

PVC and Coroplast Class

aids in africa
10. 01. 2008
0 views

aids in africa

Lecture 12
10. 01. 2008
0 views

Lecture 12

SNAP ACS
11. 01. 2008
0 views

SNAP ACS

OnionD
12. 01. 2008
0 views

OnionD

defining generational values
13. 01. 2008
0 views

defining generational values

parasit4
15. 01. 2008
0 views

parasit4

UMB2 27 07 The Primates
15. 01. 2008
0 views

UMB2 27 07 The Primates

ch 3 classical thoery
22. 01. 2008
0 views

ch 3 classical thoery

Hebrew Religion and Ethics
22. 01. 2008
0 views

Hebrew Religion and Ethics

ARC FLASH ENERGY PROTECTION
24. 01. 2008
0 views

ARC FLASH ENERGY PROTECTION

asi06schi
24. 01. 2008
0 views

asi06schi

WAG IBW China Innovation
25. 01. 2008
0 views

WAG IBW China Innovation

TIMEMANAGEMENTTOOLS2
04. 02. 2008
0 views

TIMEMANAGEMENTTOOLS2

Orientation PP
09. 01. 2008
0 views

Orientation PP

noguera
11. 01. 2008
0 views

noguera

Photosynthesis 1
28. 01. 2008
0 views

Photosynthesis 1

A Presentation on Venturing
07. 02. 2008
0 views

A Presentation on Venturing

Reproduction06
07. 02. 2008
0 views

Reproduction06

SRH 6 07
14. 02. 2008
0 views

SRH 6 07

teen skin cancer whitebackground
25. 02. 2008
0 views

teen skin cancer whitebackground

Orlan
28. 02. 2008
0 views

Orlan

Lynch Ergonomics
05. 03. 2008
0 views

Lynch Ergonomics

WaterIndianCulture
10. 03. 2008
0 views

WaterIndianCulture

ThreeGorgesDam
19. 03. 2008
0 views

ThreeGorgesDam

RCCC LA VPMD Clarkson
28. 03. 2008
0 views

RCCC LA VPMD Clarkson

SmartMeteringScenari os
08. 04. 2008
0 views

SmartMeteringScenari os

SlipsTripsFallsMod1
14. 01. 2008
0 views

SlipsTripsFallsMod1

kroeana
16. 04. 2008
0 views

kroeana

4 HazCom Overview
18. 01. 2008
0 views

4 HazCom Overview

fall2007resumecoverl ette
14. 03. 2008
0 views

fall2007resumecoverl ette

KICKING OFF
18. 04. 2008
0 views

KICKING OFF

Australia Nuclear
23. 04. 2008
0 views

Australia Nuclear

Unit 20
24. 04. 2008
0 views

Unit 20

WSF
07. 05. 2008
0 views

WSF

GA Conf07Bowles
02. 05. 2008
0 views

GA Conf07Bowles

vangogh
26. 02. 2008
0 views

vangogh

060324 Wiethoff
18. 02. 2008
0 views

060324 Wiethoff

Designing a Wedding Sevice CW
05. 02. 2008
0 views

Designing a Wedding Sevice CW

crater controversy
22. 01. 2008
0 views

crater controversy

RAFT USNA PDR2
11. 01. 2008
0 views

RAFT USNA PDR2

es marw 6c verific
16. 01. 2008
0 views

es marw 6c verific

Sermon3 Risky Business
15. 01. 2008
0 views

Sermon3 Risky Business