Abstract
SSD is an access control, which is part of a comprehensive security system developed by the Austrian Research Center Seibersdorf. SSD is being re-developed in a formal methods case study(cf Fig. 1). Since executable code has to be developed,
The Access Control and the Project Record of the Case Study.
a tool with an automatic code generator had to be chosen. VDMTools for VDM-SL is such a tool. When testing the specification, a test case indicating a contradiction in the requirements has been found. In order to achieve a better understanding of the nature of the contradiction, the theorem prover PVS has been used to formally prove properties of a certain aspect described by the requirements. The benefits of the PVS analysis include theorems which indicate inconsistencies in the requirements. Subsequently, linking VDM and PVS has been further investigated. There are VDM and PVS specifications which share the concept of events. However, they are used in a different manner in the two formalisms. Another aspect is using VDM for event-based systems.
Chapter PDF
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Droschl, G. (1999). Analyzing the requirements of an access control using VDMTools and PVS. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_61
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_61
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive