Decomposition of Functionality: A Correctness Preserving Lotos Transformation

摘要

Algorithms for transforming a single LOTOS (Language of Temporal OrderingSpecification) process into two interacting processes are presented. The two processes interact via either synchronous or asynchronous communication. The result of the transformation is proven to be weak bisimulation equivalent with the original process. This transformation has applications in the modularization of a design, the refinement of a service into a protocol, and the derivation of upper and lower testers for conformance testing. Two obvious extensions of the work are the incorporation of full LOTOS, so including datatypes and value passing, and the development of an automatic tool implementing the algorithms.