×

zbMATH — the first resource for mathematics

A stepwise approach to linking theories. (English) Zbl 06700461
Bowen, Jonathan P. (ed.) et al., Unifying theories of programming. 6th international symposium, UTP 2016, Reykjavik, Iceland, June 4–5, 2016. Revised selected papers. Cham: Springer (ISBN 978-3-319-52227-2/pbk; 978-3-319-52228-9/ebook). Lecture Notes in Computer Science 10134, 134-154 (2017).
Summary: Formal modelling of complex systems requires catering for a variety of aspects. The Unifying Theories of Programming (UTP) distinguishes itself as a semantic framework that promotes unification of results across different modelling paradigms via linking functions. The naive composition of theories, however, may yield unexpected or undesirable semantic models. Here, we propose a stepwise approach to linking theories where we deal separately with the definition of the relation between the variables in the different theories and the identification of healthiness conditions. We explore this approach by deriving healthiness conditions for Circus Time via calculation, based on the healthiness conditions of CSP and a small set of principles underlying the timed model.
For the entire collection see [Zbl 1355.68010].
MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Software:
Circus; Isabelle/UTP; Z
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River (1998)
[2] Roscoe, A.W.: Understanding Concurrent Systems. Springer, London (2010) · Zbl 1211.68205 · doi:10.1007/978-1-84882-258-0
[3] Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Aspects Comput. 21(1), 3–32 (2007) · Zbl 1165.68048
[4] Sherif, A., Cavalcanti, A.L.C., He, J., Sampaio, A.C.A.: A process algebraic framework for specification and validation of real-time systems. Formal Aspects Comput. 22(2), 153–191 (2010) · Zbl 1214.68224 · doi:10.1007/s00165-009-0119-6
[5] Wei, K., Woodcock, J., Cavalcanti, A.: Circus Time with reactive designs. In: Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.) UTP 2012. LNCS, vol. 7681, pp. 68–87. Springer, Berlin (2013). doi: 10.1007/978-3-642-35705-3_3 · Zbl 1452.68057 · doi:10.1007/978-3-642-35705-3_3
[6] Cavalcanti, A., Sampaio, A., Woodcock, J.: A Refinement Strategy for Circus. Formal Aspects Comput. 15, 146–181 (2003) · Zbl 1093.68555 · doi:10.1007/s00165-003-0006-5
[7] Harwood, W., Cavalcanti, A., Woodcock, J.: A theory of pointers for the UTP. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 141–155. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-85762-4_10 · Zbl 1161.68388 · doi:10.1007/978-3-540-85762-4_10
[8] Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall, Upper Saddle River (1996) · Zbl 0855.68060
[9] Schneider, S.: Concurrent and Real-Time Systems: the CSP Approach. Worldwide Series in Computer Science. Wiley, New York (2000)
[10] Wei, K., Woodcock, J., Cavalcanti, A.: New Circus Time. Technical report, University of York (2012). https://www.cs.york.ac.uk/circus/publications/techreports/reports/Circus%20Time.pdf · Zbl 1452.68057
[11] Butterfield, A., Gancarski, P., Woodcock, J.: State visibility and communication in unifying theories of programming. In: Third IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009, pp. 47–54, July 2009 · doi:10.1109/TASE.2009.57
[12] Canham, S., Woodcock, J.: Three approaches to timed external choice in UTP. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 1–20. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-14806-9_1 · Zbl 1457.68059 · doi:10.1007/978-3-319-14806-9_1
[13] Morgan, C.: Programming from Specifications. Prentice Hall, Upper Saddle River (1994) · Zbl 0829.68083
[14] Woodcock, J., Cavalcanti, A.: A tutorial introduction to designs in unifying theories of programming. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 40–66. Springer, Berlin (2004). doi: 10.1007/978-3-540-24756-2_4 · Zbl 1196.68031 · doi:10.1007/978-3-540-24756-2_4
[15] Cavalcanti, A., Woodcock, J.: A tutorial introduction to CSP in unifying theories of programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220–268. Springer, Berlin (2006). doi: 10.1007/11889229_6 · doi:10.1007/11889229_6
[16] Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall, Upper Saddle River (1989) · Zbl 0777.68003
[17] Ribeiro, P.: Super-Theories. Technical report, University of York (2016). https://www-users.cs.york.ac.uk/pfr/reports/super-theories.pdf
[18] Foster, S., Zeyda, F., Woodcock, J.: Isabelle/UTP: A Mechanised Theory Engineering Framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 21–41. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-14806-9_2 · Zbl 1457.68061 · doi:10.1007/978-3-319-14806-9_2
[19] Banks, M.J., Jacob, J.L.: On integrating confidentiality and functionality in a formal method. Formal Aspects Comput. 26(5), 963–992 (2013) · Zbl 1342.68191 · doi:10.1007/s00165-013-0285-4
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.