Abstract Model Specifications
Build an abstract model of required software behavior using
mathematically defined (perhaps using axioms) types (e.g.,
sets, relations).
Define operations by showing effects of that operation on the
model.
Specification includes:
Model
Invariant properties of model
For each operation:
name
parameters
return values
Pre and post conditions on the operations
Copyright
c
Nancy Leveson, Sept. 1999
a0
Z (pronounced Zed)
Z specifications are made up of "schemas"
A schema is a named, relatively short piece of specification
with two parts:
Above the line: the definition of the data entities
Below the line: the definition of invariants that hold
on those data entities
Copyright
c
Nancy Leveson, Sept. 1999
a1
Z : Defining the Abstract Model
Library
books: BOOK
status: STATUS
books = dom status
P
BOOK
Declaration says library has two visible parts of its state:
books is a set of BOOKS, which are atomic elements.
status is a partial function that maps a BOOK into a STATUS
(which is another atomic element that can take values In or Out)
The invariant says the set of books is precisely the same as
the domain of the function status.
Says every book in the Library has exactly one status
Two books may have the same status.
Example of a legal state for Library is:
books = {Principia Mathematica, Safeware}
status = (Principia Mathematica In,
Safeware
Out}
c
Copyright Nancy Leveson, Sept. 1999
a2
Z : Defining Operations
Borrow
book?: BOOK
Library
status’ = status (book?
status (book?) = In
Out)
Library declaration says operation modifies state of Library
book? is the input
A prime indicates the value after the operation
The first invariant defines a pre-condition on the operation, i.e.,
the book to be borrowed must be currently checked in.
The second invariant defines the semantics of borrowing, i.e.,
it overwrites the entry in the status function for the borrowed book.
Copyright Nancy Leveson, Sept. 1999
c
a3
Z : Proving Properties
Example: After a borrow operation, the set of books in the
library remains unchanged.
books’ = books
books’ = dom status’ [from invariant of Library]
= dom (status {book? Out}) [from post-condition of Borrow]
= dom (status {book? Out})
= dom status dom ({book? Out})
Follow from mathematics
= book book?
= book [true because first invariant of Borrow implies
that book? is an element of books]
Copyright
c
Nancy Leveson, Sept. 1999
a4
Z : Defining Observing Operations
book?: BOOK
Library
status! : STATUS
book?
status! = status (book?)
books
Find Status
indicates state is not changed by operation (a lookup op)
status! is an output variable
The first invariant says that schema only defined if the
book is known. Therefore, function application in second
invariant cannot fail.
c
Copyright Nancy Leveson, Sept. 1999
a5
Z : Another Observing Operation
Library
CheckedOut
out! = BOOKP
out! = { b:books | status(b) = Out}
Produces all the books that are currently checked out of library
Returns a (possibly empty) set of books.
Copyright Nancy Leveson, Sept. 1999
c
a6
Z : Initialization
InitLibrary
Library
books =
Still need schemas to add and remove books from the library.
Copyright Nancy Leveson, Sept. 1999
c
a7
