Technical Reports and Publications

External Publications

Modeling and Validating Distributed Embedded Real-Time Systems in VDM++, Marcel Verhoef, Peter Gorm Larsen and Jozef Hooman, in Jayadev Misra, Tobias Nipkow and Emil Sekerinski (Eds.), FM 2006: Formal Methods, Proc. 14th Intl. Symposium on Formal Methods, Lecture Notes in Computer Science 4085, Springer-Verlag, 2006, ISBN 3-540-37215-6. Slides.

Adding Syntax Error Repair to a Java-based Parser Generator, P. van der Spek, N. Plat and C. Pronk. ACM SIGPLAN Notices, 40(4):47-50. April 2005

Validated Designs for Object-oriented Systems. John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat and Marcel Verhoef. ISBN: 1-85233-881-4. Springer Verlag, New York. 2005. This is the seminal book about VDM++, the modelling language on which Overture is based. The book web site contains publication details and extensive support materials.

Technical Notes and Drafts

Interpreting Distributed System Architectures Using VDM++ - A Case Study. Marcel Verhoef, Peter Gorm Larsen. Accepted for the fifth Conference on System Engineering Research CSER (March 2007).

Third Overture Workshop, 27-28 November 2006, Newcastle University, Newcastle upon Tyne, UK

The following papers and presentations are as supplied by their authors. They have not been subject to peer review. If you have any queries about externally published materials based on these papers, please contact the authors directly.

A Review of the VDM-SL Static and Dynamic Semantics, Peter Gorm Larsen, IHA, Denmark:

• Static Semantics
• The Domain Universe
• Dynamic Semantics

Getting PROSPER Tool Support Usable Again (Slides) Peter Gorm Larsen, IHA, Denmark

What Next for VDMTools? Model Checking, Test Case Generation or Proof? (Slides) Shin Sahara, CSK Systems, Japan

Reinvigorating pen-and-paper Proofs in VDM: the pointfree approach (Slides) Jose N. Oliveira, University of Minho, Portugal

Proofs using SOS: support tooling (Slides) John Hughes and Cliff Jones, Newcastle University, UK

To be or not to be (LPF) (Slides) John Fitzgerald and Cliff Jones, Newcastle University, UK

Explicit vs. Implicit Polymorphism in OML (Slides) Thomas Christensen, University of Aarhus, Denmark

Future Proof Dynamic Semantics for Overture (Slides) Marcel Verhoef, CHESS and Radboud University Nijmegen, The Netherlands

Hybrid System Modeling in VDM (Slides) Marcel Verhoef

Recent Trends in O-o Modelling Languages JML, rCOS, CREDO (Slides) Bernhard Aichernig, Graz University of Technology, Austria

Overture Architecture & Status (Slides) Peter Gorm Larsen and Marcel Verhoef

Sex up Overture Tiago Alves,

Second Overture Workshop, 21 August 2006, McMaster University, Hamilton, Ontario, Canada

The following papers and presentations are as supplied by their authors. They have not been subject to peer review. If you have any queries about externally published materials based on these papers, please contact the authors directly.

Workshop programme. John S. Fitzgerald, Centre for Software Reliability (UK)

Separation of Context Concerns - Applying Aspect Orientation to VDM. Naoyasu Ubayashi (Kyushu Institute of Technology, JP) and Shin Nakajima (National Institute of Informatics, JP). Slides.

Overture status and improvements. Peter Gorm Larsen (Engineering College Aarhus, DK) and Marcel Verhoef (CHESS, NL).

Methods, Tools and Applications: VDM-related work at Newcastle. John S. Fitzgerald, Centre for Software Reliability (UK)

Extending VDMTools with Continuous Time Simulation. Marcel Verhoef (CHESS, NL), Peter Visser (Twente University, NL)

Current status of VDMTools. Shin Sahara, CSK Systems, Japan.

First Overture Workshop, 18 July 2005, Newcastle University, UK

The following papers and presentations are as supplied by their authors. They have not been subject to peer review. If you have an queries about externally published materials based on these papers, please contact the authors directly.

The draft papers from the workshop were released as a Newcastle Computing Science Technical Report:

Fitzgerald, J. S., Larsen, P. G., Plat, N. (eds.), Towards Next Generation Tools for VDM: Contributions to the First International Overture Workshop, Newcastle, July 2005, Technical Report CS-TR 969, School of Computing Science, Newcastle University, Jun 2006. Full Text PDF

Workshop programme.

Introduction to Overture. Peter Gorm Larsen and Nico Plat. Slides

Update on VDMTools. Shin Sahara.

Designing a Flexible Kernel providing VDM++ Support for Eclipse. Jacob Porsborg Nielsen and Jens Kielsgaard Hansen. Slides.

Grammar-centered Development of VDM Support. Tiago Alves and Joost Visser. Slides.

On The Use of VDM++ for Specifying Real-time Systems. Marcel Verhoef. Slides.

Camila Revival: VDM meets Haskell. Joost Visser, J. N. Oliveira, L. S. Barbosa, J. F. Ferreira and A. Mendes. Slides.

On the Value of Fault Injection on the Modeling Level. Bernhard K. Aichernig. Slides.

VDM++ versus Programming Language Extensions. Alexander Koptelov and Alexander Petrenko. Slides.

Results from the brainstorm session.

Theses and Student Project Reports

Development of an Overture/VDM++ Tool Set for Eclipse, Jacob Porsborg Nielsen and Jens Kielsgaard Hansen. MSc thesis. Technical University of Denmark, Department of Informatics and Mathematical Modelling, September 2005.

The Overture Project: Designing an open source tool set, Pieter van der Spek. MSc thesis. Department of Computer Science, Delft University of Technology, 2004.

The Overture Project: Towards an open source tool set. Pieter van der Spek. Research thesis. Department of Computer Science, Delft University of Technology, 2004.

Extending the VDM++ formal specification language with type inference and generic classes. Thomas Christensen. MSc thesis. Department of Computer Science, University of Århus, 2007.

-- JohnFitzgerald - 15 Jan 2007