# Presentation: 148680

## Monitoring IVHM Systems using a Monitor-Oriented Programming Framework

**S. Ghoshal, S. Manimaran - QSI**
**G. Rosu****, T. Serbanuta, G. Stefanescu - UIUC**

## IVHM System Analysis

- IVHM systems pose significantly higher safety and dependability requirements than most other systems
- Formal analysis of IVHM systems is therefore highly desirable ...
- ... but also challenging, due to their highly integrated nature (different technologies, hardware, software, sensors, etc.) and combined complexity

## Overview

- Our Approach
- MOP (University of Illinois at Urbana)
- TEAMS (Qualtech Systems Inc.)
- Project Research Plan
- Conclusion and Future Work

## Our Approach to IVHM Analysis 

- Our Approach to IVHM Analysis

- Separation of concerns
- State “health” assessment, or diagnosis
- Temporal behaviors of state sequences

- IVHM System

- Model-based
- observation

- TEAMS

- MOP

## Overview

- Our Approach
- MOP (University of Illinois at Urbana)
- TEAMS (Qualtech Systems Inc.)
- Project Research Plan
- Conclusion and Future Work

## Monitoring-Oriented Programming (MOP)http://fsl.cs.uiuc.edu/mop- proposed in 2003 –RV’03, ICFEM’04, RV’05, CAV’05, TACAS’05, CAV’06, CAV’07, OOPSLA’07, ICSE08, ...

## What is MOP?

- Framework for reliable software development
- Monitoring is basic design discipline
- ... rather than “add on” grafted onto existing code
- Recovery allowed and encouraged
- Provides to programmers and hides under the hood a large body of formal methods knowledge/techniques
- Monitor synthesis algorithms
- Generic for different languages and application domains

## Example: Correct and efficient sorting

- Works in MOP

## MOP Example: “Authentication before use”

- Execution 1, correct

- authenticate

- begin

- end

- use

- begin

- end

- Execution 2, incorrect

## MOP Example: “Authentication before use”

**class Resource {**
**/*@**
**  **_**class-scoped**_** SafeUse() {**
**      **_**event**_** authenticate : after(exec(* authenticate()))**
**      **_**event**_** use          : before(exec(* access()))**
**      **_**ptltl**_** ****: use -> <*> authenticate**
**  ****}**
**@*/**
**void authenticate() {...}**
**void access() {...}**
**...**
**}**

- MOP Example: “Authentication before use”

## MOP Example: “Enforce authentication before use”

- Execution 1, correct

- authenticate

- begin

- end

- use

- begin

- end

- Execution 2, incorrect but corrected

- Call authenticate()

## MOP Example: “Enforce authentication before use”

**class Resource {**
**/*@**
**  ****class-scoped SafeUse() {**
**      ****event**** authenticate : after(exec(* authenticate()))**
**      ****event**** use          : before(exec(* access()))**
**      ****ptltl**** : use -> <*> authenticate**
**      **_**violation**_** { **_**@this**_**.authenticate(); }**
**  ****}**
**@*/**
**void authenticate() {...}**
**void access() {...}**
**...**
**}**

- MOP Example: “Enforce authentication before use”

## MOP Example: “Correcting method matching”

**  ****class-scoped SafeClose() {**
**      ****event**** openRegKey  : after(exec(* openRegKey()))**
**      ****event**** closeHandle : before(exec(* closeHandle()))**
**      ****event**** closeRegKey : before(exec(* closeRegKey()))**
**      **_**ere**_** : any* openRegKey closeHandle**
**      **_**validation**_** {**
**        ****@this.closeRegKey();**
**        ****return;**
**      ****}**
**  ****}**
**@*/**

- Method **openRegKey** should be followed by **closeRegKey**, not by **closeHandle**

- MOP Example: “Correcting method matching”

**Notes:**
Manuvir Das 

## MOP Example: ProfilingHow many times a file is open, written to, and then closed?

**  ****class-scoped FileProfiling() {**
**      **_**[ int count = 0; int writes = 0;]**_
**      ****event**** open  : after(call(* open(..))) **_**{writes = 0;}**_
**      ****event**** write : after(call(* write(..))) **_**{writes ++;}**_
**      ****event**** close : after(call(* close(..)))**
**      ****ere**** : (open write+ close)***
**      ****violation**** { **_**@RESET**_**; }**
**      ****validation**** {**
**        ****count ++;**
**        ****File2.log(count + ": " + writes);**
**      ****}**
**  ****}**
**@*/**

- MOP Example: ProfilingHow many times a file is open, written to, and then closed?

## Fail Fast Iterators

**Vector v = new Vector();**
**v.add(new Integer(1));**
**Iterator**** i = v.****iterator****();**
**v.add(new Integer(2));**

- Following code throws exception in Java:

- No exception raised if one uses **Enumeration** instead of **Iterator**
- Java language decision, showing that  properties referring to sets of objects are important

## MOP Example:Safe Enumeration

- Basic safety property:
- If **nextElement()** invoked on an enumeration object, then the corresponding collection (vector) is not allowed to change after the creation of the enumeration object

## MOP Example:Safe Enumeration

**/*@**
_**global**_** **_**validation**_** SafeEnum(**_**Vector v, Enumeration+ e**_**) {**
** ****event**** create<v,e> :**
**             ****after(call(Enumeration+.new(v, ..))) returning e**
** ****event**** updatesource<v> : **
**             ****after(call(* v.add*(..))) \/ ...**
** ****event**** next<e> :**
**             ****before(call(Object e.nextElement()))**
** ****ere**** : create next* updatesource+ next)**
**}**
**@*/**

