Action refinement from a logical point of view

Action refinement provides a mechanism to design a complex reactive system hierarchically. This paper is devoted to action refinement from a logical point of view, and to combining the hierarchical implementation of a complex system with the hierarchical specification of the system in order to verify it in an easy way. To this end, we use a TCSP-like language with an action refinement operator as a modeling language, and an extension of the modal mu-calculus, called FLC (Fixpoint Logic with Chop) [18], as a specification language. Specifications in FLC can be refined via a mapping that takes as arguments an abstract specification phi for the process P, an action a of P and a specification psi for the process Q that may refine a and produces a refined specification. We prove under some syntactical conditions: if Q satisfies psi then P satisfies phi iff P[a curved right arrow Q] satisfies the refined specification. Therefore our approach supports 'a priori' verification in system design and can be used to decrease substantially the complexity of verification.