Abstract
We present a formal framework for characterising plug-in relationships between component specifications. A suitability requirement is defined based on the effect one component has on the other in terms of deadlock. Unlike monotonic operations such as parallel composition, not all such suitability requirements are preserved by refinement. Hence, we define the notion of a bicompositional relation between co-operating processes which is preserved by component-wise refinements. The approach is described in CSP using the failures semantic model. The aim is to underpin a mixed-paradigm approach combining different specification methods, including state-based deductive formalisms such as Action Systems, and event-based model checking formalisms such as CSP/FDR. The objective is to play to the strengths and overcome limitations of each technique, by treating different system aspects with individual tools and notations which are most appropriate.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
S.D. Brookes, C.A.R. Hoare, and A.W. Roscoe. A theory of communicating sequential processes. JACM, 31:560–599, 1984.
R.J.R. Back and R. Kurki-Suonio. Decentralisation of process nets with centralised control. In 2nd ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pages 131–142, 1983.
S.D. Brookes and A.W. Roscoe. An improved failures model for communicating sequential processes. In Proc. Pittsburgh Seminar on Concurrency. Springer, 1985.
M.J. Butler. A CSP Approach to Action Systems. DPhil thesis, University of Oxford, 1992.
M.J. Butler. csp2b: A practical approach to combining CSP and B. In J. Woodcock J. Davies, J.M. Wing, editor, FM99 World Congress. Springer Verlag, 1999.
Sadie Creese and Joy Reed. Verifying end-to-end protocols using induction with CSP/FDR. In Proc. of IPPS/SPDP Workshop on Parallel and Distributed Processing, LNCS 1586, Lisbon, Portugal, 1999. Springer.
Formal Systems (Europe) Ltd. Failures Divergence Refinement. User Manual and Tutorial, version 2.11.
C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
Gavin Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proc. of TACAS, volume 1055 of LNCS. Springer, 1996.
G. Lowe and A.W. Roscoe. Using CSP to detect errors in the TMN protocol. IEEE Trans. Soft. Eng., 23(10), 1997.
C. Meadows. The NRL protocol analyzer: An overview. J. Logic Programming, 19,20, 1994.
C.C. Morgan. Of wp and CSP. In D. Gries W.H.J. Feijen, A.G.M. van Gasteren and J. Misra, editors, Beauty is our business: a birthday salute to Edsger W. Dijkstra. Springer-Verlag, 1990.
A.W. Roscoe and R.S. Lazic. Using logical relations for automated verification of data-independent CSP. In Oxford Workshop on Automated Formal Methods ENTCS, Oxford, UK, 1996.
A.W. Roscoe. Theory and Practice of Concurrency. Prentice Hall, 1998.
G.M. Reed and A.W. Roscoe. The timed failures-stability model for CSP. Theoretical Computer Science, 211:85–127, 1999.
J.N. Reed, J.E. Sinclair, and F. Guigand. Deductive reasoning versus model checking: two formal approaches for system development. In K. Taguchi K. Araki, A. Galloway, editor, Integrated Formal Methods 1999, York, UK, June 1999. Springer Verlag.
J.N. Reed, J.E. Sinclair, and G.M. Reed. Routing-a challenge to formal methods. In Proc. of International Conference on Parallel and Distributed Processing Techniques and Applications, Las Vegas, 1999. CSREA Press.
J.M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 2nd ed., 1992.
H. Treharne and S. Schneider. How to drive a B machine. To appear.
H. Treharne and Schneider S. Using a process algebra to control B operations. In K. Taguchi K. Araki, A. Galloway, editor, Integated Formal Methods, pages 437–456, York, UK, 1999. Springer Verlag.
J.C.P. Woodcock and C.C. Morgan. Refinement of state-based concurrent systems. In Proc. of VDM Symposium, LNCS 428. Springer-Verlag, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Reed, J.N., Sinclair, J.E. (2001). Combining Independent Specifications. In: Hussmann, H. (eds) Fundamental Approaches to Software Engineering. FASE 2001. Lecture Notes in Computer Science, vol 2029. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45314-8_5
Download citation
DOI: https://doi.org/10.1007/3-540-45314-8_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41863-4
Online ISBN: 978-3-540-45314-7
eBook Packages: Springer Book Archive