v
Questions
about model checking?
Ø
Relationship
to theorem proving?
Ø
Iterative
nature of increasing confidence in a specification
Ø
Others?
v
Z-style
specifications
Ø
Brief review of
static and dynamic schema
Ø
Brief review
of the notation
§
Atomic types
·
Some built-in
(like integers)
·
New ones can
be declared (like NAME in the birthday book)
§
Three kinds
of composite types
·
Set types: a
set containing elements of a given type
¨
{1,2,4,8,16}
¨
{p : PERSON |
age(p) >16 }
·
Cartesian
product types: tuples containing
elements of (potentially) different types
·
Schema types:
essentially bindings, but beyond our scope
§
Relations and
functions
·
These are
represented in Z as sets of tuples, where every tuple in the set represents an
element in the specified relation or function
·
There is also
special syntactic sugar
¨
X « Y represents the set of binary relations
between the sets X and Y
¨
X ® Y represents
the set of total functions between the sets X and Y (and adding a vertical bar
in the middle of the arrow represents partial functions)
·
These are
mathematical entities, not algorithms or rules for computation, so one can
(like in math) compare for equality across them, etc.
·
All of the
above entities have the same type: P
(X ´ Y) (where P represents the powerset operator)
§
There are a
number of other standard parts of the notation: universal and existential
quantifiers, basic logic operators, etc.
Ø
Introduce a
bit more of the birthday book example
§
Note that the
schema describe what happens when the preconditions are met (such as, adding a
new birthday only when the name isn't previously known)
§
How should
error cases be handled?
·
One choice is
to expand the definitions of the schema
¨
This can get
unwieldy quickly
·
Another
choice is to define the normal and off-normal cases separately and to combine
them using the schema calculus
¨
Essentially,
the schema calculus allows you to apply logical operators to Z schema
§
As I have
mentioned before, this is great at the specification level, but not
straightforward at the implementation level
·
What
precisely does it mean to conjoin two implementations?
¨
Is there an
AOP (aspect oriented programming) characterization of this?
Ø
Final note on
Z per se; one of the most noted uses is at IBM, where it was used to helped a
major reengineering of the CICS system
§
http://www.comlab.ox.ac.uk/oucl/qata92.html
v
Then tie
Z-style specifications to model checking
Ø
Model
checking only applies to finite systems since it is, at its heart, enumerative
Ø
But many
Z-style specifications are infinite systems, at least with respect to the issue
of data
§
That is, Z
integers are mathematical integers, for instance
Ø
One approach
to handling infinite state systems using techniques for finite state systems:
abstraction. One builds a finite
abstraction of an infinite state system that captures key aspects of the
system, and then analyzes or checks that abstraction
·
In all such
cases, one is concerned with some questions like:
¨
If a property
is proven to be true in the abstraction, do we know if it holds in the original
system?
¨
If a property
is proven to be false in the abstraction, do we know if it is false in the
original system?
Ø
Jackson and
Damon took a somewhat different approach (Nitpick)
§
They use
enumeration, as in model checking, but they explicitly truncate the state space
that they check
·
For example,
for integers, they might try all combinations of values up through 5 or 10
·
They then
report on any counterexamples they find within that truncated state space
¨
Ex: If there
are four phones in use simultaneously, then there is a situation in which one
phone is connected to no conversations; this might be a counterexample for a
desired property (that any phone in use is involved in a conversation)
§
They have
several implementations of this, and several examples
·
One
implementation uses explicit model checking, with (smart but) actual
enumeration of all the states
·
Another
implementation uses symbolic model checking
·
Usually, the
symbolic version is faster, but in some cases it doesn't work at all (and there
is no obvious way to determine when and where it works and doesn't)