FormalMethodsMission

Mission Statement and Plan for "Formal Methods" Fedora SIG

This document defines a mission statement and plan of action for a proposed "Formal Methods" Fedora SIG, per the Defining projects page.

Introduction

"Formal methods" are techniques that use mathematics to prove that models of software, hardware, or systems will or will not have certain behavior. To be practical, they must be automated using tools. Free/Libre/Open Source Software (FLOSS) formal methods tools are now available, including automated theorem provers and model-checkers, but the tools can be difficult to install and apply.

Goal and Scope

The goal of the Formal Methods SIG is to make it easy to install formal methods tools in Fedora, ease learning how to apply them, encourage the development of "open proofs" (where an implementation, proofs, and required tools are all FLOSS), and to provide feedback to toolmakers so that the tools in Fedora can become more powerful, more scaleable, and easier to use together.

Mission Statement

Who the new project would serve?

The project would serve anyone interested in proving that certain software, hardware, or systems always have (or do not have) certain behaviors, as well as educators/researchers interested in teaching/improving these techniques.

Who will lead the project?

David A. Wheeler and Jerry James will co-lead the project.

What the goals and scope of the new project would be?

See the "goal and scope" statement above.

When can the project be considered a success?

The project is a success when people start proving models of implementations have or do not have certain behaviors, using tools packaged by this SIG.

Where the project will lead and where it will fit into the Fedora Project?

It will lead to many formal methods tools being packaged into the Fedora repository (some have already been done). The intent is that 'yum groupinstall "Formal methods"' will install this suite all at once. Soon afterward, we hope to create a "Formal methods Fedora Spin" based on that group which would make it easy for anyone to try out this suite of tools.

Why does this warrant the creation of a new project within the Fedora Project?

Formal methods are specialized, with many special tools. In concept it is very similar to the "Electronics Lab" spin; if you need to perform these tasks, you want a suite of tools to help. A group focused on meeting those needs is more likely to produce a useful result.

In theory, this work could be part of the "Science and Technology" (S&T) SIG, but many members of the S&T SIG will not be interested in this work, and conversely, much of the S&T work is of less interest to the potential members of the Formal Methods SIG. For example, one long term goal is creating a formal methods spin; this spin would not contain all the S&T related packages, but only those related to formal methods. It would be easier to do these things with a separate SIG that coordinated as necessary with existing SIGs, instead of working within an existing SIG.

How the project will benefit the Fedora Project and the Fedora Community?

1. . It will create new and improved packages of useful tools that anyone in the Fedora Community can use.
2. . Using these packages should enable the Fedora project to help develop higher-quality programs.
3. . These packages would give people a reason to try Fedora if they had not tried it before (e.g., through a spin), potentially enlarging the Fedora Community.

Plan of action

Immediate requirements to establish the project

• Create the SIG wiki page and mailing list. Link to already-existing material such as: http://www.openproofs.org
• Create the yum group "Formal methods" so that people can install the suite already packaged.
• Make this a proposed feature for Fedora 14; see: Features/Policy

Short-term strategy for the formation and governing of the project

In some sense, the project is already formed. David A. Wheeler has already identified a target set of applications to be packaged at http://www.openproofs.org, and has encouraged many to package important tools (including packaging some himself).

Jerry James created some packages separately from David A. Wheeler, and once they learned of each other, they have been working together. Others, such as Alan Dunn, Tim Colles, and Richard Jones have also created Fedora packages that implement formal methods tools and/or are key infrastructure for them.

Wheeler has created a preliminary list of the most important tools unpackaged. The short-term strategy is to first to package those most important tools. In addition, the group should help identify important integration issues (where tools are supposed to work together but do not) and then fix them themselves or encourage others to do so. Eventually, some sort of process for adding/removing/prioritizing tools and issues will be set up, but in the short term a simple list of packages & filing bugs for integration issues should serve.

A mid-term outlook of how the project will be made a permanent fixture of the Fedora Project

The "spin" should help make this a permanent fixture. As people work to not only create packages, but improve their integration with other packages, packages that previously didn't take advantage of these capabilities can do so more easily. For example, ordinary software development tools (like Eclipse) should be enhanced so that they can be easily extended to make calls to formal methods tools.

A long-term set of goals to make the project a true success

• Include in Fedora all formal method tool suites used by significant industrial projects, such as Frama-C/Jessie and ACL2.
• Aid in maturing these tools. Many of these tools are less mature, due in part to a lack of feedback from real users. Making it easier to install and use these tools will make it more likely that tool developers will get useful feedback.
• Prove the behaviors of some FLOSS programs (or portions of them), where the proofs themselves are FLOSS - i.e., to develop open proofs. The result would be programs in Fedora that provably have certain useful properties (and thus are extremely reliable). These need not be pre-existing, as long as the implementations are useful enough so that they would eventually become packages in Fedora in their own right.

Note that some of these long-term goals help not only the Fedora Project, but the larger world, as they can increase the reliability and security of software, hardware, and systems throughout the world. That is a good thing.