Monitoring and Runtime Checking Demo Application

The elevator example showcases the important mechanics of Monitoring and Runtime Checking . For this we have created a toy application "The Two Elevators of the Tower of Penn" . The MAC snoops the elevator application and checks for response time violations. The definition of a response time violation is " Suppose a user requests an elevator ,if the elevator does not service that user within a specified amount of time , it is flagged as a response time violation ." A more realistic analogy can be used at a hospital where emergency elevators servicing casualties must provide service within a specified time constraint . Another can be that of a high rise office building like the "Empire State " to service hundreds of passengers efficiently and in minimal amount of time.

Some of the interesting features of this application are :

1. Building floors are parameterized
   10 storey building 5 storey building
2. Control the time it takes for an elevator to move from floor to floor
3. Control the time it takes for the elevator to open doors
4. Control the time it takes for the elevator to close doors
5. Control the wait time for passengers to board

This opens endless possibilities to tweak and analyze the behavior of an elevator application . Surely you can also simulate the "Empire State " having 120 floors (The only constraint is your monitor screen) , two elevators which move at the speed of 2 floors per second ,


System Components and algorithm

• Each elevator has three request queues associated with it.
• UP QUEUE: If the elevator is moving up and if the request floor >= current elevator floor and request floor direction ="UP" or If the elevator is moving up and if the request floor >= current elevator floor and request floor direction ="DoWN"
• DOWN QUEUE:If the elevator is moving down and if the request floor < current elevator floor and request floor direction="Down" or If the elevator is moving down and if the request floor < current elevator floor and request floor direction="Up"
• UP DOWN QUEUE:If the elevator is moving down and if the request floor direction ="UP" and request floor> current elevator floor and or If the elevator is moving up and if the request floor < current elevator floor and request floor direction="DOWn"

How it Works

1. The two elevators start in their initial position,the first elevator starts at the ground floor, the second elevator starts at the top floor
2. Users start requesting the elevator pressing either the "UP" or "DOWN" button

Inorder for the elevator application to be monitored we need to define the formal specification of the elevator . In the MAC world this formal specification is defined using the Elevator MEDL.
The elevator application has been developed using Java . In order to map the implementation specifics with the formal specification we also define the PEDL which is a mapping of the implementation to the formal specification . The Elevator PEDL is parsed by the MAC compiler and produces the instrumentor.out and the pedl.out


Instrumentation & Filter
The instrumentator accepts the instrumentator.out and injects filtering code inside the byte code of the target application .

Event Recognizer & Checker
The event recognizer consumes the pedl.out and accepts filtering events from the target application and transforms them to a high level event definitions and then forwards them to the Checker which in turn consumes the medl.out as well as high level events from the event recognizer and evaluates the condition tree to assure that the application complies with the formal specifiaction.