Peter Gorm Larsen
Nick Battle
Skip Abstract Section
Abstract
Overture is a community-based initiative that aims to develop a common open-source platform integrating a range of tools for constructing and analysing formal models of systems using VDM. The mission is to both provide an industrial-strength tool set for VDM and also to provide an environment that allows researchers and other stakeholders to experiment with modifications and extensions to the tools and language. This paper presents the current status and future vision of the Overture project.
- Sten Agerholm and Jacob Frost. Towards an integrated case and theorem proving tool for vdm-sl. In John Fitzgerald, Cliff B. Jones, and Peter Lucas, editors, FME'97: Industrial Applications and Strengthened Foundations of Formal Methods (Proc. 4th Intl. Symposium of Formal Methods Europe, Graz, Austria, September 1997), volume 1313 of Lecture Notes in Computer Science, pages 278--297. Springer-Verlag, September 1997. ISBN 3-540-63533-5. Google Scholar
Digital Library
- Nick Battle. VDMJ User Guide. Technical report, Fujitsu Services Ltd., UK, 2009.Google Scholar
- Bernhard K. Aichernig and Peter Gorm Larsen. A Proof Obligation Generator for VDM-SL. In John S. Fitzgerald, Cliff B. Jones, and Peter Lucas, editors, FME'97: Industrial Applications and Strengthened Foundations of Formal Methods (Proc. 4th Intl. Symposium of Formal Methods Europe, Graz, Austria, September 1997), volume 1313 of Lecture Notes in Computer Science, pages 338--357. Springer-Verlag, September 1997. ISBN 3-540-63533-5. Google ScholarDigital Library
- René Elmstrøm, Peter Gorm Larsen, and Poul Bøgh Lassen. The IFAD VDM-SL Toolbox: A Practical Approach to Formal Specifications. ACM Sigplan Notices, 29(9):77--80, September 1994. Google ScholarDigital Library
- J.S. Fitzgerald and P.G. Larsen. Triumphs and Challenges for the Industrial Application of Model-Oriented Formal Methods. In T. Margaria, A. Philippou, and B. Steffen, editors, Proc. 2nd Intl. Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2007), 2007. Also Technical Report CS-TR-999, School of Computing Science, Newcastle University. Google ScholarDigital Library
- John Fitzgerald and Peter Gorm Larsen. Modelling Systems -- Practical Tools and Techniques in Software Development. Cambridge University Press, The Edinburgh Building, Cambridge CB2 2RU, UK, Second edition, 2009. ISBN 0-521-62348-0. Google ScholarDigital Library
- John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat, and Marcel Verhoef. Validated Designs for Object{oriented Systems. Springer, New York, 2005. Google ScholarDigital Library
- John Fitzgerald, Peter Gorm Larsen, and Shin Sahara. VDMTools: Advances in Support for Formal Modeling in VDM. Sigplan Notices, 43(2):3--11, February 2008. Google ScholarDigital Library
- J.S. Fitzgerald, P.G. Larsen, S. Tjell, and M. Verhoef. Validation Support for Real-Time Embedded Systems in VDM++. In Bojan Cukic and Jing Dong, editors, Proc. HASE 2007: 10th IEEE High Assurance Systems Engineering Symposium, pages 331--340. IEEE, November 2007. Google ScholarDigital Library
- Daniel Jackson. Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol., 11(2):256--290, 2002. Google ScholarDigital Library
- Cliff B. Jones. Scientific Decisions which Characterize VDM. In J.M. Wing, J.C.P. Woodcock, and J. Davies, editors, FM'99 - Formal Methods, pages 28--47. Springer-Verlag, 1999. Lecture Notes in Computer Science 1708. Google ScholarDigital Library
- Gary T. Leavens and Yoonsik Cheon. Design by Contract with JML. Draft, available from jmlspecs.org., 2005.Google Scholar
- P.G. Larsen, B.S. Hansen, et al. Information technology -- Programming languages, their environments and system software interfaces -- Vienna Development Method -- Specification Language -- Part 1: Base language, December 1996. International Standard ISO/IEC 13817-1.Google Scholar
- Peter Gorm Larsen, Kenneth Lausdahl, and Nick Battle. Combinatorial Testing for VDM++. In Submitted for publication, July 2009.Google Scholar
- Kenneth Lausdahl, Hans Kristian Agerlund Lintrup, and Peter Gorm Larsen. Connecting UML and VDM++ with Open Tool Support. In Formal Methods 09, November 2009. Google ScholarDigital Library
- Paul Mukherjee, Fabien Bousquet, Jérôme 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.Google Scholar
- David Holst Møller and Christian Rane Paysen Thillermann. Using Eclipse for Exploring an Integration Architecture for VDM. Master's thesis, Aarhus University/Engineering College of Aarhus, June 2009.Google Scholar
- Augusto Ribeiro. An Extended Proof Obligation Generator for VDM++/OML. Master's thesis, Minho University with exchange to Engineering College of Arhus, July 2008.Google Scholar
- Adriana Sucena Santos. VDM++ Test Automation Support. Master's thesis, Minho University with exchange to Engineering College of Arhus, July 2008.Google Scholar
- Sander Vermolen. Automatically Discharging VDM Proof Obligations using HOL. Master's thesis, Radboud University Nijmegen, Computer Science Department, August 2007.Google Scholar
- Marcel Verhoef. Modeling and Validating Distributed Embedded Real-Time Control Systems. PhD thesis, Radboud University Nijmegen, 2008. ISBN 978-90-9023705-3.Google Scholar
- 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. Google ScholarDigital Library
- Marcel Verhoef, Peter Visser, Jozef Hooman, and Jan Broenink. Co-simulation of Real-time Embedded Control Systems. In Jim Davies and Jeremy Gibbons, editors, Integrated Formal Methods: Proc. 6th. Intl. Conference, Lecture Notes in Computer Science 4591, pages 639--658. Springer-Verlag, July 2007. Google ScholarDigital Library
- Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John Fitzgerald. Formal Methods: Practice and Experience. ACM Computing Surveys, 41(4):1--36, 2009. Google ScholarDigital Library
Recommendations
CASE tools: understanding the reasons for non-use
Computer-Aided Software Engineering (CASE) technologies are tools that provide automated assistance for software development [3]. The goal of introducing CASE tools is the reduction of the time and cost of software development and the enhancement of the ...
The IFAD VDM Tools: Lightweight Formal Methods
FM-Trends 98: Proceedings of the International Workshop on Current Trends in Applied Formal Method: Applied Formal MethodsThe services and tools supporting the ISO Standard VDMSL notation and its object-oriented extension VDM++ are commonly known as the VDM Technology. For both notations the company IFAD provides leading edge technology tools, training and consultcincy. ...
Making active CASE tools—toward the next generation CASE tools
In CASE field, there is a long-standing topic, i.e. the reason that CASE tools seem to be dearly bought but sparsely used. Based on our practical experience of making and using CASE tools, we point out the reason is that today's CASE tools are actually ...
Comments