Schedulability Analysis Abstractions for Safety Critical Java

We present a compositional approach to schedulability analysis of safety-critical Java programs. We introduce a specification language in order to write abstract behavioural specifications regarding task execution-time and use of resources. Schedulability is checked on a model composed of the abstract specifications, possibly before any implementation, and as the specifications are implemented, these implementations can be checked individually. This means that library routines potentially can be separately checked and reused, and individual tasks can be verified according to their specifications without performing the full-system-analysis.