Ray: A Framework for Correct Event Based Applications

Software today is responsible for running and controlling much of the Services of our society. Banking, commerce, and transportation are just some examples of applications that rely entirely an Computer Software. Such Software is increasingly distributed among various Computers in different geographic locations, and is accessed by users with a large variety of devices ranging from powerful desktop Computers to cell-phones. Software technology is being challenged to meet the stringent requirements of such applications. Today`s Software technology was created for applications that used a relatively small number of homogeneous devices. Current applications need to deal with thousands, and in the future perhaps millions, of highly heterogeneous devices. As a result, an active area of research in distributed Systems is currently trying to invent Software methodologies consisting of communication paradigms, tools, mechanisms, and techniques that overcome the limitations of current languages and techniques and address the needs of the emerging computing environments and applications. One of the few promising techniques for this purpose is the event-based communication paradigm (also called implicit invocation or pubhsh/subscribe). The primary benefit of the event-based paradigm is that it Supports the Loose coupling of components that compose an application and therefore scales to large numbers of heterogeneous components. The use of the event- based architectural style has been successfully demonstrated in the development of large-scale and complex Systems. It has therefore been rapidly incorporated in not only research prototypes but also commercial products and toolkits and even in software communication standards. The practice of application development based an this paradigm is, however, ad hoc and informal. As a result, it is often difficult to reason about the correctness of the resulting applications. The lack of a systematic and rigorous basis for the development of eventbased Systems has become a serious problem as the event-based paradigm is being used increasingly in important domains such as flight-control, e-commerce, automotive, and home applications. The existing theory of specifying and verifying such applications cannot be applied for the development of large-scale and complex Systems.The aim of this research project is to develop a novel approach (Ray) for the construction of correct event-based applications. The Ray framework will include a methodology for the specification, stepwise development, and verification of event- based applications, together wich a CASE toolset to Support the methodology. The methodology will have practical application in all emerging application domains that exploit the event-based paradigm. Such domains include pervasive computing, telecommunications, electronic commerce, and Internet-based applications.

Coming to its end, the Ray project marks the introduction of a new toolset for the engineering of an important class of software called event-based applications. Event-based applications are now widely used in software and hardware industries to assemble components. Examples of fields that rely on this paradigm are news production and distribution services, e-recruiting, automobile, aerospace, and manufacturing industries. Despite its pervasiveness and its wide acceptance, the verification of event-based applications is a challenge that many practitioners are confronted with. The lack of methodology for guiding this activity was one of the issues pertaining to the ad hoc nature of the development of event-based applications. During the past three years researchers from the Distributed Systems Group of the Vienna University of Technology investigated the difficulties inherent to the construction of this sort of application. The result of this investigation can be used for simplifying the design and testing of event-based applications. The key added value to practitioners is the ability to now address the development of their applications in a stepwise yet compositional way. In essence, this means that components developed and tested separately can be put together without the need to go through the verification of each single piece again. Instead, practitioners are proposed mechanical rules to derive proof obligations for the composed system. The Ray project gave rise to a start-up company that is now launching a new sort of e-recruiting tool called Peoplet (http://www.peoplet.com). Hand in hand with the Peoplet team, researchers from the Distributed Systems Group of the Vienna University of Technology were able to validate their research results and ensure their practicability. Peoplet is a pure, non trivial and holistic approach to e-recruiting that brings more comfort, more control, better chances, and greater community support to its users.