From Safety Critical Java Programs to Timed Process Models

The idea of analysing real programs by process algebraicmethods probably goes back to the Occam language using the CSPprocess algebra [43]. In [16,24] Degano et al. followed in that traditionby 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 subtlebugs that would otherwise be very hard to find. Inspired by the idea oftranslating real programs into process algebraic frameworks, we have inrecent years pursued an agenda of translating hard-real-time embeddedsafety critical programs written in the Safety Critical Java Profile [33]into networks of timed automata [4] and subjecting those to automatedanalysis using the UPPAAL model checker [10]. Several tools have beenbuilt and the tools have been used to analyse a number of systems forproperties such as worst case execution time, schedulability and energyoptimization [12–14,19,34,36,38]. In this paper we will elaborate on thetheoretical underpinning of the translation from Java programs to timedautomata models and briefly summarize some of the results based on thistranslation. Furthermore, we discuss future work, especially relations tothe work in [16,24] as Java recently has adopted first class higher orderfunctions in the form of lambda abstractions