July 1999
3rd Irish Workshop on Formal Methods (IWFM)
Formal Methods
1st - 2nd July 1999
Tool support is known to be one of the success factors in formal specification based analysis and -program development. This paper investigates tool support in the context of a case study where a wide range of tool features is required: For an access control, C++ code has to be developed based on the user’s requirements expressed in natural language.
The access control has been classified a mixed data-control problem. This paper discusses (1) why VDMTools and PVS have been selected and (2) how they can be used together. Another aspect is the use of VDM as a framework for modeling event based systems. In our approach to tool integration, two specifications are considered to share a common part. For the present application this part consists of the scenario of all possible events.
This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/