In this cand.scient. thesis we propose a strategy for testing validityof decomposition of contract oriented specifications. The strategy isbased on Abadi and Lamport's Composition Theorem for theTemporal Logic of Actions and test case generation fromexecutable specifications.
A composition rule, inspired by the Compositon Theorem, is formulatedin a semantics based on timed streams. A subset of theSpecification and Decription Language (SDL) is defined andthe SDL subset is formalized in the semantics.
A simplification of the testing strategy was realized in anexperimental prototype tool for testing of contract decompositions inSDL. In addition another prototype tool based on a conventionalstrategy was built as a reference tool.
Testing of the two tools showed that both validated valid contractdecompositions and falsified invalid contract decompositions. Testingalso showed that the tool based on the composition rule in someinteresting situations was considerably more efficient than the toolbased on the conventional strategy.