Current Talks

Thursday 12th February 2009 [15:00] Compensable Transactions Christian Colombo Abstract: Traditionally, business transactions have always been implemented using the ACID principles where resources are locked to guarantee atomicity and isolation. However, a lot of financial transactions may span over a long period of time. In such a case, it is not feasible to lock resources for the whole duration of the transaction. Such transactions are known as long-live transactions (LLTs). Financial transactions which involve communication to third party systems are usually considered as such. Other examples include web services where a number of independent activities are invoked with a relatively high probability of failure. Mathematical notations have been proposed to model LLT activities and their compensations. These also provide other operators such as parallel composition of activities and exception handling. In this presentation, I will give an overview of two such logics which handle compensations: sagas calculi and compensating CSP. (part of the literature review of my research) Tuesday 3rd February 2009 [14:00] Dynamic Contracts, or Contract-Centric Programming Gordon Pace Abstract: With the rise of service-oriented architectures, the use of contracts to regulate the actions that systems may undertake is increasing in importance. On one hand, contracts may be seen as static properties which systems have to satisfy. However, most services include a concept of evolving or changing contracts. One may argue that such contracts are simply more intricate contracts which may handle certain changes - however, through the use of contract negotiation, unforeseen circumstances may still arise. Giving a semantics to such dynamic contractual languages can thus be extremely challenging. In this talk, we will be showing how, without committing ourselves to any contract or programming language, different forms of static contract language semantics can be extended to deal with dynamicity. Furthermore, we show that the different extensions for the different forms of semantics preserve compatibility of the semantics. Finally, we discuss the issue of reasoning about power to change and update contracts, and how this can be encapsulated within the semantics we propose in any contract language which can reason about permissions and prohibitions. (joint work with Gilles Barthe and Gerardo Schneider) Tuesday 28th October 2008 [12:00] Runtime Verification within the Semantics and Verification Research Group: Past Work, Ongoing Work and Future Perspectives Gordon Pace Abstract: As computer systems become more and more pervasive in our everyday life, the need to guarantee their correctness is rapidly increasing. Whether it is a medical system with human lives at stake, or a financial transaction system with millions of euros at stake, it is crucial that systems do not produce anomalous behaviour. Various approaches have been advocated and used in theory and practice - from riguorous testing before deployment, to complete verification through model checking. An alternative approach becoming increasingly popular is the use of runtime verification, in which the system is not assumed to be correct, but monitors are added to the system to ensure that any bad behaviour is captured and remedied at runtime. This approach complements testing (by continuing the checks at runtime) and model checking (by relating the abstracted model to the actual system) and has been shown to be extremely effective in practice. Over this past year, we have been exploring the use of runtime verification for real-time properties, and developed a theoretical framework to reason about such properties. The framework is embodied in LARVA, a tool we have developed for the runtime verification of Java programs. In this talk, I will be presenting a short introduction to runtime verification, and present recent work we have carried out in runtime monitoring of real-time properties. I will then outline ongoing projects and research directions that we are exploring, and finish with a number of areas for possible collaboration with other areas including security, systems, software engineering and adaptive systems. The talk is also aimed as an invitation to local industry to provide real-life case studies on which we can investigate the use of runtime verification. (joint work with Christian Colombo, Gerardo Schneider and Stephen Fenech) Wednesday 29th October 2008 [10:30] Proof Transformation for Program Optimizations Tarmo Uustalu Institute of Cybernetics, Tallinn University of Technology I advocate a general technology of achieving mechanical transformation of program proofs corresponding to program optimizations. This is based on presenting program optimizations declaratively as type systems with a program transformation component whereby types are employed to record the program analysis information licensing the optimization. I show this method in action on a variety of optimizations, including some most basic standard ones, but covering also subtle optimizations based on bidirectional analyses and edge-splitting program optimizations. I argue that proof transformability is essentially a logical version of optimization soundness; each entails the other. (Joint work with Ando Saabas.)