WP3Notes

TOC

WP3: Program Verification Environment (PVE)

Notes on the current state of the PVE, our testing, packaging, and shipping process and struggles (up to 20 minutes => 10 slides)

Slide 1: Introduction to the PVE

• Integrated tool set built on Eclipse IDE and JML infrastructure (JML4 is also built on Eclipse)
• Each subsystem of Mobius is also a complete software package in itself e.g. ESC/Java2

Slide 2: Architecture of the PVE

• Subsystems are categorized across three dimensions:
  • Language: BON, BPL, ByteCode, BML, Coq, Java 1.4, Java 1.5, Java 6, JavaCard, JML, Verification Conditions
  • Action: Static Analysis, Abstract Syntax Trees, Transformation (e.g. from BML to BPL)
  • Interface: command line interface, front-end API, back-end (e.g. theorem provers), interactive plug-ins, user interface
• Subsystems developed (newly built, extended or renovated) by MOBIUS partners are described as the components of the PVE
• MOBIUS components can also run standalone e.g. from the command line, for isolated testing and debugging

Slide 3: Interaction between Components

• PVE components communicate each other using a shared language and interface

  • Example: Extended Static Checking of Java with JML annotations
    • JavaFE: Java/JML -> AST
    • ESC/Java2: AST -> VC
    • Simplify: VC -> Success/Fail
    • Logging: Success/Fail -> Eclipse warnings
    • ESC plugin: adds markers to the code

• Investigating the possibility of a Distributed PVE e.g. running the backend subsystems on remote servers

Slide 4: Distribution Testing of the PVE

• Maven

  • An extensible replacement for Ant which can be customised with its own plugins
  • Project Object Model (POM) to describe build and test process
  • Tests need to be wrapped in a JUnit test suite
  • Some ESC/Java2 tests are already wrapped in JUnit, other legacy tests are being converted

• Hudson Continuous Integration Engine

  • An extensible version of Maven Continuum with its own plugins
  • More stable than Maven Continuum but also works with Maven
  • Provides RSS feeds and e-mails for test results
  • Allows distributed builds using SSH and Maven, Ant or shell scripts
  • More configurable than Continuum; can be used to run remote Makefiles, for example
  • One or more builds are triggered each time a change is committed to subversion
  • Very large test suites can be distributed between several servers
  • See http://voting.ucd.ie:8080

• This is work-in-progress; we are still configuring the test framework; no useful results yet

Slide 5: Operating Environments being used for Continuous Testing

• Mac OS X 10.5 (Leopard) on Intel hardware
• Mac OS X 10.4 (Tiger) on PowerPC
• Linux
• Solaris

Slide 6: Release Modes

PVE components are released in various modes:

• Standalone releases of components as command line tools
• Standalone releases of components as Eclipse plugins
• Eclipse bookmarks with URLs for update sites of all plugins
• Eclipse team project set with subversion URLS for all MOBIUS projects
• Full release of Mobius PVE integrated with latest release of Eclipse/JML4
  • Eclipse Workspace for MOBIUS developers with subversion URLs
  • Eclipse Workspace for MOBIUS users with examples and tests

Slide 7: Supported Operating Environments

PVE components are shipped in three major operating environments, to ensure that there are no platform specific dependencies i.e. that the PVE is platform independent (it depends only on Java, Eclipse and JML).

• Mac OS X (Universal Binary)
• Linux (32-bit)
• Windows XP/Vista (minimal testing/support only)

We don't have enough resources or bandwidth to support other operating environments or to fully support and test Windows environments. We depend on users of other operating environments to build and test the PVE for us.

Slide 8: Documentation and the Mobius Tools Wiki

• Each component has its own internal documentation
• Each component also has its own wiki page e.g. https://mobius.ucd.ie/wiki/Umbra
• Each wiki page contains links to:
  • Tickets
  • Milestones
  • Status
  • Recent Changes
  • Location within Repository
  • Related wiki pages
  • External URLs
  • Releases
  • Home page i.e. where to get further information

Slide 9: Software Reuse

• Building Restoration as a metaphor
• We want to preserve the best original features of ESC/Java2
• Existing users of ESC/Java2 should be able to make a seamless transition to using the MOBIUS PVE
• Avoid unnecessary changes to the user interface or APIs
• MOBIUS components could be re-used within other systems and projects

Slide 10: Summary, Conclusion and Questions

• Tightly integrated but loosely coupled; components can be run standalone
• Components can be distributed between servers e.g. using SSH public keys
• Using Maven and Hudson to manage distributed testing of the PVE

Version: 22 Time: Tue Jun 3 18:32:27 2008 Author: dcochran (dcochran) IP: 78.152.239.200