CEC Presentation

CEC Presentation

Example of a Complementary use of Model Checking and Agent-based Simulation Gabriel Gelman & Karen Feigh Georgia Institute of Technology & John Rushby Stanford Research Institute Introduction Increasing Complexity Leads to Automation Surprises Such as Challenges in HMI Tackled by

Model Checking Agents Simulation Pilots Potential Issues Automation Combine to leverage benefits of both To examine System Behavior HMI = Human-Machine Interaction 2 Comparison: Model Checking/ Simulation Simulation

Model Checking Sophisticated models Simple models, few actions Limited to scenarios Exhaustive state space search Slow (one simulation takes time) Fast (millions of runs in seconds) Time can be explicitly modeled No explicit modeling of time High-Fidelity aircraft dynamics Cannot handle continuity (state explosion) 3 Method: Connecting the Frameworks

Extending the Counterexample Guided Abstraction Refinement (CEGAR) method Scenario Narrative Create Model & Specifications for Model Checking (SAL) Analyze Using Model Checking (SAL) Analyze Using Simulation (WMC) Create Models & Metric Specifications for Simulation (WMC) 1. Verify that the action sequence predicted by MC to be problematic continues to be problematic 2. Refine MC prediction to include specific temporal relationships between events 4 Automation Surprise Aviation Case Study

Automation Surprise An Automation Surprise occurs when the automation behaves in a manner that is different from what the operator is expecting, Palmer (1995) + Result of implementation of badly designed automation or lack of pilots training on system + Introduction of highly automated aircraft (glass cockpits) Starting with aircraft like B-757, B-737 and A320 Sarter and Woods A320 study (80% surprised; n = 167) Failure to activate Approach 6 Automatic Mode Changes Case Study: Airbus Automatic Speed Protection Sequence on approach Flight Path Angle mode engaged Airspeed too fast

Overspeed Protection Open mode engaged OPEN CLIMB FCU altitude with respect to current altitude Higher Lower OPEN DESCENT Note: During descent FCU altitude is usually set to Missed Approach altitude if Go Around required 7 FCU: Flight Control Unit V/S: Vertical Speed FPA: Flight Path Angle Sequence Automation Surprise

FPA = 3 1 e.g. 5000ft FCU Altitude = Go Around Altitude Altitud e Inst rum ent La 5 2 ndin g 3 Syst em

(ILS ) 4 Glid eslo p 10 > FPA > 3 e Ground Runway Step 1: Aircraft is on ILS Glideslope and in FPA V/S mode Step 2: Air Traffic Control tells aircraft to level off Step 3: Aircraft tries to recapture ILS Glideslope with higher FPA Step 4: Because of steeper approach the speed exceeds Vmax Step 5: Mode change to OP CLB because FCU alt higher than current alt 8 FCU: Flight Control Unit FPA: Flight Path Angle Modeling Platforms

Model Checking: SAL (Symbolic Analysis Laboratory) + Simple models are checked for a given property + Reachable state space of a specification is explored + Exhaustive exploration of action space Symbolic Model Checking does not require to explore full space Abstract System Model Trace of Actions State OK Initial Conditions Start List State 1 State 3

Actioni State 2 State NOT OK List (singe action or combination of actions) 10 Case Study Modeled in SAL Initial State (FCU Alt = 3201 feet) Airplane: Flies (descending) Automation: VS/FPA mode Pilot: Extends Flaps 1 Airplane: Flies with Flaps (descending) Automation: OP CLB mode 4

Pilot: Does nothing 5 Alt increase from 2990 to 3291 Mental Model still in descend Positive Pitch 11 Note: Each step is a state transition, time is not modeled 2 3 AUTOMATION SURPRISE Airplane: Flies (descending) Automation: Track Mode

Pilot: Dials Descend Airplane: Flies with Flaps (descending) (exceeds Vmax) Automation: Reverses Mode Pilot: Does nothing State State Transition FCU: Flight Control Unit Airplane: Flies with Flaps (descending) Automation: OP CLB mode Pilot: Does nothing 6 Step 1 2 3 4 5 6 Flight Mode Airspeed Altitude Flaps Max Speed Mental Model Pitch Other

200 3000 Retracted 400 Level -1/100 V/S FPA 201 2989 Retracted 400 Descend -1/100 V/S FPA 200 2988 Extended 180 Descend 0 OPEN CLB 201 2989 Extended 180 Descend 0 OPEN CLB 200 2990 Extended

180 Descend 1/50 OPEN CLB 190 3291 Extended 180 Descend 3/100 Simulation: WMC (Work Models that Compute) Actions Resources Scripted Events Expectations Agents Initial Conditions SIM Core

Altitude, Heading, Mental Model WMC Work Model Aircraft Work Model Speed, Vertical Speed Auto Surprise Pulls Human Agent Stores Mental Model Updateable World Representation

Traces of Key Metrics 12 Simulation Runs Based on MC Output 1. 2. Verify that the action sequence predicted by SAL to be problematic continues to be problematic Refine SAL's prediction to include specific temporal relationships between events Step 1: Arm Approach Step 2: Extend Flaps Step 3: Monitor Speed 13 t = 2: Arm Approach

Becomes t = 5: Extend Flaps t = 9: Monitor Speed Simulation States that Varied Cruise Go Around Altitude AR ST ch oa pr ap Flaps Extension Speed Altitud