- MOP Example:Safe Enumeration

- AspectJ code generated from the above: ~700 LOC

## MOP Example:Safe Locking Policy

- Each lock should be released as many times as it was acquired

## MOP Example:Safe Locking

**/*@**
_**method-scoped**_** SafeLock(Lock l) {**
** ****event**** acquire<l> : before(call(* l.acquire()))**
** ****event**** release<l> : before(call(* l.release()))**
** **_**cfg**_** : S -> epsilon | S acquire S release**
**}**
**@*/**

- MOP Example:Safe Locking

## MOP Approach to Monitoring

- Keep the following distinct and generic:
-  specification formalisms
-  event definitions
-  validation handlers

## MOP Distinguished Features: Extensible logic framework 

- Observation: no silver-bullet logic for specs
- MOP logic plugins (the “How”): encapsulate monitor synthesizers; so far we have plugins for
- ERE (extended regular expressions), PtLTL (Past-time LTL), FtLTL (Future-time LTL), ATL (Allen temporal logic), JML (Java modeling language), PtCaRet (Past-time Call/Return), CFG (Context-free grammars)
- Generic universal parameters
- Allow monitor instances per groups of objects

**Notes:**
Not the task of mop to detect compilation

## MOP Distinguished Features: Configurable monitors

- Working scope
- Check point: check spec at defined place
- Method: within a method call
- Class: check spec everywhere during obj lifetime
- Interface: check spec at boundaries of methods
- Global: may refer to more than one object
- Running mode
- Inline: shares resources with application
- Outline: communicates with application via sockets
- Offline: generated monitor has random access to log

**Notes:**
Not the task of mop to detect compilation

## MOP Distinguished Features: Decentralized Monitoring/Indexing

*The problem*: how to monitor a universally quantified specification* efficiently*!

**create****<v,e>**
**udatesource****<v>**
**next****<e>**
**create next* updatesource+ next**

*(**** ***v,e***)** ***

## Decentralized Monitoring

- Monitor instances
- (one per parameter instance)

*M****p1*

*M****p2*

*M****p3*

*...   **M****p1000*

## Indexing ...

*The problem*: how can we retrieve all needed monitor instances efficiently?

**udatesource****<v>**

- Naïve implementation
- very inefficient (both time- and memory-wise)

## MOP’s Decentralized Indexing

- Monitors scattered all over the program
- Monitor states piggybacked to object states
- Weak references

- SafeEnum events
**create****<v,e>**
**udatesource****<v>**
**next****<e>**

## MOP: Evaluation

- More than 100 program-property pairs
- Dacapo benchmark, Tracematches benchmark, Eclipse, ...
- Overhead < 8% in most cases; close to hand-optimized

**Notes:**
Put some simplified table (only select a few rows or a few columns)

## MOP: Evaluation (cont.)

- Even significantly faster than logic specific solutions

## Overview

- Our Approach
- MOP (University of Illinois at Urbana)
- TEAMS (Qualtech Systems Inc.)
- Project Research Plan
- Conclusion and Future Work

## QSI’s TEAMS

- Model-based diagnosis system
- TEAMS model = dependency model capturing relationships: failure modes  observable effects
- QSI’s TEAMS Tool Set
- TEAMS Designer: help create models
- TEAMS-RT: processing data in real time
- TEAMATE:  infers health status + optimal tests
- TEAMS-RDS:  remote diagnostic server

## TEAMS Designer

- Help users create models
- (model can also be imported)
- Capture component and data dependency + other aspects that allow efficient diagnosis
- Model = hierarchical multi-layered directed graph
- Node: physical component
- Test-point: “observation” node
- Edge: cause-effect dependency

## Overview

- Our Approach
- MOP (University of Illinois at Urbana)
- TEAMS (Qualtech Systems Inc.)
- Project Research Plan
- Conclusion and Future Work

## Project Objectives

- Develop tools, techniques and ultimately an integrated framework for IVHM system monitoring, control and verification
- Show that runtime verification and monitoring can play a crucial role in the development of safe, robust, reliable, scalable and operational IVHM systems

## Project Plan

- TEAMS: capture system “health”
- MOP: generate and integrate monitors
- Integrated system: check IVHM system at runtime, steering if failures are detected

## What is done: TEAMS side Case study: B-737 Autoland 

- With data provided by Celeste M. Belcastro and Kenneth Eure, a model for B-737 is being developed

## What is done: MOP side Case study: B-737 Autoland 

- Two new logic plugins
- Context-free patterns
- Past-time LTL with Calls/Returns
- (still missing timed logic plugins)
- Improved monitor garbage collection
- Current MOP more than an order of magnitude faster than other RV systems

## Overview

- Our Approach
- MOP (University of Illinois at Urbana)
- TEAMS (Qualtech Systems Inc.)
- Project Research Plan
- Conclusion and Future Work

## Conclusion and Future Work

- Discussed initial steps towards integrated  framework for IVHM system monitoring, control and verification
- Separation of concerns
- Observation / diagnosis of system “health”
- Monitoring of temporal behaviours
- A lot to be done
- Complete TEAMS model for B-737 autoland
- Automate integration of TEAMS and MOP