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.
Chapter PDF
References
M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82:253–284, 1991.
M. Abadi and G. Plotkin. A logical view of composition and refinement. Theoretical Computer Science, 114:3–30, 1993.
Aceto L. and Hennessy. M, Towards action refinement in process algebra. Proc. LICS’89, 138–145,1989.
Bowen Alpern and Fred B. Schneider. Defining liveness. Information Processing Letters, 21:191–185, 1995.
A. Bouajjani, J.C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis. Safety for branching time semantics. 18th ICALP,July 1991, LNCS 510, pp. 76–92.
G. Boudol. Atomic actions. Bull. European Assoc. The. Com. Sci. 38:136–144.
J.C. Bradfield. Verifying Temporal Properties of Systems. Birkhäuser Boston, Mass.
P. Degano and R. Gorrieri, Atomic Refinement in Process Description Languages. TR 17-91 HP Pisa Center, 1991.
R.J. van Glabbeek and F.W. Vaandrager. Petri nets models for algebraic theories of concurrency. Proc. PARLE conference, Eindhoven, The Netherlands 1987, Vol. II (Parallel Languages), LNCS 259, pp. 224–242.
R. Gorrieri and A. Rensink. Action refinement. Handbook of Process Algebra, Elsevier Science, 1047–1147. 2001.
C.A.R. Hoare. Communicating Sequential Processes, Prentice-Hall, 1985.
Michaela Huhn. Action refinement and properties inheritance in systems of sequential agents. CONCUR’96, LNCS 1119, pp. 263–277.
Martin Lange and Colin Stirling. Model checking fixed point logic with chop. FOSSACS 2002, LNCS 2303, pp. 250–263.
Mila Majster-Cederbaum and Frank Salger. Correctness by construction: towards verification in in hierarchical system development. SPIN 2000, LNCS 1885, pp. 163–180.
Mila Majster-Cederbaum and Frank Salger. A priori verification of reactive systems. In Eds T. Bolognesi, D. Latella: Formal Methods for Distributed System Development. pp.35–50. Kluwer Publishers, 2000.
Mila Majster-Cederbaum, Naijun Zhan and Harald Fecher. Action refinement from a logical point view. To appear as a research report.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
Markus Müller-Olm. A Modal Fixpoint Logic with Chop. STACS’99, LNCS 1563, pp. 510–520.
Peter Niebert. A í-calculus with local views for systems of sequential agents. MFCS’95, LNCS 969, pp.563–573.
M. Nielsen, U. Engberg and K.S. Larsen. Fully abstract models for a process language with refinement. Proc. REX School on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, 1989, LNCS 354, pp. 523–548.
A. Rensink. Models and Methods for Action Refinement. PhD thesis, University of Twente, Enschede, Netherlands, Aug. 1993.
J. Sifakis. Research directions for concurrency. ACM Computing Surveys, 28(4es):55. 1996.
C. Stirling. Modal and temporal logics for processes, Banff Higher Order Workshop 1995, LNCS 1043, pp. 149–237.
A. Tarski. A lattice-theoretical fixpoint theorem and its application. Paci.c J. Math., 5:285–309, 1955.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Majster-Cederbaum, M., Zhan, N., Fecher, H. (2003). Action Refinement from a Logical Point of View. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2003. Lecture Notes in Computer Science, vol 2575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36384-X_21
Download citation
DOI: https://doi.org/10.1007/3-540-36384-X_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00348-9
Online ISBN: 978-3-540-36384-2
eBook Packages: Springer Book Archive