VDMTools

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

VDMTools: advances in support for formal modeling in VDM
Full text	Pdf (276 KB)
Source	ACM SIGPLAN Notices archive Volume 43 , Issue 2 (February 2008) table of contents Pages 3-11 Year of Publication: 2008 ISSN:0362-1340
Publisher	ACM New York, NY, USA
Bibliometrics	Downloads (6 Weeks): 9, Downloads (12 Months): 65, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1361213.1361214 What is a DOI?

ABSTRACT

We describe the current status of "VDMTools", a group of tools supporting the analysis of system models expressed in the formal language of the Vienna Development Method. Three dialects of the language are supported: the ISO standard VDM specification language with support for modular structuring, the extension VDM++ which supports object-oriented structuring and concurrency, and a version extending VDM++ with features for modeling and analysing distributed embedded real-time systems. VDMTools provides extensive static semantics checking, automatic code generation, round-trip mapping to UML class diagrams, documentation support, test coverage analysis and debugging support. The tools' focus is on supporting the cost-effective development and exploitation of formal models in industrial settings. The paper presents the components of VDMTools and reports recent experience using them for the development of large models.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
	2	Michael Andersen, René Elmstrøm, Poul Bøgh Lassen, and Peter Gorm Larsen. Making Specifications Executable -- Using IPTES Meta-IV. Microprocessing and Microprogramming, 35(1--5):521--528, September 1992.
	3	Frédéric Badeau and Arnaud Amelot. Using B as a High Level Programming Language in an Industrial Project: Roissy VAL. In Z to B Conference / Nantes, pages 334--354, 2005.
	4	Bernhard K. Aichernig , Peter Gorm Larsen, A Proof Obligation Generator for VDM-SL, Proceedings of the 4th International Symposium of Formal Methods Europe on Industrial Applications and Strengthened Foundations of Formal Methods, p.338-357, September 15-19, 1997
	5	Juan C. Bicarregui , John S. Fitzgerald , Peter A. Lindsay , Richard Moore , Brian Ritchie, Proof in VDM: a practitioner's guide, Springer-Verlag New York, Inc., New York, NY, 1994
	6	Paulo Borba , Silvio Meira, From VDM specifications to functional prototypes, Journal of Systems and Software, v.21 n.3, p.267-278, June 1993 [doi>10.1016/0164-1212(93)90028-V]
	7	Paulo Borba , Silvio Meira, A system for translating executable VDM specifications into Lazy ML, Software—Practice & Experience, v.27 n.3, p.271-289, March 1997 [doi>10.1002/(SICI)1097-024X(199703)27:3<271::AID-SPE84>3.0.CO;2-T]
	8	Igor B. Bourdonov , Alexander Kossatchev , Victor V. Kuliamin , Alexandre Petrenko, UniTesK Test Suite Architecture, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods - Getting IT Right, p.77-88, July 22-24, 2002
	9	Jonathan P. Bowen , Michael G. Hinchey, Ten Commandments of Formal Methods, Computer, v.28 n.4, p.56-63, April 1995 [doi>10.1109/2.375178]
	10	Peter Breuer and Jonathan Bowen. Towards correct executable semantics for z. In J. P. Bowen and J. A. Hall, editors, Z User Workshop, pages 185--209. Springer-Verlag, 1994. Cambridge.
	11	T. M. Brookes , John S. Fitzgerald , Peter Gorm Larsen, Formal and Informal Specifications of a Secure System Component: Final Results in a Comparative Study, Proceedings of the Third International Symposium of Formal Methods Europe on Industrial Benefit and Advances in Formal Methods, p.214-227, March 18-22, 1996
	12	Edmund M. Clarke , Jeannette M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys (CSUR), v.28 n.4, p.626-643, Dec. 1996 [doi>10.1145/242223.242257]
	13	Tim Clement , Ian Cottam , Peter K. D. Froome , Claire Jones, The Development of a Commercial ``Shrink-Wrapped Application'' to Safety Integrity Level 2: The DUST-EXPERTTM Story, Proceedings of the 18th International Conference on Computer Computer Safety, Reliability and Security, p.216-225, September 01, 1999
	14	Susan Gerhardt Dan Craigen and Ted Ralston. An International Survey of Industrial Applications of Formal Methods, volume Volume 2 Case Studies. U.S. Department of Commerce, Technology Administration, National Institute of Standards and Technology, Computer Systems Laboratory, Gaithersburg, MD 20899, USA, March 1993.
	15	René Elmstrøm , Peter Gorm Larsen , Poul Bøgh Lassen, The IFAD VDM-SL toolbox: a practical approach to formal specifications, ACM SIGPLAN Notices, v.29 n.9, p.77-80, Sept. 1994 [doi>10.1145/185009.185028]
	16	J. S. Fitzgerald and P. G. Larsen. Balancing Insight and Effort: the Industrial Uptake of Formal Methods. In Cliff B. Jones, Zhiming Liu, and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, Essays in Honour of Dines Bjørner and Chaochen Zhou on the Occasion of Their 70th Birthdays, pages 237--254, Volume 4700, September 2007. Springer, Lecture Notes in Computer Science. ISBN 978-3-540-75220-2.
	17	John S. Fitzgerald , Simon Tjell , Peter Gorm Larsen , Marcel Verhoef, Validation Support for Distributed Real-Time Embedded Systems in VDM++, Proceedings of the 10th IEEE High Assurance Systems Engineering Symposium, p.331-340, November 14-16, 2007 [doi>10.1109/HASE.2007.76]
	18	John Fitzgerald , Peter Gorm Larsen , Paul Mukherjee , Nico Plat , Marcel Verhoef, Validated Designs For Object-oriented Systems, Springer-Verlag TELOS, Santa Clara, CA, 2005
	19	J. S. Fitzgerald and C. B. Jones. Proof in the Validation of a Formal Model of a Tracking System for a Nuclear Plant. In J. C. Bicarregui, editor, Proof in VDM: Case Studies, FACIT Series. Springer-Verlag, 1998.
	20	Brigitte Fröhlich. Towards Executability of Implicit Definitions. PhD thesis, TU Graz, Institute of Software Technology, September 1998.
	21	Brigitte Fröhlich , Peter Gorm Larsen, Combining VDM-SL Specifications with C++ Code, Proceedings of the Third International Symposium of Formal Methods Europe on Industrial Benefit and Advances in Formal Methods, p.179-194, March 18-22, 1996
	22	Norbert E. Fuchs, Specifications are (preferably) executable, Software Engineering Journal, v.7 n.5, p.323-334, Sept., 1992
	23	C. Ghezzi , D. Mandrioli , A. Morzenti, TRIO: A logic language for executable specifications of real-time systems, Journal of Systems and Software, v.12 n.2, p.107-123, May 1990 [doi>10.1016/0164-1212(90)90074-V]
	24	Anthony Hall, Seven Myths of Formal Methods, IEEE Software, v.7 n.5, p.11-19, September 1990 [doi>10.1109/52.57887]
	25	Ian Hayes , C. B. Jones, Specifications are not (necessarily) executable, Software Engineering Journal, v.4 n.6, p.330-338, Nov. 1989
	26	Cliff B. Jones, Systematic software development using VDM (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
	27	Aaron Kans , Clive Hayton, Using ABC to prototype VDM specifications, ACM SIGPLAN Notices, v.29 n.1, p.27-36, Jan. 1994 [doi>10.1145/181577.181582]
	28	Taro Kurita, Toyokazu Oota, and Yasumasa Nakatsugawa. Formal specification of an embedded IC for cellular phones. In Proceedings of Software Symposium 2005, pages 73--80. Software Engineers Associates of Japan, June 2005. (in Japanese).
	29	Peter Gorm Larsen. Ten Years of Historical Development: "Bootstrapping" VDMTools. Journal of Universal Computer Science, 7(8):692--709, 2001.
	30	Peter Gorm Larsen , John Fitzgerald , Tom Brookes, Applying Formal Specification in Industry, IEEE Software, v.13 n.3, p.48-56, May 1996 [doi>10.1109/52.493020]
	31	Peter Gorm Larsen, John S. Fitzgerald, and Steve Riddle. Learning by Doing: Practical Courses in Lightweight Formal Methods using VDM++. Technical Report CS-TR:992, School of Computing Science, Newcastle University, December 2006.
	32	Peter Gorm Larsen , Poul Bøgh Lassen, An Executable Subset of Meta-IV with Loose Specification, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.604-618, October 21-25, 1991
	33	Shaoying Liu , Hao Wang, An automated approach to specification animation for validation, Journal of Systems and Software, v.80 n.8, p.1271-1285, August, 2007 [doi>10.1016/j.jss.2006.12.540]
	34	Sun Microsystems. JavaDoc homepage. http://java.sun.com/j2se/javadoc/, 2007.
	35	Paul Mukherjee. Computer-aided Validation of Formal Specifications. Software Engineering Journal, pages 133--140, July 1995.
	36	Paul Mukherjee, Fabien Bousquet, Jerome Delabre, Stephen Paynter, and Peter Gorm Larsen. Exploring Timing Properties Using VDM++ on an Industrial Application. In J. C. Bicarregui and J. S. Fitzgerald, editors, Proceedings of the Second VDM Workshop, September 2000. Available at www.vdmportal.org.
	37	Overture-Core-Team. Overture Web site. http://www.overturetool.org, 2007.
	38	Overture Group. The VDM Portal. http://www.vdmportal.org, 2007.
	39	P. G. Larsen and B. S. Hansen and H. Brunn N. Plat and H. Toetenel and D. J. Andrews and J. Dawes and G. Parkin and others. Information technology -- Programming languages, their environments and system software interfaces -- Vienna Development Method -- Specification Language -- Part 1: Base language, December 1996.
	40	Nico Plat. The Industrial use of VDM++. In IEE Colloquium on Industrial Use of Formal Methods. IEE, May 1997.
	41	Armand Puccetti and Jean Yves Tixadou. Application of VDM-SL to the Development of the SPOT4 Programming Messages Generator. In John Fitzgerald and Peter Gorm Larsen, editors, VDM in Practice, pages 127--137, September 1999.
	42	Paul R. Smith and Peter Gorm Larsen. Applications of VDM in Banknote Processing. In John S. Fitzgerald and Peter Gorm Larsen, editors, VDM in Practice: Proc. First VDM Workshop 1999, September 1999. Available at www.vdmportal.org.
	43	Sunil Vadera, F. Meziane, and M. Huang. Experience with mural in formalising dust-expert. Information and Software Technology, 43:231--240, 2001.
	44	Samuel H. Valentine, Z--, an Executable Subset of Z, Proceedings of the Z User Workshop, p.157-187, December 16-17, 1991
	45	Marcel Verhoef and Peter Gorm Larsen. Interpreting Distributed System Architectures Using VDM++ -- A Case Study. In Brian Sauser and Gerrit Muller, editors, 5th Annual Conference on Systems Engineering Research, March 2007. Available at http://www.stevens.edu/engineering/cser/.
	46	Marcel Verhoef, Peter Gorm Larsen, and Jozef Hooman. Modeling and Validating Distributed Embedded Real-Time Systems with VDM++. In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors, FM 2006: Formal Methods, pages 147--162. Lecture Notes in Computer Science 4085, 2006.
	47	Sander Vermolen. Automatically Discharging VDM Proof Obligations using HOL. Master's thesis, Radboud University Nijmegen, Computer Science Department, August 2007.