Sammendrag
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.