RTSJ in Java Pathfinder Project

Gary Lindstrom
Willem Visser
Peter C. Mehlitz

• Realtime Java home page
• Java Pathfinder home page

• Model Checking Real Time Java Using Java PathFinder, presented at ATVA 2005, Taipei, Taiwan, October 4-7, 2005.
• A Simulation Based Model Checker for Real Time Java, presented at JTRES OOPSLA workshop, October 17, 2005.
• Talk at NASA ARC RSE Group May 18, 2005 (pdf).

• System being modeled
  • A one-way bridge, which can hold at most one car at a time
  • Car i for 0..4
    • has priority i+1,
    • arrive at bridge at times 1, 13, 24, 34, 43.
  • Priority inheritance is in effect
    • see for example the increase of Car 3's priority (originally 4) when Car 4 (priority 5) is waiting for bridge
  • Pages 11-12 of this talk
• RTSJ classes used
  • AbsoluteTime,AsyncEvent,AsyncEventHandler,PeriodicTimer,PriorityParameters,RealtimeThread,RelativeTime, ReleaseParameters
• Java output
  • Deterministic
  • Nondeterministic (random selection among events with equal time)
• JPF output
  • Deterministic
  • Nondeterministic (all possible orders among events with equal time)
• Source code
  • Bridge, BridgeObserver, BridgeReporter,Car, CarArrivals, OneWayBridge

• Source
  • Asaf Degani's book Taming HAL
  • Pages 12-13 of this talk
• RTSJ classes used
  • AbsoluteTime,AsyncEvent,AsyncEventHandler,OneShotTimer,PriorityParameters,RealtimeThread,RelativeTime
• JPF output
  • Nondeterministic
• Source code
  • Airplane.java,ChangeFlaps.java,ChangeLandingGear.java,Pilot.java,TestAirplane.java, TestAltitude.java.

• System being modeled
  • Page 15 of this talk
  • Section 6.1 of this paper
• RTSJ classes used
  • PriorityParameters,RealtimeThread,RelativeTime
• Java output
  • FIFO CPU resource type
    • Deterministic
    • Pseudo random selection among events with equal time
  • Priority CPU resource type
    • Deterministic
    • Pseudo random selection among events with equal time
  • Priority ceiling CPU resource type (ceiling priority 6)
    • Deterministic
    • Pseudo random selection among events with equal time
  • Priority inheritance CPU resource type
    • Deterministic
    • Pseudo random selection among events with equal time
  • Preemptable CPU resource type
    • Deterministic
    • Pseudo random selection among events with equal time
• JPF output
  • FIFO CPU resource type
    • Deterministic
    • Pseudo random selection among events with equal time
    • Nondeterministic
  • Priority CPU resource type
    • Deterministic
    • Pseudo random selection among events with equal time
    • Nondeterministic
  • Priority ceiling CPU resource type (ceiling priority 6)
    • Deterministic
    • Pseudo random selection among events with equal time
    • Nondeterministic
  • Priority inheritance CPU resource type
    • Deterministic
    • Pseudo random selection among events with equal time
    • Nondeterministic
  • Preemptable CPU resource type
    • Deterministic
    • Pseudo random selection among events with equal time
    • Nondeterministic
• Source code
  • Job.java,Main.java

• System being modeled
  • Pages 16-21 of this talk
  • Section 6.2 of this paper
• RTSJ classes used
  • AsyncEventHandler,PriorityParameters,RealtimeThread,RelativeTime,ReleaseParameters
• Java output
  • FIFO intersection resource type
    • Deterministic
    • Pseudo random selection among events with equal time
  • Priority intersection resource type
    • Deterministic
    • Pseudo random selection among events with equal time
  • Priority ceiling intersection resource type (ceiling priority 8)
    • Deterministic
    • Pseudo random selection among events with equal time
  • Priority inheritance intersection resource type
    • Deterministic
    • Pseudo random selection among events with equal time
  • [Preemption intersection resource type does not make sense here!]
• JPF output
  • FIFO intersection resource type
    • Deterministic
    • Pseudo random selection among events with equal time
  • Priority intersection resource type
    • Deterministic
    • Pseudo random selection among events with equal time
  • Priority ceiling intersection resource type (ceiling priority 8)
    • Deterministic
    • Pseudo random selection among events with equal time
  • Priority inheritance intersection resource type
    • Deterministic
    • Pseudo random selection among events with equal time
• Source code
  • Car.java, Intersection.java, Main.java

• All classes implemented

Maintained by Gary Lindstrom. Last modified