State Machines , an extension of UML 2.0  State Machines
permitting to capture the interleaving and nesting of operation calls,
employ the trace semantics and compliance relation of Behavior
Protocols  to reason on component substitutability.
The key goal of this thesis is to make the Port State Machines more accessible for use in UML tools by employing the Object Constraint Language (OCL)  to express the compliance relation. An additional goal is to also express in OCL the various constraints imposed on Port State Machines.
These goals have been achieved and implemented using the Object Constraint Language Environment (OCLE) 2.0, developed in the Computer Science Research Laboratory at the Babes-Bolyai University.
The thesis has been successfully defended on Sep 20, 2005, and is now publicly accessible and available for download.
The following are available for download:
 Mencl, V.: Specifying Component Behavior with Port State
Machines, Electronic Notes in Theoretical Computer Science, vol. 101C
pp. 129-153, Proceedings of the Workshop on the Compositional
Verification of UML Models (CVUML, Oct 21, 2003, part of UML 2003),
Edited by F. de Boer and M. Bonsangue, Elsevier Science, DOI 10.1016/j.entcs.2004.02.019, Nov 2004
 OMG: Unified Modeling Language: Superstructure, version 2.0, Final Adopted specification, ptc/03-08-02, http://www.omg.org/uml/
 OMG: UML 2.0: Object Constraint Language, 2nd revised submission, document ad/03-01-07, http://www.omg.org/uml/