| This thesis presents a general purpose code transformation system, iFSM translation system, to translate high-level behavior specifications to low-level efficient implementations in C++ and Java. In particular, we have designed a finite-state-machine based language, iFSM, to collectively specify both the behavioral logic and the implementation details of general-purpose object-oriented classes so that the consistency between the software design and the implementation strategies can be automatically verified using model-checking techniques. We then use the iFSM translation system to automatically translate iFSM specifications to object-oriented implementations in C++/Java. Our experimental results confirm that the auto-generated class implementations are similar in style to the corresponding manually written classes and are comparable in performance as well. Finally, we use the iFSM translation system to automatically translate iFSM specifications to the input language of a model checker (NuSMV) and apply model-checking to verify that these class implementations are consistent with their behavioral models. |
