Validation of Contract Decomposition by Testing

Abstract

In this cand.scient. thesis we propose a strategy for testing validity of decomposition of contract oriented specifications. The strategy is based on Abadi and Lamport's Composition Theorem for the Temporal Logic of Actions and test case generation from executable specifications.

A composition rule, inspired by the Compositon Theorem, is formulated in a semantics based on timed streams. A subset of the Specification and Decription Language (SDL) is defined and the SDL subset is formalized in the semantics.

A simplification of the testing strategy was realized in an experimental prototype tool for testing of contract decompositions in SDL. In addition another prototype tool based on a conventional strategy was built as a reference tool.

Testing of the two tools showed that both validated valid contract decompositions and falsified invalid contract decompositions. Testing also showed that the tool based on the composition rule in some interesting situations was considerably more efficient than the tool based on the conventional strategy.