Abstract
We have proposed a formal semantics for a programming language that supports the announcement of events. Based on this semantics, it is clear that event-based systems share some substantial properties with parallel systems. In particular, announcing an event results in the parallel execution of subscribers to this event with the remainder of the announcing program. In this paper, we show how usual concurrency concepts such as synchronization and mutual exclusion can be supported in the stepwise development of event-based applications. The approach in this paper is based on Jones’s rely/guarantee method for the development of interfering programs. We also show how deadlock free event-based applications can be developed. Finally, the paper extends Stølen’s technique of handling auxiliary variables to support the development of more complex event-based applications.
This work was supported in part by the European Commission projects MOTION (MObile Teamwork Infrastructure for Organizations Networking) and EasyComp (Easy Composition in Future Generation Component Systems) and the Austrian Research Foundation (FWF) project OPELIX.
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
Aczel, P.: An inference rule for parallel composition. Technical report, University of Manchester (February 1983)
Barret, D.J., Clarke, L.A., Tarr, P.L., Wise, A.E.: A framework for event based software integration. ACM Transactions on Software Engineering and Methodology 5(4), 378–421 (1996)
Bergner, K., Rausch, A., Sihling, M.: A componentware development methodology based on process patterns. In: Proceedings of 5th Annual Conference on Pattern Languages of Programs, PLOP 1998 (1998)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Carzaniga, A., Rosenblum, D.S., Wolf, A.L.: Design and evaluation of a wide-area event notification service. ACM Transactions on Computer Systems 3(19), 332–383 (2001)
Dingel, J.: Systematic parallel programming. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh (December 1999)
Dingel, J., Garlan, D., Jha, S., Notkin, D.: Reasonning about Implicit Invocation. In: Proceedings of the 6th International Symposium on the Foundations of Software Engineering, FSE-6. ACM, New York (1998)
Dingel, J., Garlan, D., Jha, S., Notkin, D.: Towards a formal treatment of implicit invocation using rely/guarantee reasoning. Formal Aspects of Computing 10 (1998)
Fenkam, P., Gall, H., Jazayeri, M.: A Systematic Approach to the Development of Event-Based Applications. In: Proceedings of the 22th IEEE Symposium on Reliable Distributed Systems (SRDS 2003), Florence, Italy, October 2003. IEEE Computer Press, Los Alamitos (2003)
Fenkam, P., Gall, H., Jazayeri, M.: Composing Specifications of Event Based Applications. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 67–86. Springer, Heidelberg (2003)
Garlan, D., Khersonsky, S.: Model checking implicit-invocation systems. In: Proceedings of the 10th International Workshop on Software Specification and Design, San Diego, CA (November 2000)
Garlan, D., Notkin, D.: Formalizing design spaces: Implicit invocation mechanisms. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 551. Springer, Heidelberg (1991)
Jackson, D.: Automatic analysis of architectural styles. Technical report, MIT Laboratory for Computer Sciences, Software Design Group, Unpublished Manuscript, Available at http://sdg.lcs.mit.edu/dnj/publications.html
Jones, C.B.: Tentative steps towards a development method for interfering programs. Transactions on Programming Languages and Systems 5(4) (October 1983)
Milner, R.: The Calculus of Communicating Systems. Prentice-Hall, Englewood Cliffs (1993)
Object Management Group. OMG Formal Documentation. Technical report, OMG (December 1999)
Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Communications of the ACM 19(5) (May 1976)
Prasad, K.: A calculus of broadcasting systems. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol. 493. Springer, Heidelberg (1991)
Reiss, S.P.: Connecting tools using message passing in the field program development environment. IEEE Software 19(5) (July 1990)
Roman, E., Ambler, S.W., Jewell, T.: Mastering Enterprise JavaBeans, 2nd edn. John Wiley & Sons, Chichester (2002)
Soundararajan, N.: A proof technique for parallel programs. Theoretical Computer Science 31, 13–29 (1984)
Stølen, K.: Development of Parallel Programs on Shared Data-Structures. PhD thesis, Department of Computer Science, University of Manchester (1990)
Stølen, K.: A Method for the Development of Totally Correct Shared-State Parallel Programs. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 510–525. Springer, Heidelberg (1991)
TIBCO Software Inc. TIB/Rendezvous TX Concepts Release 1.1. Technical report, TIBCO Software Inc.,Palo Alto, CA (November 2002), http://www.tibco.com
Xu, Q., He, J.: A theory of state-based parallel programming by refinement: part 1. In: Proceedings of the 4th BCS-FACS Refinement Workshop. Springer, Heidelberg (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fenkam, P., Gall, H., Jazayeri, M. (2003). Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_35
Download citation
DOI: https://doi.org/10.1007/978-3-540-45236-2_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40828-4
Online ISBN: 978-3-540-45236-2
eBook Packages: Springer Book Archive