Counter-constrained finite state machines: modelling component protocols with resource-dependencies

This report deals with the specification of software component
protocols (i.e., the set of service call sequences). The
contribution of this report is twofold: (a) We discuss specific
requirements of real-world protocols, especially in the presence
of components wich make use of limited resources. (b) We define
counter-constrained finite state machines (CC-FSMs), a novel
extension of finite state machines, specifically created to
model protocols having dependencies between services due to
their access to shared resources. We provide a theoretical
framework for reasoning and analysing CC-FSMs. Opposed to finite
state machines and other approaches, CC-FSMs combine two
valuable properties: (a) CC-FSMs are powerful enough to model
realistic component protocols with resource allocation, usage,
and de-allocation dependencies between methods (as occurring in
common abstract datatypes such as stacks or queues) and (b)
CC-FSMs have a decidabile equivalence- and inclusion problem as
proved in this report by providing algorithms for efficient
checking equivalence and inclusion. These algorithms directly
lead to efficient checks for component interoperability and
... mehrsubstitutability.

Keywords: software component protocols, finite state machine
extension, decidable inclusion check, interoperability,
substitutability.