Verification-centric Software Engineering
A GLOBAN Summer School Course
Date: 22-23 September 2008
Location: Institute of Informatics, University of Warsaw, Warsaw, Poland
Instructor: Joe Kiniry
Tutorial materials prepared with the able assistance of: David Cok, Fintan Fairmichael, Gary Leavens, Erik Poll, and Dan Zimmerman
Abstract
This series of talks focus on the practical aspects of designing, constructing, and validating global computing software systems. A suite of robust academic tools, many of which were developed under the EU FP6 MOBIUS project, which are part of the MOBIUS Program Verification Environment (PVE), are summarized and demonstrated.
The first talk gives an overview of the tools options available today, including tools used in this series of talks and others. The second talk focuses on the practical aspects of designing systems for verification. The third talk focuses on refining designs into implementations and validating those designs and refinements via various static checking techniques and automated testing. The final talk focuses on using interactive and automatic theorem provers to perform full functional verification.
Participants are given the latest release of the MOBIUS PVE and other related tools on a CD-ROM or USB key.
Attendee Background
Any Java programmer who wishes to improve the quality of their software should attend. Also, educators who want to use BON, JML, and/or ESC/Java2 in teaching, as a gentle way to introduce students to state-of-the-art specification and verification techniques and tools supporting formal methods, should also attend this tutorial.
Objectives
Attendees will come out of this tutorial with a firm understanding of the use of specifications in software design and engineering, a basic knowledge of the BON and JML specification languages, and will be knowledgeable about the various tools available for the BON and JML languages, particularly BONc and ESC/Java2.
Tutorial History
Variations of this tutorial have been presented to over a hundred academics and several hundred undergraduate and postgraduate students over the past several years. The first version of this tutorial was one of the most successful tutorials at ECOOP 2004. Extensive slides, homework assignments, and an ongoing book on JML and ESC/Java2 are available. Alternate versions of this tutorial have also been given at several other top academic conferences, including ECOOP, ETAPS, FM, TOOLS, and FMCO.
Biography
Joseph Kiniry, University College Dublin
Joe is a lecturer in the School of Computer Science and Informatics at
University College Dublin. He was previously in the SoS Group at
Radboud University Nijmegen. He earned his Ph.D. in Computer Science
from the California Institute of Technology. Joe is the coauthor of
ESC/Java2 and has contributed to, or led the development of, several
other verification tools including
BONc,
FreeBoogie,
Simplify,
Fx7,
the JML tool suite,
PVS,
the LOOP compiler, and, of course,
the Mobius PVE.
Registration
Please see the main GLOBAN website for how to register for the Summer School.
Slides
The slides presented in this tutorial are here:
- The Mobius Program Verification Environment (slide set 1)
- Verification-centric Software Development with BON, JML, and ESC/Java2
Exam
The exam for this course is included in the following workspace in the project named GLOBAN. This workspace also includes many of the examples discussed in the GLOBAN slides and in past tutorials.
Resources
The following resources are available for all interested in JML and ESC/Java, whether you decide to attend our tutorial or not.
- Primary Tools for the Tutorial
- The Mobius Program Verification Environment (PVE):
https://www.kindsoftware.com/products/opensource/Mobius/
- The BONc tool suite:
https://www.kindsoftware.com/products/opensource/BONc/
- ESC/Java2:
https://www.kindsoftware.com/products/opensource/ESCJava2/
- The JML tool suite:
https://www.jmlspecs.org/
- The Mobius Program Verification Environment (PVE):
- Papers
- The Mobius PVE is described on the Mobius Tools Trac site located at https://oss.itu.dk/trac/mobius/.
- For a good overview of JML and the tools available, read An Overview of JML Tools and Applications
- For background, history, and motivations of the design of JML, see JML: Notations and Tools Supporting Detailed Design in Java
- For an overview of using JML to support Design by Contract in Java, see Design by Contract with JML
- Many other papers on JML and related tools are available via the JML papers web page.
- Slides from Past Tutorials
- Verification-centric Software Development in Java with BON, JML, and ESC/Java2
- A JML Tutorial Modular Specification and Verification of Functional Behavior for Java
- Introduction to JML (4 up)
- ESC/Java2: Use and Features (4 up)
- ESC/Java2 Warnings (4up)
- Specification Tips and Pitfalls (4 up)
- Advanced JML (and more Tips and Pitfalls) (4 up)
- ESC/Java: Extended Static Checking for Java (a summary and non-interactive demonstration)
- Effectively Using JML: Software Engineering Processes incorporating Formal Specification
- Using ESC/Java2 Architecture, Hints, and Tricks
- Using Formal Methods for VLSI Development: Using Java and JML in the Real World
- Models are the `M' in JML: Using ADT Models in Formal Specification with JML
- The ESC/Java2 Calculi and Object Logics: Implications on Specification and Verification
- Homework
- JML and ESC/Java Homework Exercises (learning JML and ESC/Java2 through hands-on work)