Safety-Critical Java SCJ introduces a new programming paradigm for applications that must be certified. The SCJ specificationi¾?JSR 302 is an Open Group Standard, but it does not include verification techniques. Previous work has addressed verification for SCJ Leveli¾?1 programs. We support the much more complex SCJ Leveli¾?2 programs, which allows the programming of highly concurrent multi-processor applications with Java threads, and wait and notify mechanisms. We present a formal model of SCJ Leveli¾?2 that captures the state and behaviour of both SCJ programs and the SCJ API. This is the first formal semantics of the SCJ Leveli¾?2 paradigm and is an essential ingredient in the development of refinement-based reasoning techniques for SCJ Leveli¾?2 programs. We show how our models can be used to prove properties of the SCJ API and applications.
This is the first work supporting verification for SCJ Level 2 programs. K-Java @cite_11 models a subset of SE Java 1.4 and produces executable specifications for model checking. However, SCJ programs have features not included in SE Java. The authors of @cite_9 present a technique for translating SCJ programs into timed automata models. However, their technique appears to only be aimed at Levels 0 and 1. Further, neither of these techniques provide support for top-down refinement of SCJ Level 2 programs or refinement-based reasoning.
@cite_9 @cite_11
1919563168 2082036516
The idea of analysing real programs by process algebraic methods probably goes back to the Occam language using the CSP process algebra [43]. In [16, 24] followed in that tradition by analysing Mobile Agent Programs written in the Higher Order Functional, Concurrent and Distributed, programming language Facile [47], by equipping Facile with a process algebraic semantics based on true concurrency. This semantics facilitated analysis of programs revealing subtle bugs that would otherwise be very hard to find. Inspired by the idea of translating real programs into process algebraic frameworks, we have in recent years pursued an agenda of translating hard-real-time embedded safety critical programs written in the Safety Critical Java Profile [33] into networks of timed automata [4] and subjecting those to automated analysis using the UPPAAL model checker [10]. Several tools have been built and the tools have been used to analyse a number of systems for properties such as worst case execution time, schedulability and energy optimization [12---14, 19, 34, 36, 38]. In this paper we will elaborate on the theoretical underpinning of the translation from Java programs to timed automata models and briefly summarize some of the results based on this translation. Furthermore, we discuss future work, especially relations to the work in [16, 24] as Java recently has adopted first class higher order functions in the form of lambda abstractions. This paper presents K-Java, a complete executable formal semantics of Java 1.4. K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology. In order to maintain clarity while handling the great size of Java, the semantics was split into two separate definitions -- a static semantics and a dynamic semantics. The output of the static semantics is a preprocessed Java program, which is passed as input to the dynamic semantics for execution. The preprocessed program is a valid Java program, which uses a subset of the features of Java. The semantics is applied to model-check multi-threaded programs. Both the test suite and the static semantics are generic and ready to be used in other Java-related projects.