Relating Communicating Processes with Different Interfaces

• Autorzy: Burton J. , Koutny M. , Pappalardo G.
• Języki publikacji: EN

Abstrakty

EN

We present here an implementation relation intended to formalise the notion that a system built of communicating processes is an acceptable implementation of another base, or target, system in the event that the two systems have different interfaces. Such a treatment has clear applicability in the software development process, where (the interface of) an implementation component may be expressed at a different level of abstraction to (the interface of) the relevant specification component. Technically, processes are formalised using Hoare's CSP language, with its standard failures-divergences model. The implementation relation is formulated in terms of failures and divergences of the implementation and target processes. Interface difference is modelled by endowing the implementation relation with parameters called extraction patterns. These are intended to interpret implementation behaviour as target behaviour, and suitably constrain the former in connection to well-formedness and deadlock properties. We extend the results of our previous work and replace implementation relations previously presented by a single, improved scheme. We also remove all the restrictions previously placed upon target processes. Two basic kinds of results are obtained: realisability and compositionality. The latter means that a target composed of several connected systems may be implemented by connecting their respective implementations. The former means that, if target and implementation in fact have the same interface, then the implementation relation they should satisfy collapses into standard implementation pre-order. We also show how to represent processes and extraction patterns in a manner amenable to computer implementation, and detail a graph-theoretic restatement of the conditions defining the implementation relation, from which algorithms for their automatic verification are easily derived.

Słowa kluczowe

EN

theory of parallel and distributed computation; behaviour abstraction; refinement; communicating sequential processes; compositionality; verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 59, nr 1
• Strony: 1--37
• Opis fizyczny: Bibliogr. 22 poz..

Twórcy

autor

Burton J.

• School of Computing Science, University of Newcastle, Newcastle upon Tyne NE1 7RU, U.K.

autor

Koutny M.

• School of Computing Science, University of Newcastle, Newcastle upon Tyne NE1 7RU, U.K.

autor

Pappalardo G.

• Dipartimento di Matematica e Informática, Universitci di Catania, 1-95125 Catania, Italy

Bibliografia

• [1] Abadi, M., Lamport, L: The Existence of Refinement Mappings, Theoretical Computer Science, 82, 1991, 253-284.
• [2] Aceto. L. Hennessy, M. C. B.: Towards Action-Relinement in Process Algebras, Information and Computation, 103. 1993. 204-269.
• [3] Brinksma. E., Jonsson. B.. Orava. F.: Refining Interfaces of Communicating Systems, TAPSOFT '91: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advances in Distributed Computing (ADC) and Colloquium on Combining Paradigms for Software Developmemnt (CCPSD) (S. Abramsky, T. S. E. Maibaum, Eds.). LNCS 494, Springer-Verlag. 1991.
• [4] Burton, J. Koutny, M. Pappalardo, G.: Implementing Communicating Processes in the Event of Interface Difference. Proceedings of ACSD 2001 (A. Valmari, A. Yakovlev, Eds.), IEEE Computer Society, 2001.
• [5] Burton, J. Koutny, M. Pappalardo. G.: Verifying Implementation Relations, Proceedings of International Symposium on FME 2001: Formal Methods for Increasing Software Productivity (S. Abramsky, T. S. E. Maibaum. Eds.), LNCS 2021. Springer-Verlag. 2001.
• [6] Burton, J., Koutny. М.. Pappalardo, G., Pietkiewicz-Koutny, M.: Compositional Development in the Event of Interface Difference, Concurrency in Dependable Computing (P. Ezhilchelvan. A. Romanovsky. Eds.), Kluwer Academic Publishers. 2002.
• [7] Collette, P., Jones, C. B.: Enhancing the Tractability of Rely/Guarantee Specifications in the Development of Interfering Operations. Technical Report CUMCS-95-10-3. Department of Computing Science, Manchester University. 1995.
• [8] Hennessy. M. C. B.: Algebraic Theory of Processes, MIT Press, 1988.
• [9] Hoare, C. A. R.: Communicating Sequential Processes, Prentice Hall, 1985.
• [10] Jonsson, B.: Compositional Specification and Verification of Distributed Systems, ACM TOPLAS, 16, 1994, 259-303.
• [11] Koutny, M., Mancini, L., Pappalardo, G.: Two Implementation Relations and the Correctness of Communicated Replicated Processing, Formal Aspects of Computing.9. 1997, 119-148.
• [12] Koutny, M., Pappalardo, G.: Behaviour Abstraction for Communicating Sequential Processes, Fundamenta Informaticae. 48. 2001, 21-54.
• [13] Lamport, L.: The Implementation of Reliable Distributed Multiprocess Systems, Computer Networks, 2, 1978.95-114.
• [14] Lynch, N. A., Tuttle, M. R.: Hierarchical Correctness Proofs for Distributed Algorithms, Proceedings of 6th PODC, ACM. 1987.
• [15] Mancini, L. V., Pappalardo, G.: Towards a Theory of Replicated Processing, Proceedings of Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (M. Joseph. Ed.). LNCS 331, Springer-Verlag, 1988.
• [16] Milner, R.: Communication and Concurrency. Prentice Hall. 1989.
• [17] Rensink, A., Gorrieri, R.: Vertical Implementation, Information and Computation. 170, 2001,95-133.
• [18] Roscoe, A. W.: The Theory and Practice of Concurrency, Prentice-Hall, 1998.
• [19] Schepers, H., Hooman, J.: Trace-Based Compositional Reasoning About Fault Tolerant Systems, Proceedings of PARLE '93 - Parallel Architectures and Languages Europe (A. Bode. M. Reeve. G. Wolf. Eds.), LNCS 694, Springer-Verlag, 1993.
• [20] Stark. E. W.: Proving Entailment Between Conceptual State Specifications. Theoretical Computer Science, 56. 1988, 135-154.
• [21] Wong, K., Wonham, W. M.: Hierarchical Control of Discrete-Event Systems, Discrete Event Dynamic Systems: Theory and Applications, 6(3), 1996, 241-27.
• [22] Zhong, H., Wonham, W. M.: On the Consistency of Hierarchical Supervision in Discrete-Event Systems, IEEE Transactions on Automatic Control, 35(10), 1990, 1125-1134.