e Level Off Altitude Level Off Duration ILS G lide slo pe FPA = 3 Ground Runway STAR: Standard Terminal Arrival Route ILS: Instrument Landing System FPA: Flight Path Angle 14 Results

Meaningful Scenarios from Simulation Traces Simulation Traces Leads to OPEN DES Automation Surprise OPEN CLB No Auto Surprise No Change 16 Overview of Scenarios in Simulation Output SC 1 Mode AS DES No 2 3

CLB DES 4** CLB 5 DES 6 CLB Description Mode reversion before level off, early flaps extension leads to overspeed Yes --"-Yes* Mode reversion after level off, early flaps extension leads to overspeed Yes --"-Yes* After level off, dive leads to overspeed on current flap configuration Yes --"-- SC: Scenario AS: Automation Surprise (*) Possibly due to artifact

(**) SAL Scenario 17 SAL Model Checking Matching Case Action Extend flaps Level Off Altitude Level Off Duration GA Altitude 18 Value 201 knots 3200 feet 100 seconds 3281 feet WMC Unknown time step

Scenario 4: OPEN CLB 1. 2. 3. 4. Level off Return to glideslope (dive) Flaps Extension Sets max speed below current speed (former max speed = 220 knots, max speed with flaps = 205 knots) Zoom 19 5. OPEN CLB engages 6. Aircraft climbs Scenario 6: OPEN CLB 1. 2. 3. 4.

5. Zoom 20 Level off Return to glideslope (dive) Overspeed from dive OPEN CLB engages Aircraft climbs Preconditions for Scenarios Go Around (GA) altitude fixed at 3291 feet (as in SAL) Flaps Extension speed fixed at 226 knots (as in SAL) Level Off altitude and duration varied SC: Scenario AS: Automation Surprise 21 Preconditions for Scenarios

Go Around (GA) altitude fixed at 6000 feet Level Off altitude fixed at 7000 feet Level Off duration and Flaps Extension speed varied SC: Scenario AS: Automation Surprise 22 Conclusion Next Step: Simulation Model Checking + Implement capability for new scenarios into model checking + Make model checking model more detailed Scenario Narrative 24 Create Model & Specifications for Model Checking (SAL)

Analyze Using Model Checking (SAL) Analyze Using Simulation (WMC) Create Models & Metric Specifications for Simulation (WMC) Conclusion + Examined same scenario using both model checking and simulation + Simulation results show expansion of Model Checking results (more scenarios & comprises aircraft dynamics and time) + Method was shown how to use the two frameworks in conjunction to examine system behavior 25

Intro Auto Surp Platforms Method Model Checking Simulation Results Conclusion Questions & Comments Welcome Now 26

Recently Viewed Presentations

  • Microsoft Office 2007 PPTX CONTENTdm Favorites Document

    Microsoft Office 2007 PPTX CONTENTdm Favorites Document

    Microsoft Office 2007 PPTX CONTENTdm Favorites Document generated using PHP. ... -YO in full Indian dress on Rocky Boy Reservation, Montana. The boy wears leggings, moccasins, and a beaded chocker. He stands in front of a tipi. ... Microsoft Office...
  • SIFT A Literary Analysis Method

    SIFT A Literary Analysis Method

    (SIFT) Figures of Speech Analyze figurative language and other devices. Writers form images by using figures of speech such as simile, metaphors, hyperbole, and personification. Other devices can include: irony, allusion Simile A direct comparison of two things, usually using...
  • 投影片 1 - YunTech

    投影片 1 - YunTech

    A Benefit of Freshwater Fish to Our Environment 淡水魚與環保的關係 Speaker: Andrea Chen 05/19 Outline News Report Clips Question Vocabulary Benefit N. 利益/好處/優勢 Dengue 登革熱 (Dengue fever) Environmental protection 環保 (Green industry) Freshwater adj. 淡水的 (antonym: Saltwater ) Insecticide N. 殺蟲劑...
  • Red Mangrove - University of Arizona

    Red Mangrove - University of Arizona

    In the United States the red mangrove can be found along the Atlantic and Gulf coasts in the warmer areas Not found where there is a frost What are they good for… habitat for other organisms nursery for juvenile fish...
  • Introduction to Expert Choice - National Institutes of Health

    Introduction to Expert Choice - National Institutes of Health

    A consensus decision. Ultimately better and more justifiable decisions. Select the most important objectives from your PMP in the Learning and Growth perspective that you want to focus on in the main presentation. Then copy that row from your PMP...
  • Daily Oral Language - 8th Grade

    Daily Oral Language - 8th Grade

    Daily Oral Language Review Daily ... Oral Language 53. ms jackson stared at leslies messy desk in unbelief "of all the students in the eigth grade, she said, david is the less noisier" Day 53 - Daily Oral Language 53....
  • Academic Vocabulary: Imagery Write imagery in the term

    Academic Vocabulary: Imagery Write imagery in the term

    Personification - Complete an A.V. Frame. Take three minutes to. write down some . descriptions. of the the word . personification . in the descriptions box. These are YOUR OWN ideas, not someone else's, so DON'T TALK about them yet.
  • Revival History: Miracles, Signs and Wonders

    Revival History: Miracles, Signs and Wonders

    Moses and Aaron gathered the people. Gathering to hear the Word of God, unity is very important in revival. In Acts they were all in one accord in one place and prayed. All revivals have been accompanied by preaching the...