Extracting state machines from model-based formal specifications by focusing on data types

In software development, verification of the specifications and designs at the earlier stage of development is effective in reducing errors which occur at the later development stage. While there are many methods for verification of the specifications and designs, combining such methods in a systematic way enables us to analyze multi-aspect of the target system. In this paper, we discuss a systematic method to extract FSP models from a VDM-SL model. Our approach is to focus on the data types related to the functional property and trace the transition of the value of the variables whose data types are focused on.