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:
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