Specification for Testing - Formal Methods and Hybrid Real-Time Systems - page 291

Creation followed immediately by removal of a user does not change the system
state. But conversely, removal followed by creation of a user may result in a different
password log ( u ?) . pd and a different log ( u ?) . at . Continuing the subscript convention,
that is expressed

CreateU ser 9 RemoveU ser = id
RemoveU ser 9 CreateU ser = id[ Webbo State pd , at ] .

Further laws in Webbo follow from the following observations. The action of a user
posting mail to another does not have the same effect as that of an administrator per-
forming an analogous AdminPostOne . For it is a precondition of the former but not the
latter that sender u ? be logged in, and a precondition of the latter but not the former that
administrator a ? be logged in; but otherwise the effects are the same.
From a fresh start, log ( u ?) . no = 0, three unsuccessful logins of user u ?leavethe
system in a state in which all components are the same except that log ( u ?) . no = 3,
log ( u ?) . lock holds and log ( u ?) . at is arbitrary.
A successful login of a user followed by its logout thus leaves state unchanged except
for the log ( u ?) . at component. However a logout followed immediately by a login of the
same user leaves state unchanged only if u ? was originally logged in and at the same
client as the login.
All provide opportunities, subject to the qualification above about implementation
detail, for testing; and all suggest information that can be provided by the specifier.

4.2 Reality Check

However in real systems the check for identity requires the checking of all system com-
ponents. For example, it requires checking that the database has all and only the in-
formation that was present at the start of the operations. Expense precludes this from
being part of the testing process. But worse, such simple identities are almost never
true. Databases and other applications (such as the authentication engine) keep log files
for rollback and forensics. As these log files do not affect the functionality they rarely
feature in specifications.
Thus for testing purposes it is essential to specify explicitly the components that are
used (or not used) for the calculation of the identity relation; hence our use of the nota-
tion above. In practice that requires a combination of knowledge of both specification
(to determine which components to observe) and link (how they are represented in the
implementation).

5 Testing Consistency

Different (state-based) specification notations employ slightly different styles and hence
place emphasis on slightly different concepts. A state invariant in Z (like the three ex-
plicit predicates that constrain Loginfo 1 or the single explicit predicate that constrains

1

The statement at : C provides an implicit constraint since it expands to the type statement
at : Client with explicit constraint at ∈ C .