Combining VDM-SL specifications with C++ code

Abstract

Experience shows that it is not economically feasible to formally specify all parts of a system in an industrial application. Either one already has a number of existing components which are trusted and therefore desirable for reuse, or components are so simple that there is no gain in formally specifying their behavior. In both cases it may be felt that it is not worth spending time on developing a detailed formal specification of the entire system. This raises the question what tools should be provided for the analysis of the entire system in which actual code is combined with specifications. In this paper we propose an approach which enables integration of code into a formal specification for prototyping facilities. The integration of code is supported by an extension to the IFAD VDM-SL Toolbox such that heterogeneous models can be interpreted.