Lecture 16 (February 10, 1999)

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)