Collective specification and verification of behavioral models and object-oriented implementations

Abstract. We present a finite-state-machine-based language, iFSM, to seamlessly integrate the behavioral logic and implementation strategies of object-oriented applications to prevent their design and implementa-tion from being out-of-sync. The language allows developers to focus on higher-level abstractions to support software analysis and design instead of focusing on language or architecture specific details. To support the language, we provide a transformation engine which automatically trans-lates iFSM specifications to lower-level C++/Java implementations of object-oriented classes. The auto-generated implementations from iFSM are similar in style to the manually written code, so that they are read-able and easily integrable with the existing code. Our experiments show that their performance is similarly comparable to that of manually writ-ten programs. We have automatically verified that these implementations are consistent with their behavioral models by translating iFSM specifi-cations into the input language of model checker NuSMV.