From Safety Critical Java']Java Programs to Timed Process Models

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] Degano et al. 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.