Dalsgaard, Andreas E.3; Hansen, René Rydhof3; Schoeberl, Martin4
1 Department of Informatics and Mathematical Modeling, Technical University of Denmark2 Embedded Systems Engineering, Department of Informatics and Mathematical Modeling, Technical University of Denmark3 Aalborg University4 Department of Applied Mathematics and Computer Science, Technical University of Denmark
Safety-critical Java (SCJ) avoids garbage collection and uses a scope based memory model. This memory model is based on a restricted version of RTSJ  style scopes. The scopes form a clear hierarchy with different lifetimes. Therefore, references between objects in different scopes are only allowed from objects allocated in scopes with a shorter lifetime to objects allocated in scopes with a longer lifetime. To ensure memory safety, programmers are required to either manually annotate the application with complex annotations, rely on a runtime test of each reference assignment, or statically analyze all reference assignments and avoid runtime checks when all assignments are proven to be correct. A violation of the assignment rule at runtime leads to an unchecked exception. For safety-critical code that needs to be certified, runtime exceptions must be avoided and the absence of illegal reference assignments needs to be proven. In this paper we present a static program analysis tool that automates the proof that no illegal assignments occur.
Proceedings of the 10th International Workshop on Java Technologies for Real-time and Embedded Systems (jtres 2012), 2012, p. 9-17
Main Research Area:
International Workshop of Java Technologies for Real-time and Embedded Systems. Proceedings
10th International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES 2012)International workshop on Java technologies for real-time and embedded systems