The table example that we used in previous chapters can be qualified as functional: looking from the outside, we can view it as a function that returns an answer when it is called. We don’t have any concerns or get distracted by its internal computation and internal workings. In contrast, we can hardly understand systems which constantly react to their environments if we don’t study the series of actions they perform. This is the case for communication protocols, operating systems or command-and-control equipment. For protocols for instance, we have to consider synchronization, to prevent deadlocks, undesired arrival of messages, etc. The complexity of such protocols is by and large, concentrated in these aspects.
KeywordsModel Check Transition System Temporal Logic Transition Relation Linear Temporal Logic
Unable to display preview. Download preview PDF.