On the Integration of Formal Methods: Events and Scenarios in PVS and VDM

Abstract

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.

Conference

Publication date: July 1999

Publication date (Print): July 1999

Pages: 1-17

Affiliations

Austrian Research Center Seibersdorf

Seibersdorf, Austria

and

Institute for Software Technology, Technical University of Graz

Graz, Austria

Article

DOI: 10.14236/ewic/IWFM1999.4

Copyright statement: © Georg Droschl. Published by BCS Learning and Development Ltd. 3rd Irish Workshop on Formal Methods

License:

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/

Conference name: 3rd Irish Workshop on Formal Methods

Conference acronym: IWFM

Conference number: 3

Conference location: Galway, Ireland

Conference date: 1st - 2nd July 1999

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Formal Methods

Product

Product Information: 1477-9358BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/IWFM1999.4

Self URI (journal page): https://ewic.bcs.org/

Categories

Series title: Electronic Workshops in Computing