ProgramVerificationEnvironmentExplanation

WikiInclude(ProgramVerificationEnvironmentDescription)

Overview

Many large software engineering projects have functional specifications that are thousands of pages long. These are usually written in a natural language, such as English, and with semi-formal notation such as diagrams and tables. There are often subtle ambiguities or internal contradictions within the software requirements, which are often not discovered until very late in the software development life cycle, simply because the project becomes too big for any one developer or analyst to fully understand and remember all the relevant details at the same time.

Popular high-level "modeling" languages in current use (e.g. UML) are not amenable to formal analysis because of a lack of semantics and interoperable tool support. Even so, high-level representations are compelling and useful in modern software engineering practice and software engineers regularly struggle with using these inadequate languages, even for mission critical applications.

The Mobius PVE is a customized version of the Eclipse platform that integrates a set of tools that support software development using state-of-the-art formal methods and software engineering techniques. The Mobius PVE supports the specification and verification of JML-annotated Java programs at the source code level as well as at the bytecode level using logic- and type-based techniques and the Proof-Carrying Code paradigm. The properties of particular interest include security (e.g. data is secret and never leaked) and resource guarantee properties (e.g. this method will never use more than this much memory or that much CPU) as well as total functional correctness. The Mobius PVE is thus, in a sense, a prototype realization of the U.K. Grand Challenge 6 Verifying Compiler, specialized to the domain of Java programs (HM05).

The Mobius PVE integrates theoretical and technical best-practices, leveraging the hard work of many research groups within, as well as outside of, the MOBIUS grant consortium. Many Java software engineers use the Eclipse development environment, together with plugins such as FindBugs and PMD. The Mobius PVE is bundled with Eclipse and these well-known third-party plugins so that Java developers are presented with a pre-configured development environment without the need to manually install each plugin.

For example, a Java developer might use the Mobius PVE to derive a JML specification from a high-level functional specification. The JML subsystem of the Mobius PVE might then be used to typecheck the JML specification, and, in a complementary fashion, the ESC/Java2 used look for inconsistencies in the specification. A variety of other pre-configured subsystems like CheckStyle, FindBugs, PMD, and others are executed asynchronously while the developer writes, modifies, and evolves their software architecture. Feedback about the completeness and quality of the system's documentation, formal specification, and program code are always at the developer's fingertips. Once the Java code has been verified against the JML specification, both statically using ESC/Java2 and dynamically using hand-written and automatically generated unit tests using JML's runtime assertion checking, then the developer has very high confidence that the requirements have been implemented correctly. At this stage, one performs automatic and interactive verification using the MOBIUS Direct VC Generator and Prover Editor, fully verifying functional and non-functional properties.