tractable object models Daniel Jackson Software Design Group MIT Laboratory for Computer Science WG 2.9 · Flims · February 7, 2000
lightweight formal methods
focus
high risk issues
structural aspect
light notation
minimal syntax, pure ascii
simple semantics
integrated graphical/textual
light analysis
fully automatic, interactive speed
concrete output (instances & counters)
declarative style
incrementality & views
essential properties
progress
nitpick (1996)
sets & binary relations
Z-like schema calculus
sequential composition
alcoa (1999)
first-order quantifiers
object model declarations
mutability constraints
more nimble schema calculus
alcoa’ (2000)
structures (hierarchy)
sequential composition
numbers, sequences & orders
semantic minimalism
for simple semantics, no
undefined or unknown
implicit coercions or flattenings
special treatment of attributes
relation attributes
aggregation
for conceptual modelling, no
classes, types, packages
methods
navigability
relational structure
database viewpoint [Codd, Chen, etc]
relations are tables with named columns
can have 3-way relationships
constraints use lots of quantifiers
relational calculus viewpoint [Tarski, Abrial, etc]
relations are binary
constraints use set & relation operators
my work
based on relational calculus
constraints more succinct, diagrams simpler?
but database view more familiar?
thanks to Emmanuel Letier
example
nobody has the same name as her parent
database view
all x, y, m, n | Parent (x, y) && Named (x, m) && Named (y, n) -> m != n
relational view
no p | p.name in p.parents.name
pure relational view
name & (parent ; name) = {}
modelling implication
example
worst case stopping distance
depends on train and segment
database view
relation on from Train to Segment
on has attribute wcsd
relational view
introduce new object Occupancy
segment : Occupancy -> Segment!
train : Occupancy -> Train!
wcsd : Occupancy -> Distance!
or use a function (indexed relation)
wcsd : Segment => (Train -> Dist!)
partial function problem
problem
f(x) = g(y) when x outside the domain of f?
other options
special undefined value (KAOS?, UML)
undef appears in specs
what is (x.f + y.g).h when x.f = undef ?
special logic (VDM, UML)
formulas can be half true
special semantics (Z, UML)
not all terms have a meaning
some p | p.name = daniel is meaningless
undefined applications are false (Parnas, Nitpick)
x.f != x.f true if short for !(x.f = x.f)
my approach
idea
scalar represented as singleton set
examples
some p | p.name = daniel
all p | no (p.wife & p.siblings)
all e : Employee | e.boss in e.company.employees
nice properties
no guards
no flattenings or promotions
all terms have meaning
use multiplicities for sets
no free lunch
no p | p.wife in p.siblings false if somebody’s unmarried!
no p | p.wife /in p.siblings
an example
problem
specify topology of railway
investigate placement of gates
caveats
structural aspect only
I haven’t even read the 15pp
started at midnight last night …
basic notions
segments
capability to use track in one direction
a connector at each end
seg1.from = con1
seg3.from = seg4.from
overlap
model crossings etc by overlap
seg5 in seg6.overlaps
gates
some segments have gates at the end
gates are open or closed
trains
occupy segments; ignore position
object model diagram
Alloy model: declarations
model Bart {
domain {Segment, Connector, Gate, Train}
state Segments {
from, to : Segment -> Connector!
overlaps : Segment -> Segment
gate : Segment! -> Gate?
partition Open, Closed : Gate
on : Train -> Segment !
succ : Segment -> Segment
conflicts : Segment -> Segment
}
an indicative invariant
inv Overlaps {
all s, t | s.from = t.to && s.to = t.from -> s in t.overlaps
all s | s in s.overlaps
}
a safety condition
// no every segment has at most one train on it and its overlapping segments
cond Safety {
all s | sole (s + s.overlaps).~on
}
two definitions
// the successors of a segment are those that are from the connector it is to
def succ {
all s | s.succ = {t | t.from = s.to}
}
// a segment conflicts with another segment if their successors overlap
def conflicts {
all s | s.conflicts = {t | some (s.succ & t.succ.overlaps)} - s
}
policy invariants
// place a gate wherever there’s a conflict
inv GatePlacement {
all s | some s.conflicts -> some s.gate
}
// at most one open gate in a conflicting group
inv Policy {
all s | sole (s.conflicts + s).gate & Open
}
an operation
// in a step, any number of trains can move // no train goes through a closed gate
op TrainsMove (ts : Train) {
all t : ts | t.on' in t.on.succ
no (ts.on.gate & Closed)
all t : Train - ts | t.on = t.on'
}
analysis strategy
check consistency
ask for instances of states and transitions
specify conditions to get good cases
check consequences
assert implications of invariants
assert properties of operations
eg, preservation of invariant
bug example, inconsistency
I asked Alcoa to show me a state
none found in scope of 3
realized I had made from and to surjective
the condition I executed
cond Acyclic {some Segment && no s | s in s.+succ}
Alcoa’s output
Analyzing Acyclic ...
Scopes: Gate(3), Connector(3), Segment(3), Train(3)
Total conversion time: 0 seconds
Total solver time: 0 seconds
No instances exist in this scope
the fix: drop the plus
from, to : Segment + -> Connector!
bug example, implication
I asserted that conflicts is symmetric
Alcoa generated a counterexample
realized overlaps should be symmetric too
the assertion I checked
assert ConflictsSym {
all s, t | s in t.conflicts -> t in s.conflicts
}
the fix: add the constraint
all s, t | s in t.overlaps -> t in s.overlaps
output
Alcoa’s output
Analyzing ConflictsSym ...
Scopes: Gate(3), Connector(3), Segment(3), Train(3)
Counterexample found:
Domains:
Connector = {C1,C2}
Segment = {S1,S2}
Relations:
conflicts = {S2 -> {S1}}
from = {S1 -> C2, S2 -> C1}
overlaps = {S1 -> {S1,S2}, S2 -> {S2}}
succ = {S1 -> {S1}, S2 -> {S2}}
to = {S1 -> C2, S2 -> C1}
Skolem constants:
s = S1
t = S2
bug example, preservation of invariant
I asserted that the safety condition is preserved
assert PolicyWorks {
all t | TrainsMove (t) && Safety -> Safety'
}
scenarios Alcoa produced how I responded
ex nihilo train creation add Trains = Trains’ to operation
train enters backlooping segment constrained assertion to ignore this
train hits train in succ segment added separation to policy
funky overlap scenario went to sleep
funky overlap
why it’s hard (1)
what we’d like Alcoa to do
given a formula
find a solution
or show there aren’t any
solution is state or transition
theory says no!
Alloy is undecidable (because of relations)
so no decision procedure
practice says yes!
more important to find bugs
than to show there aren’t any
only consider instances in scope
now a finite search: decidable
small scope hypothesis
most bugs can be caught by considering only small instances
why it’s hard (2)
even in finite scope
huge space of configurations
add a relation in scope of k
for transition, 2x components
why search is needed
language is declarative
no recipe for after-states
example: BART
6 relations
for transition, 12 rels
scope of 3
2^ 144 ~ 10^40 cases
at 10G/sec, 10^20 centuries (1 nanocentury = ? secs)
translating to SAT
what you learned in CS 101
3-SAT: first NP-c problem
to show a problem is hard
what we know now
SAT is usually easy
to show a problem is easy
research status
case studies
mobile IPv6
Sullivan’s COM analysis, Jini, intensional naming
with NASA: air-traffic control
with IBM: K42 operating system
tool development
new symmetry scheme
open interfaces
visualization
application to code
shape analysis
design conformance
conclusion
key ideas
abstract -> not tractable?
small scope hypothesis
focus on existence, not absence
acknowledgments
language: M. Jackson, Liskov, Hall
tool: Schechter, Shlyakhter
SAT solvers: Nelson, Selman, Kautz, Zhang
Moore: 1980-2000, 3 hrs -> 1 sec
Alcoa! Free while supplies last!
http://sdg.lcs.mit.edu/alcoa