by Thomas Bøgholm, René R. Hansen, Anders P. Ravn, Hans Søndergaard, and Bent Thomsen
While embedded systems development is becoming increasingly complex due to demands for greater functionality and a shorter time to market, it is still using low-level, close to hardware, implementation languages. Modern languages like Java handle such complexities more elegantly, but issues with predictability hinder their adaptation in the embedded systems world. We have developed Predictable Java, a Java-based framework for safety-critical embedded systems, along with analysis tools based on formal modelling.
Embedded systems are everywhere, and are increasingly affecting our everyday life. Demands for shorter time to market, greater functionality and lower costs makes it difficult to develop these systems using traditional programming languages. Years ago, the traditional software industry shifted from low-level languages to modern languages with great success, increasing productivity significantly. Standard Java, however, is difficult to deploy and analyse in a real-time system setting. Java is based on a rather complex virtual machine, making analysis hard, and being object oriented, it has a very dynamic behaviour with almost unpredictable memory and time consumption. Additionally, Java is based on garbage collected memory, causing unforeseen interruptions which further complicates analyses.
We suggest that modern software engineering practices and languages be used in embedded systems software development by providing the required technology. The framework based on our Predictable Java profile provides the ability to express very complex systems in a simple, understandable and clear language which is recognizable and easily adaptable by most Java programmers.
Our tool SARTS (schedulability analsyser for real-time systems) is a schedulability analysis tool based on a formal model of timed automata, for proving schedulability of systems developed using our framework. This work is funded by DaNES (Danish Network for Intelligent Embedded Systems) and CISS (Center for Embedded Software Systems) at Aalborg University, and is publicly available.
In an attempt to reach the closest correspondence between actual running code and the properties being verified, SARTS works directly on the actual executed bytecode. This allows for a very close correspondence between the running system and the verified properties. For our prototype, we use the time-predictable Java processor, JOP, developed by Martin Schöberl at the Vienna University of Technology. This is an open and well-documented processor designed with predictability in mind.
The bytecode from the Java compiler is converted into a formal model, representing the real system, which is analysed in UPPAAL: a tool for modelling and verification of real-time systems.This approach provides a fully automatic process from code to verdict; developers need no training in formal verification, timed automata or UPPAAL.
Our technique provides a tight analysis by taking into consideration the control flow in the program code. This allows for analysing blocking, preemption and many of the dynamic features available in Java, which are considered hard to analyse, such as finalizers and dynamic method dispatch.
Figure 1: (left) A small snippet of a Java code verified using SARTS; (right) a simplified UPPAAL model of the highlighted code.
The Predictable Java framework provides a target for developing other analyses. We are designing the language profile as well as the analyses for the language profile. This enables us to fine-tune the developer framework in order to reach a reasonable compromise between restrictions and analyzability, making Java suited for safety-critical embedded systems.
Inspired by the techniques applied in SARTS, we are also developing memory consumption analysis, along with Eclipse IDE plugins that will assist programmers using the profile and profile conformance checker.
Links:
SARTS and Predictable Java: http://pj.cs.aau.dk
DaNES: http://danes.aau.dk
CISS: http://www.ciss.dk
UPPAAL tool: http://uppaal.com
Please contact:
Bent Thomsen
Aalborg University / DANAIM, Denmark
Tel: +45 9940 8897
E-mail:
