Bipartitioning of LOTOS Specifications

摘要

Bipartitioning of a LOTOS specification means decomposition of the behavior into two parts. These parts communicate over a hidden synchronization gate or over a reliable underlying service. Bipartitioning is a Correctness Preserving Transformation. The resulting specification is proved to be weak bisimulation equivalent with the original specification. The design decision on which the transformation is based is a bipartitioning of the gates of the specification to be bipartitioned by the designer. The thesis develops algorithms for the bipartitioning of Basic LOTOS specifications. The algorithms are implemented in a software tool, called CLEAVER. A designer makes a partitioning of observable and non-observable gates of a specification and the tool then automatically derives the target specification. Deriving protocols from services is one of the important uses of the bipartitioning method. Other applications are restructuring and modularization of a design and the derivation of Upper and Lower Testers for conformance testing.