Nothing Special   »   [go: up one dir, main page]

Skip to main content

Refinement of Structured Interactive Systems

  • Conference paper
Theoretical Aspects of Computing – ICTAC 2014 (ICTAC 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8687))

Included in the following conference series:

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 to check access.

Access this chapter

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)

    Google Scholar 

  2. 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)

    Article  Google Scholar 

  3. Abrial, J.-R.: Modeling in Event-B: System and Software Design. Cambridge University Press (2010)

    Google Scholar 

  4. Back, R.J., Kurki-Suonio, R.: Decentralization of process nets with centralized control. In: PODC 1983, pp. 131-142. ACM (1983)

    Google Scholar 

  5. Back, R.J., Wright, J.V.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)

    Book  MATH  Google Scholar 

  6. 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)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  8. Banu-Demergian, I.T., Stefanescu, G.: Towards a formal representation of interactive systems. Fundamenta Informaticae 131, 313–336 (2014)

    MathSciNet  MATH  Google Scholar 

  9. Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier (2001)

    Google Scholar 

  10. Broy, M.: Compositional refinement of interactive systems. Journal of the ACM 44, 850–891 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  11. Broy, M., Olderog, E.R.: Trace-oriented models of concurrency. In: [9], pp. 101–196

    Google Scholar 

  12. Broy, M., Stefanescu, G.: The algebra of stream processing functions. Theoretical Compututer Science 258, 99–129 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  13. 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)

    Chapter  Google Scholar 

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

  15. 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)

    Chapter  Google Scholar 

  16. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall International (1976)

    Google Scholar 

  17. 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)

    Google Scholar 

  18. 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)

    Google Scholar 

  19. 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)

    Chapter  Google Scholar 

  20. Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes I and II. Information and Computation 100, 1–77 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  21. Misra, J., Cook, W.R.: Computation Orchestration. Software and System Modeling 6, 83–110 (2007)

    Article  Google Scholar 

  22. Morgan, C.: Programming from Specifications. Prentice-Hall (1998)

    Google Scholar 

  23. Olszewski, M., Back, R.-J.: Agile Development with Stepwise Feature Introduction. In: ENASE 2012, pp. 161–166 (2012)

    Google Scholar 

  24. Petri, C.A., Reisig, W.: Petri net. Scholarpedia 3(4), 6477

    Google Scholar 

  25. Popa, A., Sofronia, A., Stefanescu, G.: High-level structured interactive programs with registers and voices. Journal of Universal Computer Science 13, 1722–1754 (2007)

    MathSciNet  Google Scholar 

  26. Stefanescu, G.: Network algebra. Springer (2000)

    Google Scholar 

  27. Stefanescu, G.: Interactive systems with registers and voices. Draft, School of Computing, National University of Singapore (July 2004)

    Google Scholar 

  28. Stefanescu, G.: Interactive systems with registers and voices. Fundamenta Informaticae 73, 285–306 (2006)

    MathSciNet  MATH  Google Scholar 

  29. Stefanescu, G.: Towards a Floyd logic for interactive rv-systems. In: ICCP 2006, Technical University of Cluj-Napoca, pp. 169–178 (2006)

    Google Scholar 

  30. RODIN tool platform, http://www.event-b.org/platform.html

  31. Walden, M., Sere, K.: Reasoning About Action Systems Using the B-Method. Formal Methods in Systems Design 13, 5–35 (1998)

    Article  Google Scholar 

  32. Wegner, P.: Interactive foundations of computing. Theoretical Computer Science 192, 315–351 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  33. URL, http://www.petrinets.info/

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics