4L-7
An Approach to Model-Based Construction of Soft Real-Time Embedded Java Code
○Ilankaikone Senthooran,渡部卓雄(東工大)
Developing software for embedded real-time systems has become a challenge while
maintaining its functional requirements, such as timeliness, correctness, etc. Model-based
formal verification method is widely applied in the code development of real-time systems.
However, verification of such model only ensures the correctness of the model, not the
software of that system. We propose a method for generating Java code enabling soft
real-time feature, from a model verified by UPPAAL model checker, which is based on
Timed Automata. Thereby increasing confidence in the code, based on the notion of
correct-by-construction. Finally, we evaluate our method by applying it to non-trivial
real-time systems, including a maze-solver robot.