Action refinement from a logical point view

Abstract. 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 µ-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 φ for the process P, an action a of P and a specification ψ for the process Q that may refine a and produces a refined specification. We prove under some syntactical conditions: if Q | = ψ then P | = φ iff P [a 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