Abstract
The refinement concept provides a formal tool for addressing the complexity of software-intensive systems, by verified stepwise development from an abstract specification towards an implementation. In this paper we propose a novel notion of refinement for a structured formalism dedicated to interactive systems, that combines a data-flow with a control-oriented approach. Our notion is based on scenarios, extending to two dimensions the trace-based definition for the refinement of classical sequential systems. We illustrate our refinement notion with a simple example and outline several extensions to include more sophisticated distributed techniques.
Part of this research has been sponsored by the EU funded FP7 project 214158 (DEPLOY).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)
Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: An Open Toolset for Modelling and Reasoning in Event-B. International Journal on Software Tools for Technology Transfer 6, 447–466 (2010)
Abrial, J.-R.: Modeling in Event-B: System and Software Design. Cambridge University Press (2010)
Back, R.J., Kurki-Suonio, R.: Decentralization of process nets with centralized control. In: PODC 1983, pp. 131-142. ACM (1983)
Back, R.J., Wright, J.V.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)
Back, R.J., Wright, J.V.: Trace Refinement of Action Systems. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 367–384. Springer, Heidelberg (1994)
Banu-Demergian, I.T., Paduraru, C.I., Stefanescu, G.: A new representation of two-dimensional patterns and applications to interactive programming. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 183–198. Springer, Heidelberg (2013)
Banu-Demergian, I.T., Stefanescu, G.: Towards a formal representation of interactive systems. Fundamenta Informaticae 131, 313–336 (2014)
Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier (2001)
Broy, M.: Compositional refinement of interactive systems. Journal of the ACM 44, 850–891 (1997)
Broy, M., Olderog, E.R.: Trace-oriented models of concurrency. In: [9], pp. 101–196
Broy, M., Stefanescu, G.: The algebra of stream processing functions. Theoretical Compututer Science 258, 99–129 (2001)
Bryans, J.W., Wei, W.: Formal Analysis of BPMN Models Using Event-B. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 33–49. Springer, Heidelberg (2010)
Diaconescu, D., Leustean, I., Petre, L., Sere, K., Stefanescu, G.: Refinement Preserving Translation from Event-B to Register-Voice Interactive Systems. TUCS Technical Reports No. 1028 (December 2011), http://tucs.fi/publications/view/?pub_id=tDiLePeSeSt11a
Diaconescu, D., Leustean, I., Petre, L., Sere, K., Stefanescu, G.: Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 221–236. Springer, Heidelberg (2012)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall International (1976)
Dragoi, C., Stefanescu, G.: AGAPIA v0.1: A programming language for interactive systems and its typing systems. In: FINCO 2007. ENTCS, vol. 203, pp. 69–94 (2008)
Dragoi, C., Stefanescu, G.: On compiling structured interactive programs with registers and voices. In: Geffert, V., Karhumäki, J., Bertoni, A., Preneel, B., Návrat, P., Bieliková, M. (eds.) SOFSEM 2008. LNCS, vol. 4910, pp. 259–270. Springer, Heidelberg (2008)
Salehi Fathabadi, A., Rezazadeh, A., Butler, M.: Applying Atomicity and Model Decomposition to a Space Craft System in Event-B. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 328–342. Springer, Heidelberg (2011)
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes I and II. Information and Computation 100, 1–77 (1992)
Misra, J., Cook, W.R.: Computation Orchestration. Software and System Modeling 6, 83–110 (2007)
Morgan, C.: Programming from Specifications. Prentice-Hall (1998)
Olszewski, M., Back, R.-J.: Agile Development with Stepwise Feature Introduction. In: ENASE 2012, pp. 161–166 (2012)
Petri, C.A., Reisig, W.: Petri net. Scholarpedia 3(4), 6477
Popa, A., Sofronia, A., Stefanescu, G.: High-level structured interactive programs with registers and voices. Journal of Universal Computer Science 13, 1722–1754 (2007)
Stefanescu, G.: Network algebra. Springer (2000)
Stefanescu, G.: Interactive systems with registers and voices. Draft, School of Computing, National University of Singapore (July 2004)
Stefanescu, G.: Interactive systems with registers and voices. Fundamenta Informaticae 73, 285–306 (2006)
Stefanescu, G.: Towards a Floyd logic for interactive rv-systems. In: ICCP 2006, Technical University of Cluj-Napoca, pp. 169–178 (2006)
RODIN tool platform, http://www.event-b.org/platform.html
Walden, M., Sere, K.: Reasoning About Action Systems Using the B-Method. Formal Methods in Systems Design 13, 5–35 (1998)
Wegner, P.: Interactive foundations of computing. Theoretical Computer Science 192, 315–351 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Diaconescu, D., Petre, L., Sere, K., Stefanescu, G. (2014). Refinement of Structured Interactive Systems. In: Ciobanu, G., Méry, D. (eds) Theoretical Aspects of Computing – ICTAC 2014. ICTAC 2014. Lecture Notes in Computer Science, vol 8687. Springer, Cham. https://doi.org/10.1007/978-3-319-10882-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-10882-7_9
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10881-0
Online ISBN: 978-3-319-10882-7
eBook Packages: Computer ScienceComputer Science (R0)