Abstract
The event based architectural style has been recognized as fostering the development of large-scale and complex systems by loosely coupling their components. It is therefore increasingly deployed in various environments such as middleware for mobile computing, message oriented middleware, integration frameworks, communication standards, and commercial toolkits. The development of applications based on this paradigm is, however, performed in such an ad-hoc manner that it is often difficult to reason about their correctness. This is partly due to the lack of suitable specification and verification techniques. In this paper, we review the existing theory of specifying and verifying such applications, argue that it cannot be applied for the development of large-scale and complex systems, and finally propose a novel approach (LECAP) for the construction of correct event based applications. Our approach is superior to the existing approaches in many respects: 1) we assume a while-parallel language with a synchronization construct, 2) neither a pending event infrastructure nor a consume statement are required, 3) a dynamic (instead of static) binding is assumed, 4) no restriction is made on the number of simultaneous executions of the same program 5) our approach is oriented towards top-down development of systems. The paper also presents two examples for illustrating the approach.
This work was supported by the European Commission in the Framework of the IST Program,Key Action II on New Methods of Work and eCommerce.Project number: IST-1999-11400 MOTION (MObile Teamwork Infrastructure for Organizations Networking).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
P. Aczel. An inference rule for parallel composition, University of Manchester, 1983.
Stern Agerholm and Peter Gorm Larsen. A Lightweight Approach to Formal Methods. In Proceedings of the Interna-tional Workshop on Currents Trends in Applied Formal Methods. Springer Verlag, October 1998.
K.P. Birman. The progress group approach to reliable distributed computing. Communications of the ACM, 12:37–53, December 1993.
K. Brockschmidt. Inside OLE. Microsoft Press, Redmond, 1995.
C.A.R Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
A. Carzaniga, D.S. Rosenblum, and A.L. Wolf. Design and evaluation of a wide-area event notification service. ACM Transactions on Computer Systems, 3(19):332–383, August 2001.
K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison Wesley, 1988.
G. Cugola, E. Di Nitto, and A. Fuggetta. The JEDI Event-Based Infrastructure and its Application to the Development of the OPSS WFMS. Transaction of Software Engineering (TSE), 27(9), September 2001.
E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
J. Dingel, D. Garlan, S. Jha, and D. Notkin. Reasonning about Implicit Invocation. In Proceedings of the 6th International Symposium on the Foundations of Software Engineering, FSE-6. ACM, 1998.
J. Dingel, D. Garlan, S. Jha, and D. Notkin. Towards a formal treatment of implicit invocation using rely/guarantee reasoning. Formal Aspects of Computing, 10, 1998.
C. Ene and Traian Muntean. A broadcast-based calculus for communicating systems. Technical report, Laboratoire d’Informatique de Marseille, 2000.
Object Management Group. OMG Formal Documentation. Technical report, OMG, December 1999.
C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10), 1969.
D. Jackson and J. Wing. Lightweight Formal Methods. In IEEE Computer. Springer Verlag, April 1996.
C.B. Jones. Tentative steps toward a development method for interfering programs. Transactions on Programming Languages and Systems, 5(4), October 1983.
Cli. B. Jones. Systematic software development using VDM. Prentice-Hall International, 1990. 2nd edition.
B. Krishnamurthy and N.S. Barghouti. Provence: A process visualization and enactment environment. In Proceedings of 4th European Software Engineering Conference, pages 451–465, 1993.
R. Milner. The Calculus of Communicating Systems. Prentice Hall, 1993.
Robert Orfali, Dan Harkey, and Jeri Edwards. The Essential Client/Server Survival Guide. Wiley Computer Publishing, second edition, 1996.
S. Owicki and D. Gries. Verifying properties of parallel programs: an axiomatic approach. Communications of the ACM, 19(5), May 1976.
K. Prasad. A calculus of broadcasting systems. In Proceedings of TAPSOFT’91, volume 493, 1991.
J.M. Purtilo. The polylith software bus. ACM Transactions on Programming Languages and Systems, 16(1):151–174, 1994.
S.P. Reiss. Connecting tools using message passing in the field program development environment. IEEE Software, 19(5), July 1990.
Ed Roman and Scott W. Ambler and Tyler Jewell. Mastering Enterprise JavaBeans. John Wiley & Sons, second edition, 2002.
K. Stolen. A Method for the Development of Totally Correct Shared-State Parallel Programs. In CONCUR’91, pages 510–525. Springer Verlag, 1991.
SunSoft. The ToolTalk Service: An Inter-operability Solution. Prentice-Hall, 1993.
Peter Sutton, Rhys Arkins, and Bill Segall. Supporting disconnectednesstransparent information delivery for mobile and invisible computing. In Proceedings of 2001 IEEE International symposium on Cluster Computing and the Grid (CCGrid’01), May 2001.
Jim Woodcock and Arthur Hughes. Unifying theories of parallel programming. In Proceedings of the International Conference on Formal Engineering Methods (ICFEM 2002). Springer Verlag, 2002.
Q. Xu, W.-P. de Roever, and J. He. The rely guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 9:149–174, 1997.
Q. Xu and J. He. A theory of state-based parallel programming by refinement: part 1. In Proceedings of the 4th BCS-FACS Refinement Workshop. Springer Verlag, 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). Composing Specifications of Event Based Applications. In: Pezzè, M. (eds) Fundamental Approaches to Software Engineering. FASE 2003. Lecture Notes in Computer Science, vol 2621. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36578-8_6
Download citation
DOI: https://doi.org/10.1007/3-540-36578-8_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00899-6
Online ISBN: 978-3-540-36578-5
eBook Packages: Springer Book Archive