Exploring Java code generation based on formal specifications in RTPA

The use of formal specification techniques in developing large-scale software is considered as a necessary approach towards the implementation of efficient and reliable software systems. Barriers to the widespread adoption of formal methods in system development are attributed to the fact that many formal methods work only at the specification phase and it is still necessary to implement the code manually when specifications are ready. This paper explores the transformability between system specifications in real-time process algebra (RTPA) and code in Java. Automatic Java code generation on the basis of formal specifications in RTPA not only drastically reduce the effort and time spent in interpreting and translating the specifications by programmers, but also significantly improve the quality of code. Case studies on a number of real-world projects have shown the feasibility and efficiency of RTPA-based code generation methodology.