wiki:projects/rtembed
Last modified 18 months ago

jpf-rtembed

The rtembed extension is aimed at verification of Java programs for real-time and embedded platforms, such as RTSJ and SCJ.

Contact: Pavel Parizek, parizek at d3s.mff.cuni.cz

Features

Currently, the extension includes the following components:

  • implementation of a significant part of RTSJ API and its semantics (e.g., region-based memory model),
  • implementation of a significant part of SCJ API and its semantics (levels 0 and 1 are supported),
  • RTSJ-compliant scheduler based on thread priorities, periods and releases, and limited preemption,
  • abstraction of real time clock based on thread periods and numbers of past thread releases,
  • thread scheduling for SCJ and model of time based on WCET for bytecode instructions on the JOP processor ( http://www.jopdesign.com),
  • a listener that detects invalid usage of scoped memory areas (including private and mission memory areas in SCJ), and
  • a general optimization of state space traversal based on platform-specific restrictions of concurrency.

Related publications:

  • Pavel Parizek and Tomas Kalibera. Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs, In Proceedings of the 14th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), LNCS, vol. 5825, 2009.  http://d3s.mff.cuni.cz/~parizek/papers/fmics09.pdf
  • Tomas Kalibera, Pavel Parizek, Michal Malohlava, and Martin Schoeberl. Exhaustive Testing of Safety Critical Java, In Proceedings of the 8th International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES 2010), ACM, 2010.  http://d3s.mff.cuni.cz/~parizek/papers/jtres10.pdf

Running

The extension behavior can be configured via a number of properties. Value of the rtembed.scheduler.processors property states how many processors a platform has (i.e., how many threads can run in parallel). The rtembed.scheduler.timeslicing property states whether JPF should simulate a platform that employs time-preemption (time slicing), and the rtembed.scheduler.backbranches property specifies whether JPF should consider back-branches as thread yield points. Other properties are related to various aspects of RTSJ-compliant and/or SCJ-compliant scheduling and semantics.

Specifically, to run the extension in the RTSJ mode with scheduling algorithm based on release history and thread periods, you need to specify the following properties as a part of JPF configuration: 

+listener=gov.nasa.jpf.rtembed.memory.MemoryAreasChecker,\
        gov.nasa.jpf.rtembed.scheduling.SchedulingDataManager,\
        gov.nasa.jpf.rtembed.time.TimeDataManager
+vm.scheduler_factory.class=gov.nasa.jpf.rtembed.scheduling.RTSJSchedulerFactory
+vm.insn_factory.class=gov.nasa.jpf.rtembed.restrictpar.PlatformSpecificInstructionFactory
+rtembed.scheduler.processors=1
+rtembed.scheduler.timeslicing=false
+rtembed.scheduler.backbranches=false
+rtembed.scheduler.threadpriorities=true
+rtembed.scheduler.scopedmemaware=true
+rtembed.scheduler.priorityinheritance=true
+rtembed.scheduler.timemodel=true
+rtembed.scheduler.history=true
+rtembed.scheduler.boundoffsets=true
+rtembed.scheduler.maxoffsetms=10
+rtembed.scheduler.initrelease=2
+rtembed.scheduler.firstrelease=true

To run the extension in the SCJ mode, you need to provide the following configuration: 

+listener=gov.nasa.jpf.rtembed.memory.MemoryAreasChecker,\
        gov.nasa.jpf.rtembed.scheduling.SchedulingDataManager,\
        gov.nasa.jpf.rtembed.time.TimeDataManager
+vm.scheduler_factory.class=gov.nasa.jpf.rtembed.scheduling.SCJWCETSchedulerFactory
+vm.insn_factory.class=gov.nasa.jpf.rtembed.scheduling.SCJInstructionFactory
+rtembed.scheduler.processors=1
+rtembed.scheduler.timeslicing=false
+rtembed.scheduler.backbranches=false
+rtembed.scheduler.threadpriorities=true
+rtembed.scheduler.scopedmemaware=true
+rtembed.scheduler.priorityinheritance=true
+rtembed.scheduler.timemodel=true
+rtembed.timemodel.class=gov.nasa.jpf.rtembed.time.JopTiming
+rtembed.timemodel.cpufreq.mhz=40
+rtembed.timemodel.print=true
+rtembed.scheduler.gentcginsn=true

You also need to apply JPF on the javax.safetycritical.SCJRuntime class and pass the name of the main application class as an argument.

Repository

The Mercurial repository can be found on  http://babelfish.arc.nasa.gov/hg/jpf/jpf-rtembed