Research On VDM-JML Mapping Mechanisms And Its Application In Software Development Process

In software engineering, it is a practical choice to use natural language to specify the system. For example, the tools for UML diagrams are common. However, natural language is not suitable for all kinds of systems because of its polymorphism, ambiguity and context-sensitiveness especially for complicated systems and high integrity software.On the opposite, formal language has many good features. Formal method uses the formal specification language to describe the software requirement, and make precise and unambiguous semantics to ensure the system is of correctness and maintainability. So it suits the industry use.Formal method can be classified as five approaches, of which one representative method is the Vienna Development Method (VDM). VDM is one of the most popular formal language used in software development, its mathematical approach allows unambiguous specification and development of high integrity software. A central element of VDM is its specification language VDM-SL.JML is a behavioral interface specification language tailored to Java(TM). It was derived from Eiffel of design-by-contract. And the JML-based tools of debugging, verifying and testing existing are mature.The paper analysis the two specification language: VDM-SL of high abstract level and JML lower abstract level. And it provides a mechanism mapping constant values, variable and constraints from VDM-SL to JML. In particular, the paper defines the mapping mechanisms of basic data types, collections, user-defined types, states, invariant, functions, operations and others. The solution facilitates the guidance between design and development which can make the flow of software life cycle continues and smooth.The paper proposes a tool called JML-SL_to_JML based on the mapping theories above. It is an Eclipse plug-in and it support automated transition mapping the VDM-SL notations to Java code annotated by JML. The java classes are to be fulfilled by programming developers. Referring to proof obligation, the tool uses the tools of JML to test the VDM-SL notations indirectly.By modeling from VDM-SL to JML, specifications can guide the subsequent software development more concretely, and makes it possible for the low design and test reflects the high level design absolutely. Through the iteration of phrases of software development, the software prototype is refined step by step like the screw model. In a conclusion, the mechanism of mapping from VDM-SL to JML combine the steps from analysis of natural language and specification with development and testing in series, to make the flow of software life cycle continues and smooth.