Formal Methods:
Three suggestions for rapid adoption
Wolfram Schulte
RiSE, MSR
Workshop on Usable Verification
11/15/2010
First
Build on the shoulder of giants:
Unify and leverage tool chains
From Program analysis tools in 2000-2003…
Slam
Fugue
Prefix/
Prefast
ESP
Modelchecker
Dataflow
Analyzer
Symbolic
Interpret.
Dataflow
Analyzer
Abstract
Domains
Custom
Decision
Procedure
Abstract
Domains
Simple
Decision
Procedure
… to formal methods tools in 2004-2010…
SymDiff
Daphne
Chalice
VCC
Spec#
Poirot
Havoc
Fine
Sage
Rex
Boogie
Isabelle
Simplify
Sym Autom
Z3
Bek
Pex
Formula
CodeContracts
….to…
Second
Specifications for free:
Embrace developer languages
CodeContracts
•
•
•
•
Use a language agnostic library to author contracts
Enables runtime and compile-time checking based on AI
Supports full scenario: author, check, view, doc
Authoring ships in VS 2010, > 50k downloads for tools, key feature
CodeContracts: Code as Specifications
•
•
•
•
Use a language agnostic library to author contracts
Enables static and dynamic checking
Contracts support “squiggles”, views, doc.- generation
Authoring ships in VS 2010, > 50k downloads for tools
static int MinIndex(int[] data) {
Contract.Requires(data != null);
Contract.Ensures(Contract.Result<int>() >= -1);
Contract.Ensures(Contract.Result<int>() < data.Length);
var result = -1;
for (int i = 0; i < data.Length; i++)
result = (result<0 || data[i]<data[result]) i: result;
return result;
}
Pex: Tests as Specifications
•
•
•
•
Embrace Unit Tests/Test Driven Development
Supports auto. test case gen./environment isolation (Moles)
Uses extended reflection and dynamic symbolic execution
Pex as powertools for VS 2010, Moles for VS 2012, >70k downloads
void ReadWrite(string name, string data) {
Assume.IsTrue(name != null && data != null);
Write(name, data);
var readData = Read(name);
Assert.AreEqual(data, readData);
}
 string name, string data:
name ≠ null ⋀ data ≠ null ⇒
equals(
ReadResource(name,WriteResource(name,data)),data)
SymDiff: Programs as Specifications
• Addresses AppCompat/Versioning problem
• Performs static semantic diff of closely related programs
• Uses boogie, etc to check where programs are different
Pex4Fun: Programs as Puzzles
Third
Catch flaws early:
from code to design analysis
Formula for Modeling
Provide a general/intermediate language for capturing model-based
abstractions, and support automated model synthesis in any direction.
Core formal
specification language
(CLP with negation
over regular types)
Use-case:
Formalize domainspecific abstractions
Module system for
composing specs and
crossing abstraction
boundaries
Formal descriptions of
design spaces and
reachability problems (in
progress)
Use-case:
Combine/relate
specs with help
from the language
Use-case:
Design-space exploration /
model synthesis
Formula’s Model Synthesis
Given a spec and a partial model, then symbolic execution constructs a
formula representing the design space.
Formula
Specification
Symbolic
Execution
SMT Formula
Encode solution region
Try something new
Z3 Solver
Reconstruct
FORMULA model
Infer Cardinality bounds
on data type instances
Add symmetry breaking
Pick next region
Formula: Applications
Translate your logic/configuration/constraint /…
problem into Formula:
• Software/Hardware Mappings: Autozar/Muscle
controller
• Architectures for the cloud: ECM
• Policy management and generic policy engines:
Dkal, SecPal, etc
• VM provisioning for the cloud: Systemcenter
• UML/DSL mappings…
Summary: Usable Verification
• Build on the shoulder of giants:
Unify and leverage tool chains
• Specifications for free:
Embrace developer languages
• Catch flaws early:
From code to design analysis
And use modern media to tell about
success stories usable verification
Descargar

Three suggestions for Usable Formal Methods