(Iniitial version) |
(→Detailed Description: Add link to new page) |
||
| (51 intermediate revisions by 2 users not shown) | |||
| Line 3: | Line 3: | ||
= Feature Name = | = Feature Name = | ||
Formal methods | |||
<!-- If too short, could say "Basic support for key provers, solvers, and formal methods tools" --> | |||
== Summary == | == Summary == | ||
"Formal methods" are techniques that use mathematics to prove that models of software, hardware, or systems will or will not have certain behaviors. To be practical, they must be automated using tools. | |||
systems using mathematics | Fedora has now added basic support for some key formal methods tools, | ||
greatly increase the reliability of software and hardware. | letting you prove that some facts are true (given other facts) and/or model systems using mathematics. In some limited cases they can be used to greatly increase the reliability of software and hardware. | ||
This suite has been primarily packaged by the members of the [[FormalMethods|Fedora Formal Methods SIG]]. | |||
== Owner == | == Owner == | ||
* Name: [[User:dwheeler|David A. Wheeler]] | * Name: [[User:dwheeler|David A. Wheeler]] (proposer) | ||
== Current status == | == Current status == | ||
* Targeted release: [[Releases/ | * Targeted release: [[Releases/13 | Fedora13 ]] | ||
* Last updated: | * Last updated: 2010-01-14 | ||
* Percentage of completion: 100% | * Percentage of completion: 100% | ||
| Line 22: | Line 26: | ||
== Detailed Description == | == Detailed Description == | ||
No realistic software or hardware can be exhaustively tested; exhaustively testing | |||
a program that merely adds three 64-bit numbers would take more time than the Earth has existed. | |||
So for decades people have worked to develop tools that can apply | |||
mathematical techniques to prove that software and hardware (or a model of them) does or does not do something. | |||
These tools can also be used whenever it's important to prove something is true, | |||
or to solve for values given a large number of constraints. | |||
Although these tools are still maturing, they are beginning to become useful in some limited circumstances. | |||
Now some key ones are packaged so developers on Fedora can begin to experiment with them. | |||
The [[Formal methods tool suite]] page provides a longer description of the various kinds of tools, and the packages that implement them. | |||
Here are some of these kinds of tools, along with packages of programs | |||
that perform them: | |||
* Automated Theorem Provers: These take mathematical facts and attempt to prove a goal, completely automatically. Packages: ''prover9'', ''Zenon''. | |||
* Interactive Theorem Provers: These help humans take mathematical facts and attempt to prove a goal, in cases where the automated tools can't manage. Package: ''Coq'', ''PVS'' (as pvs-sbcl) | |||
* Program Provers: These take software code and work to prove claims about them, typically by breaking the code and claims into a large number of verification conditions (VCs) for the above to prove. Package: ''Why'' (for annotated C and Java) | |||
* Formal specification languages: These let people describe software or systems using a mathematically rigorous language, such as Z. Package: ''tex-zfuzz'' | |||
* Boolean Satisfiability (SAT) solvers: These take boolean equations and solve for them; they are a basic building block for some implementations of the above. Packages: sat4j, minisat2 | |||
Do ''not'' assume that you can just take a program prover on a big existing program and start | |||
using it effectively; program prover tools are just ''starting'' to become mature. | |||
All such tools have limitations, scale can be a problem, and it's typically more effective | |||
to develop the proofs simultaneously with the program. | |||
Nevertheless, for those who are interested in the technology, have small-scale problems | |||
where they can be applied, or who wish to help it mature, | |||
these are a great place to start. | |||
SAT solvers ''have'' been used in a variety of places. | |||
[http://en.opensuse.org/Libzypp/Sat_Solver Another distribution is using a SAT solver to speed up RPM dependency analysis]. | |||
For more information, and a list of FLOSS tools, see | |||
[http://www.dwheeler.com/essays/high-assurance-floss.html|High Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS)... with Lots on Formal Methods / Software Verification]. | |||
== Benefit to Fedora == | == Benefit to Fedora == | ||
This enables developers to start using these kinds of programs in a variety of circumstances. | |||
== Scope == | == Scope == | ||
Developers have had to package a number of programs, most of which have not been packaged before. | |||
In some cases, we've had to address integration problems. | |||
This feature has no effect on those who don't wish to use these tools. | |||
== Test Plan == | == Test Plan == | ||
No special hardware or system preparation is required; simply install the packages | |||
listed above. | |||
Many of the toolsuites include some checking. | |||
In addition, the "Why" suite can use many other tools; we have used its | |||
"binary-search.c" example with gwhy to test integration with Zenon and Coq. | |||
<!-- This does not need to be a full-fledged document. Describe the dimensions of tests that this feature is expected to pass when it is done. If it needs to be tested with different hardware or software configurations, indicate them. The QA team will turn this information into a more complete test plan. The more specific you can be, the better the final test plan will be. | <!-- This does not need to be a full-fledged document. Describe the dimensions of tests that this feature is expected to pass when it is done. If it needs to be tested with different hardware or software configurations, indicate them. The QA team will turn this information into a more complete test plan. The more specific you can be, the better the final test plan will be. | ||
| Line 45: | Line 90: | ||
== User Experience == | == User Experience == | ||
Target users will notice that they can easily install these tools. | |||
<!-- If this feature is noticeable by its target audience, how will their experiences change as a result? Describe what they will see or notice. --> | <!-- If this feature is noticeable by its target audience, how will their experiences change as a result? Describe what they will see or notice. --> | ||
== Dependencies == | == Dependencies == | ||
There are no special dependencies. | |||
<!-- What other packages (RPMs) depend on this package? Are there changes outside the developers' control on which completion of this feature depends? In other words, completion of another feature owned by someone else? Other upstream projects like the kernel (if this is not a kernel feature)? --> | <!-- What other packages (RPMs) depend on this package? Are there changes outside the developers' control on which completion of this feature depends? In other words, completion of another feature owned by someone else? Other upstream projects like the kernel (if this is not a kernel feature)? --> | ||
== Contingency Plan == | == Contingency Plan == | ||
None necessary, revert any undesirable packages. | |||
<!-- If you cannot complete your feature by the final development freeze, what is the backup plan? This might be as simple as "None necessary, revert to previous release behaviour." Or it might not. If you feature is not completed in time we want to assure others that other parts of Fedora will not be in jeopardy. --> | <!-- If you cannot complete your feature by the final development freeze, what is the backup plan? This might be as simple as "None necessary, revert to previous release behaviour." Or it might not. If you feature is not completed in time we want to assure others that other parts of Fedora will not be in jeopardy. --> | ||
== Documentation == | == Documentation == | ||
Where permitted by license, packages include documentation. | |||
In a few cases (e.g., minisat2), no documentation was provided at all, | |||
and we have added some basic documentation to help people get started. | |||
We expect this to improve in future releases; it will also be easier to get | |||
people to write documentation once the programs themselves are easier to install. | |||
<!-- Is there upstream documentation on this feature, or notes you have written yourself? Link to that material here so other interested developers can get involved. --> | <!-- Is there upstream documentation on this feature, or notes you have written yourself? Link to that material here so other interested developers can get involved. --> | ||
== Release Notes == | |||
No special release notes. | |||
<!-- The Fedora Release Notes inform end-users how to deal with platform changes such as ABIs/APIs, configuration or data file formats, or upgrade concerns. If there are any such changes involved in this feature, indicate them here. You can also link to upstream documentation if it satisfies this need. This information forms the basis of the release notes edited by the documentation team and shipped with the release. --> | <!-- The Fedora Release Notes inform end-users how to deal with platform changes such as ABIs/APIs, configuration or data file formats, or upgrade concerns. If there are any such changes involved in this feature, indicate them here. You can also link to upstream documentation if it satisfies this need. This information forms the basis of the release notes edited by the documentation team and shipped with the release. --> | ||
---- | ---- | ||
[[Category:FeaturePageIncomplete]] | [[Category:FeaturePageIncomplete]] | ||
Latest revision as of 15:41, 20 January 2010
Feature Name
Formal methods
Summary
"Formal methods" are techniques that use mathematics to prove that models of software, hardware, or systems will or will not have certain behaviors. To be practical, they must be automated using tools.
Fedora has now added basic support for some key formal methods tools, letting you prove that some facts are true (given other facts) and/or model systems using mathematics. In some limited cases they can be used to greatly increase the reliability of software and hardware.
This suite has been primarily packaged by the members of the Fedora Formal Methods SIG.
Owner
- Name: David A. Wheeler (proposer)
Current status
- Targeted release: Fedora13
- Last updated: 2010-01-14
- Percentage of completion: 100%
Detailed Description
No realistic software or hardware can be exhaustively tested; exhaustively testing a program that merely adds three 64-bit numbers would take more time than the Earth has existed. So for decades people have worked to develop tools that can apply mathematical techniques to prove that software and hardware (or a model of them) does or does not do something. These tools can also be used whenever it's important to prove something is true, or to solve for values given a large number of constraints.
Although these tools are still maturing, they are beginning to become useful in some limited circumstances. Now some key ones are packaged so developers on Fedora can begin to experiment with them.
The Formal methods tool suite page provides a longer description of the various kinds of tools, and the packages that implement them.
Here are some of these kinds of tools, along with packages of programs that perform them:
- Automated Theorem Provers: These take mathematical facts and attempt to prove a goal, completely automatically. Packages: prover9, Zenon.
- Interactive Theorem Provers: These help humans take mathematical facts and attempt to prove a goal, in cases where the automated tools can't manage. Package: Coq, PVS (as pvs-sbcl)
- Program Provers: These take software code and work to prove claims about them, typically by breaking the code and claims into a large number of verification conditions (VCs) for the above to prove. Package: Why (for annotated C and Java)
- Formal specification languages: These let people describe software or systems using a mathematically rigorous language, such as Z. Package: tex-zfuzz
- Boolean Satisfiability (SAT) solvers: These take boolean equations and solve for them; they are a basic building block for some implementations of the above. Packages: sat4j, minisat2
Do not assume that you can just take a program prover on a big existing program and start using it effectively; program prover tools are just starting to become mature. All such tools have limitations, scale can be a problem, and it's typically more effective to develop the proofs simultaneously with the program. Nevertheless, for those who are interested in the technology, have small-scale problems where they can be applied, or who wish to help it mature, these are a great place to start.
SAT solvers have been used in a variety of places. Another distribution is using a SAT solver to speed up RPM dependency analysis.
For more information, and a list of FLOSS tools, see Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS)... with Lots on Formal Methods / Software Verification.
Benefit to Fedora
This enables developers to start using these kinds of programs in a variety of circumstances.
Scope
Developers have had to package a number of programs, most of which have not been packaged before. In some cases, we've had to address integration problems.
This feature has no effect on those who don't wish to use these tools.
Test Plan
No special hardware or system preparation is required; simply install the packages listed above. Many of the toolsuites include some checking. In addition, the "Why" suite can use many other tools; we have used its "binary-search.c" example with gwhy to test integration with Zenon and Coq.
User Experience
Target users will notice that they can easily install these tools.
Dependencies
There are no special dependencies.
Contingency Plan
None necessary, revert any undesirable packages.
Documentation
Where permitted by license, packages include documentation. In a few cases (e.g., minisat2), no documentation was provided at all, and we have added some basic documentation to help people get started. We expect this to improve in future releases; it will also be easier to get people to write documentation once the programs themselves are easier to install.
Release Notes
No special release notes.