Model Checking and Reduction of Behavior Protocols

Behavior protocol is a formalism used for behavior specification of software components. In a regular-expression like syntax, admissible sequences of method invocations are specified abstracting from components' internal data. While it seems to be a reasonable level of abstraction for checking correctness of communication of the software components, it can be still quite difficult for a human to read and understand. This thesis aims to help the software designer to understand the behavior specification of components more easily. An approach to automatic verification of the general temporal properties stated in Linear Temporal Logic is presented along with two techniques for reduction of behavior protocols. Reduction with respect to composition prunes out those parts of the protocols that are not used in the particular composition and vlarifies the actual role of each component. Reduction with respect to property removes the parts of the protocols that are irrelevant to the given property. The behavior protocols reduced in this manner should emphasize which part of the protocol makes the given property satisfied