Checking the consistency between the protocol and the output trace is a kind of model verification. An automatic approach is taken to check this consistency for each simulation. If a large number of checks are successful, confidence in model correctness increases.
Before automatic checking can be done, the protocol must be translated into a formal description to be processed by computer programs. Here, a rule-based approach is employed. A rule file to be processed contains several rules that the output trace must conform to. The rules are written with extended regular expressions, an extended form of UNIX regular expressions. Each rule consists of 4 parts: pre-condition, post-condition, guard (optional) and counter-rule property (optional). Pre-condition is a regular expression used to match a part of the output trace. It, combined with the guard (a boolean expression), defines when and where the rule is applicable. If it is applicable and the counter-rule property is false, the post-condition (another regular expression) must be found in the output; on the contrary, if counter-rule is true, the post-condition must not be found.
For example, the rule in Table 7.1 expresses the requirement that the sender of a message does NOT receive the broadcast after 1 second. (However, it does not address whether it can receive the message after 0.9999 second or 1.0001 seconds.)
In the pre-condition, five groups are defined between parentheses. They are numbered 1 to 5 in the order of their appearance. Group 1 matches the floating-point time. Group 2 matches the sequence number. They constitute a time tuple. Group 3 matches the integer ID of the sender. Group 4 matches the message, which is an arbitrary string. Group 5 matches the ID of the chat room that the sender is connected to.
In the post-condition, [(...)] contains an expression, where
values of groups can be cited with their index numbers behind
``\''. Thus, [(\1+1)] is the value of the first
group plus 1. [(\3)] is equal to group 3. More about
regular expressions can be found in [41].
Suppose the execution stops at simulated time 50. The checking should
not exceed time 50. Without additional conditions, if a message is
sent to a chat room at time 49.5, the checker would expect a
corresponding broadcast at time 50.5. To cope with this, a guard [(\1+1)]<50 is added. This tells the checker that the rule is
applicable only when the value of group 1 (floating-point time) plus 1
is less than 50.
Since a client should not receive its own message, the counter-rule property is set to true.