A JML/POSIX Filesystem

Participating in the Second Grand Challenge 6 Pilot Project: A Formally Verified Filesystem

  • Supervisor Dr. Joseph Kiniry
  • Subject Area Software Engineering
  • Pre-requisites Good knowledge of Java and basic knowledge of filesystems
  • Co-requisites (things you must learn along the way) Strong knowledge of POSIX filesystems, JML, and BON will be obtained during the course of this project
  • Subject Coverage Software Engineering for Reliable Systems, File Systems
  • Project Type Design and Implementation
  • Hardware/Software PC, laptop or workstation capable of running Java and Eclipse

Description

Some of this text is taken directly from the York ABZ conference web pages. Please see that site for more information.

The first VSR pilot project experiment took place during 2006. This project involved the successful mechanization of the verification of a commercially sanitized version of the first project to meet the high-assurance standard, ITSEC Level 6: the Mondex smart-card banking application. The original formal specification and design are publicly available, and the mechanization was accomplished by over a half dozen groups using different theories and tools. Their work is being recorded in a special issue of the Formal Aspects of Computing Journal.

In the first conference on Verified Software: Theories, Tools, and Experiments, held in Zurich in 2005, Joshi and Holzmann suggested a new pilot project for the grand challenge: the specification and verification of the POSIX file-store interface of Unix. This project involves a small subset of POSIX (which is detailed below) suitable for flash-memory hardware with strict fault-tolerant requirements to be used by forthcoming NASA's Jet Propulsion Laboratory missions.

The purpose of this project is to specify, implement, and verify a small part of the POSIX file-store interface in JML and Java. Previous work at York has specified the core aspects of this system in the Z specification language and in JML (primarily as a HashMap). This project will build upon that excellent work and we will collaborate with York on the results.

Mandatory Goals

  1. Gain familiarity with the BON specification language.
  2. Gain familiarity with JML, basic use of ESC/Java2, and the KOA system.
  3. Write BON specifications for the full POSIX filesystem, as stipulated by the pilot project's requirements.
  4. Write JML specifications for one facet of the POSIX filesystem pilot project (to be determined based upon student interest and skills, timing, etc.).
  5. Implement said facet using standard tools and practices of KindSoftware research group.

Discretionary Goals

  1. Enter system design and specification into GC6 pilot project and submit to the Verified Software Repository.

Exceptional Goals

  1. Write, submit, and publish a paper on the results.

Sources of Information and Preparatory Reading

  1. The ABZ POSIX file-store web site
  2. "A mini challenge: Build a verifiable filesystem" by R. Joshi and G. J. Holzmann. Published in FACS, volume 19, number 2, June 2007, and available via SpringerLink via UCD Library web site.
  3. The JML web site
  4. The ESC/Java2 web site
  5. Read the two recent papers available via the JML web page: "An overview of JML tools and applications" and "JML: notations and tools supporting detailed design in Java".
  6. Download, install, and play around with the JML tool suite and ESC/Java2 to get a feel for the technology.