Abstract
Two barriers to the widespread industrialisation of formal methods are a lack of methodology, and the use of mathematical notations that are not easily understood by the non-specialist.
The work presented in this paper addresses these problems by defining diagrams which may be used to visualise aspects of formal specifications. The diagrams used are adaptations of classical approaches such as entity-relationship and state-transition diagrams.
The approach described imposes a methodology on the early stages of system specification, and provides the analyst with a choice of notations, visual and non-visual, while maintaining an underlying formality. During the process of analysis, the notation most appropriate for the expression and communication of the concepts required can be selected.
Two sorts of diagram are discussed: Entity-Structure Diagrams, and Operation-State Diagrams, the former in detail, the latter in sketch form.
A tool is envisaged that assists the analyst in moving between diagrams and VDM. Each diagram can be mapped onto parts of a common VDM specification, which forms the central underlying system description. Consistency can then be checked by a VDM type-checker.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. J. R. Back, Refinement Diagrams, In Proc. Fourth Refinement Workshop, Wolfson College, Cambridge, Jan 1991
R. D. van der Bos, L. M. G. Feijs, R. C. van Ommering, POLAR, A Picture-Oriented Language for Abstract Representations, Philips Research Laboratories, Research report No. RWR-113-RB-89021-RB, October 1989
G. Boudier, F. Gallo, R. Minot, I. Thomas, An Overview of PCTE and PCTE+, ACM Symposium on Software Development Environments 1988, pp. 248–257
British Standards Institute, The BSI/VDM Proto-Standard, Draft of 7 Sept 1990, Brian Richee (Ed.)
British Standards Institute, The Dynamic Semantics of the BSI/VDM Specification Language, Draft of August 1990, Peter Gorm Larsen (Ed.)
P. P. Chen, The Entity-Relationship Model: towards a unified view of data, ACM Transactions on Database Systems, Vol 1, No 1, March 1976
R. J. Cunningham, S. J. Goldsack, Why FOREST?, In Proc. of UK IT88, IEE, 1988, pp. 91–94
J. Dick, J. Loubersac, A Visual Approach to VDM: Entity-Structure Diagrams, Bull Research Center Report, DE/DRPA/DMA/91001, Jan 1991.
D. Harel, Statecharts: A visual formalism for complex systems, Sci. Comput. Programm. Vol. 8, pp. 231–274, 1987
Cliff B. Jones, Systematic Software Development using VDM, Second Edition, Prentice Hall Int., 1990
M. W. Maimone, J. D. Tygar, J. M. Wing, Formal Semantics for Visual Specification of Security, in Visual Languages and Visual Programming, Shi-Kuo Chang (Ed.), Plenum Publishing Corp., 1990
Maurice Naftalin, A Formal Framework for Opportunistic Design, Univ. of Stirling Tech. Report TR72, April 24 1991
Nico Plat, Jan van Katwijk, Kees Pronk, A Case for Structured Analysis/Formal Design, Submitted for publication.
Fiona Polack, Integrating Formal Notations and Systems Analysis: Using Entity Relationship Diagrams, University of York Research Report, SAZ 91/004, Feb. 27, 1991
Lesley Semmens, Pat Allen, Using Yourdon and Z: an Approach to Formal Specification, In Proc. 5th Z Users Group Meeting, December 1990, (to be published by Springer Verlag in Workshops in Computing Science.)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dick, J., Loubersac, J. (1991). Integrating structured and formal methods: A visual approach to VDM. In: van Lamsweerde, A., Fugetta, A. (eds) ESEC '91. ESEC 1991. Lecture Notes in Computer Science, vol 550. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540547428_42
Download citation
DOI: https://doi.org/10.1007/3540547428_42
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54742-6
Online ISBN: 978-3-540-46446-4
eBook Packages: Springer Book Archive