Abstract
The paper describes two perspectives on a verification approach for Paradigm, a coordination modeling language specifying an architecture in terms of components and their collaborations. One perspective concentrates on a single collaboration: per collaboration, properties can be derived through a small set of proof rules. The other perspective concentrates on dynamic dependencies between collaborations: guided by the architecture and driven by shared components behavioral properties of the complete model can be established. Two Paradigm models, a parallel assignment and a linear pipeline of workers and buffers, illustrate the approach.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Andova, S., Groenewegen, L.P.J., Stafleu, J., de Vink, E.P.: Formalizing adaptation on-the-fly. In: Salaün, G., Sirjani, M. (eds.) Proceedings of FOCLASA. ENTCS, vol. 255, pp. 23–44 (2009)
Andova, S., Groenewegen, L.P.J., de Vink, E.P.: Towards dynamic adaptation of probabilistic systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part II. LNCS, vol. 6416, pp. 143–159. Springer, Heidelberg (2010)
Andova, S., Groenewegen, L.P.J., de Vink, E.P.: Dynamic consistency in process algebra: from paradigm to ACP. Sci. Comput. Program. 76(8), 711–735 (2011)
Andova, S., Groenewegen, L.P.J., de Vink, E.P.: Dynamic adaptation with distributed control in Paradigm. Sci. Comput. Program. 94, 333–361 (2014)
de Bakker, J.W., de Vink, E.P.: Control Flow Semantics. Foundations of Computing Series. The MIT Press, Cambridge (1996)
Cheng, B.H.C., de Lemos, R., Giese, H., Inverardi, P., Magee, J. (eds.): Software Engineering for Self-Adaptive Systems. LNCS, vol. 5525. Springer, Heidelberg (2009)
Engels, G., Groenewegen, L.: Specification of coordinated behaviour by SOCCA. In: Warboys, B.C. (ed.) EWSPT 1994. LNCS, vol. 772, pp. 128–151. Springer, Heidelberg (1994)
Groenewegen, L., de Vink, E.P.: Operational semantics for coordination in paradigm. In: Arbab, F., Talcott, C. (eds.) COORDINATION 2002. LNCS, vol. 2315, pp. 191–206. Springer, Heidelberg (2002)
Jones, C.B.: Development methods for computer programs including a notion of interference. Ph.D. thesis, Oxford University (1981)
Pierik, C., de Boer, F.S.: A proof outline logic for object-oriented programming. Theor. Comput. Sci. 343, 413–442 (2005)
Reimer, W., Schäfer, W., Schmal, T.: Towards a dedicated object-oriented software process modeling language. In: Dannenberg, R.B., Mitchell, S. (eds.) ECOOP 1997 Workshops. LNCS, vol. 1357, pp. 299–302. Springer, Heidelberg (1998)
de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Non-compositional Methods. Cambridge University Press, New York (2001)
Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects Comput. 9(2), 149–174 (1997)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Groenewegen, L.P.J., Kuiper, R., de Vink, E.P. (2016). Towards a Proof Method for Paradigm. In: Ábrahám, E., Bonsangue, M., Johnsen, E. (eds) Theory and Practice of Formal Methods. Lecture Notes in Computer Science(), vol 9660. Springer, Cham. https://doi.org/10.1007/978-3-319-30734-3_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-30734-3_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-30733-6
Online ISBN: 978-3-319-30734-3
eBook Packages: Computer ScienceComputer Science (R0)