Transformation of the Ravenscar Profile Based Ada Real-time Application to the Verification-ready Statecharts: Reverse Engineering and Statemate approach.
Chang‐Jin Kim, Jin‐Young Choi · 2006
The Ravenscar Profile is a subset of Ada95 tasking model which removes the Ada’s unsafe real-time characteristics and allows high-integrity of system. By the Ravenscar Profile, Ada95 can meet the determinism on system behavior. It also allows schedulability analysis and formal verification on the concurrent model of system. But the formal verification may be additional hard works to improve value of the Ravenscar Profile. In this paper, we present the transformation of Ravenscar programs to statecharts model by reverse engineering techniques, which allows the statecharts to be used for program analysis and formal verification. The advantage of these works is transforming the Ada application code into the verification-ready statecharts with ease and simple way than general formal methods approach. We used STI’s