Interface Moore machines are used as the operational model for interface specifications of systems. A logic of actions (LA) is defined to specify interface Moore machines which implement interface specifications. Specific notations and methods for specifying, implementing, composing, and verifying interface Moore machines are introduced. A concurrent composition operator is defined for Moore machines. It is shown how to refine interface specifications into Moore machine specifications and further on into Moore machine programs and how to relate, derive and prove implementations, invariants, and functional interface specifications for Moore machines. The interface behavior of the concurrent composition of Moore machines is identical to the concurrent composition of their interface behavior.