CSE503: Software Engineering
Lecture 16 (February 10, 1999)

David Notkin

 

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)