From Safety Critical 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.