2014-03-28 Engineering Panel of the Marsden Fund
Professor Gernot Heiser accepted invitation to Engineering Panel of the Marsden Fund, NZ equivalent of ARC Discovery More...

2014-03-25: Seminar Venugopal (UNSW) on Towards a Unified View of Elasticity

The defining feature of cloud computing is elasticity, or the ability to add and remove resources at will. Elasticity has created interesting opportunities for research into resource provisioning, fault tolerance, and scalability. However, most of the current research into elasticity has focussed on linear scaling of application logic without reference to management of state information. Additionally, current solutions for scaling applications relies on centralised control using threshold-based rules. This talk will focus on research performed in UNSW on decentralised and autonomic scaling of applications on cloud resources. It will describe a scaling mechanism that learns application performance characteristics in order to make decisions on adding or removing cloud resources. It will also touch upon our efforts on elastically scaling the persistence layer. This talk will end with some thoughts on presenting a unified view of elasticity across the entire application stack.

2014-03-21: Seminar Nestmann (TU Berlin) on Dynamic Coalitions and Dynamic Event Structures

Dynamic Coalitions essentially represent a coordination principle, where hierarchically nested sets are equipped with a notion of dynamic membership. Challenges, however, arise from extensions by further dimensions with, for example, private data and corresponding access policies. Dynamic Event Structures were developed in order to support the formation of Dynamic Coalitions. The first part of the talk provides an overview of our current work in this area. The second part focuses on some of the technical aspects of Dynamic Event Structures.

2014-03-18: Seminar Luttik (TU Eindhoven) on Unique Parallel Decomposition

A recurring question in process theory is to what extent the behaviours definable in a certain process calculus have a unique decomposition into indecomposable parallel components. Milner and Moller were the first to consider the unique decomposition property in a process calculus for specifying simple finite behaviours. Since then, the property has been re-established several times for different process calculi, each time using a variant of the same proof idea, and most recently for a fragment of the applied pi-calculus. Bas Luttik will present and discuss an abstract theory of unique decomposition in commutative monoids that is tailored towards application in process theory, explain how the theory can be straightforwardly applied to establish unique parallel decomposition in process calculi modulo strong bisimilarity, and how an adaptation facilitates application in settings modulo weak and branching bisimilarity.

2014-03-14: Seminar Futatsugi (JAIST) on Generate & Check Method for Verification of Transition Systems

Effective coordination of inference (a la theorem proving) and search (a la model checking) is one of the most important and interesting research topics in formal methods. We have developed several techniques for coordinating inference and search for verification with proof scores in CafeOBJ. The generate & check method is a recent development of this kind in verification of transition systems with CafeOBJ. The method is based on (1) state representations with state patterns, and (2) systematic generation of finite state patterns which subsume all possible infinite states. This talk explains the generate & check method using a simple but non-trivial example of mutual exclusion protocols.