Skip to content

MobiusSubsystemsExplanation

Attila Sukosd edited this page Mar 15, 2013 · 9 revisions

The Mobius PVE is built on top of the Eclipse platform. The primary units of software within Eclipse are known as features, which are in turn composed of one or more plugins. We generally call these two kinds of units subsystems in Mobius PVE documentation.

The Mobius PVE is a customized version of Eclipse that contains over forty subsystems dedicated to reliable, dependable software development. Over half of these subsystems were implemented by MOBIUS partners.
More information on each subsystem is available via this Trac server, within publications related to specific tools cited appropriately, and from the original development team, in the case of externally developed tools.

Development on some of these subsystems (e.g. the static checker ESC/Java2) began before the project started, but their development continued within the project as their capabilities directly complemented the goals of the Mobius PVE. Other subsystems (e.g., the Umbra bytecode subsystem) were developed entirely within and for the MOBIUS project and the Mobius PVE.

There are two forms of subsystems: those (co-)developed by MOBIUS partners (known as "MOBIUS subsystems"), and those developed outside of MOBIUS (known as "non-MOBIUS subsystems"). Subsystems developed within MOBIUS are often discussed in more detail unless a non-MOBIUS subsystem has some special interaction with a MOBIUS one.

Some subsystems are exposed to the verification application developer via a programmatic API. Others are full-fledged Eclipse features'' and/or ''plugins. Many subsystems, even those that are plugins, also have rich command-line interfaces and are executed as normal processes.

In general, all MOBIUS subsystems written in Java (the majority of them) were developed with various version of the Mobius PVE itself. Moreover, some of them have full formal specifications and have been partially or fully validated (e.g., extensively unit tested) and/or verified (e.g., ESC/Java2 reports no errors) with the Mobius PVE. When a subsystem has one of these properties, it is highlighted in the text.

The source code, documentation, version control logs, and bug and feature tracking database of all subsystems is available via this Trac-based CDE. All subsystems developed within MOBIUS are Open Source and released under the GPLv2 or a BSD-style license.

Most of these subsystems are still under development and are evolving to match the needs of Mobius PVE users and MOBIUS partners and their research and industry collaborators.

Information about these components (their description, status, location in the source repository, etc.) is also summarized in the Components wiki page.

Many MOBIUS subsystems are developed by MOBIUS partners working in collaboration with non-MOBIUS researchers throughout North America and Europe.

Many subsystems have interdependencies, many of which grew organically over several years of development, as one plugin will depend upon the availability of another. In fact, teasing out, documenting, and formalizing these dependencies in plugin descriptors has been a main organizational effort in Mobius PVE development.

Broadly speaking, subsystems are organized into three dimensions. The first dimension is organized by language:

  • Java
  • Java Modeling Language (JML)
  • Java Bytecode
  • Bytecode Modeling Language (BML)
  • Coq

The second, by action:

  • Static Analyses
  • Abstract Syntax Trees (AST)

The third, by interface:

  • Application Programmer Interfaces
  • Backends
  • Interactive Plugins

Some subsystems lie along multiple facets of these dimensions. For example, many subsystems are interactive, but also have APIs. Others, tie together every facet. For example, in the case of ESC/Java2, it reasons about Java source code, bytecode, and JML, contains several different ASTs, provides several APIs, uses many backends, and finally, is also an interactive plugin.

Version: 9 Time: Tue Apr 1 16:06:55 2008 Author: dcochran (dcochran) IP: 193.1.132.32

Clone this wiki locally