A stepwise approach to linking theories

Pedro Ribeiro; Ana Cavalcanti; Jim Woodcock

doi:10.1007/978-3-319-52228-9_7

A stepwise approach to linking theories

Pedro Ribeiro^*, Ana Cavalcanti, Jim Woodcock

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English
Title of host publication	Unifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers
Editors	Jonathan P. Bowen, Huibiao Zhu
Publisher	Springer
Pages	134-154
Number of pages	21
ISBN (Print)	9783319522272
DOIs	https://doi.org/10.1007/978-3-319-52228-9_7
Publication status	Published - 11 Jan 2017
Event	6th International Symposium on Unifying Theories of Programming, UTP 2016 - Reykjavik, Iceland Duration: 4 Jun 2016 → 5 Jun 2016

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10134 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	6th International Symposium on Unifying Theories of Programming, UTP 2016
Country/Territory	Iceland
City	Reykjavik
Period	4/06/16 → 5/06/16

Bibliographical note

Funding Information:
We would like to thank Simon Foster for his support regarding Isabelle/UTP. This work is funded by EPSRC grants EP/H017461/1 and EP/M025756/1.

Publisher Copyright:
© Springer International Publishing AG 2017.

Keywords

Circus
CSP
Theory engineering
UTP

Access to Document

10.1007/978-3-319-52228-9_7

Cite this

Ribeiro, P., Cavalcanti, A., & Woodcock, J. (2017). A stepwise approach to linking theories. In J. P. Bowen, & H. Zhu (Eds.), Unifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers (pp. 134-154). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10134 LNCS). Springer. https://doi.org/10.1007/978-3-319-52228-9_7

Ribeiro, Pedro ; Cavalcanti, Ana ; Woodcock, Jim. / A stepwise approach to linking theories. Unifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers. editor / Jonathan P. Bowen ; Huibiao Zhu. Springer, 2017. pp. 134-154 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{9004bb8036d2463e83a53b7d00479dfa,

title = "A stepwise approach to linking theories",

abstract = "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.",

keywords = "Circus, CSP, Theory engineering, UTP",

author = "Pedro Ribeiro and Ana Cavalcanti and Jim Woodcock",

note = "Funding Information: We would like to thank Simon Foster for his support regarding Isabelle/UTP. This work is funded by EPSRC grants EP/H017461/1 and EP/M025756/1. Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 6th International Symposium on Unifying Theories of Programming, UTP 2016 ; Conference date: 04-06-2016 Through 05-06-2016",

year = "2017",

month = jan,

day = "11",

doi = "10.1007/978-3-319-52228-9_7",

language = "English",

isbn = "9783319522272",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "134--154",

editor = "Bowen, {Jonathan P.} and Huibiao Zhu",

booktitle = "Unifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers",

address = "Germany",

}

Ribeiro, P , Cavalcanti, A & Woodcock, J 2017, A stepwise approach to linking theories. in JP Bowen & H Zhu (eds), Unifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10134 LNCS, Springer, pp. 134-154, 6th International Symposium on Unifying Theories of Programming, UTP 2016, Reykjavik, Iceland, 4/06/16. https://doi.org/10.1007/978-3-319-52228-9_7

A stepwise approach to linking theories. / Ribeiro, Pedro ; Cavalcanti, Ana ; Woodcock, Jim.
Unifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers. ed. / Jonathan P. Bowen; Huibiao Zhu. Springer, 2017. p. 134-154 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10134 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A stepwise approach to linking theories

AU - Ribeiro, Pedro

AU - Cavalcanti, Ana

AU - Woodcock, Jim

N1 - Funding Information: We would like to thank Simon Foster for his support regarding Isabelle/UTP. This work is funded by EPSRC grants EP/H017461/1 and EP/M025756/1. Publisher Copyright: © Springer International Publishing AG 2017.

PY - 2017/1/11

Y1 - 2017/1/11

N2 - 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.

AB - 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.

KW - Circus

KW - CSP

KW - Theory engineering

KW - UTP

UR - http://www.scopus.com/inward/record.url?scp=85010635519&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-52228-9_7

DO - 10.1007/978-3-319-52228-9_7

M3 - Conference contribution

AN - SCOPUS:85010635519

SN - 9783319522272

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 134

EP - 154

BT - Unifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers

A2 - Bowen, Jonathan P.

A2 - Zhu, Huibiao

PB - Springer

T2 - 6th International Symposium on Unifying Theories of Programming, UTP 2016

Y2 - 4 June 2016 through 5 June 2016

ER -

Ribeiro P , Cavalcanti A , Woodcock J. A stepwise approach to linking theories. In Bowen JP, Zhu H, editors, Unifying Theories of Programming - 6th International Symposium, UTP 2016, Revised Selected Papers. Springer. 2017. p. 134-154. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-52228-9_7

A stepwise approach to linking theories

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Cite this