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.

2014-02-25: Seminar Reeves (University of Waikato, Hamilton) on Adding Visualisations to Formal Models of Interactive Medical Devices

Creating formal models of interactive medical devices, such as infusion pumps, allows us to perform important checks to ensure that both the functionality of the device and its interaction possibilities correctly support requirements. As these are safety-critical devices errors can be potentially fatal. We often want to be able to demonstrate aspects of behaviour from the models to medical practitioners, bio-technicians, device manufacturers etc. who are not typically familiar with the languages and notations of our models. The best way to communicate with these people is via simulations of the device, however developing such simulations is time-consuming and error-prone. In this paper we describe ongoing work which looks at ways of creating visualisations and simulations directly from the formal models as a way of addressing this problem.

2014-02-18: NSW Big Picture Seminar Franklin (University of California, Berkeley) on The Berkeley Data Analytics Stack: Present and Future
This talk will outline the AMPLab's research approach and describe how we have integrated the three main resources available to address the cross-disciplinary nature of Big Data challenges: Algorithms (such as machine learning and statistical techniques), Machines (in the form of scalable clusters and elastic cloud computing), and People (individually as analysts and as crowds).

2014-01-16: Seminar Clarke & Osterweil (University of Massachusetts Amherst) on Process-based Security Analysis for Human-intensive Systems

This talk describes a process-model based, systematic approach for detecting security vulnerabilities in human-intensive systems. Such systems typically involve complex interaction and cooperation among software applications, hardware devices, and human participants, and are increasingly central to key societal infrastructure.Thus, protecting such systems from attack is correspondingly centrally important. Clarke and Osterweil view is that these systems can be viewed as collections of processes whose security can be improved by modelling, analysing, and subsequently using the feedback gained to support continuous improvement. Their work features a process-modelling notation, with rich and well-defined semantics, that is able to represent the complexity of such systems as well as be the subject of rigorous analysis, such as model checking and fault-tree analysis. In this talk, Clarke and Osterweil will describe how they applied their approach to models of election processes used in Yolo and Marin Counties in California, show how their analyses have identified some example vulnerabilities, and indicate the kinds of improvements that can reduce vulnerabilities. Although no system can ever be made immune to any possible attack, Clarke and Osterweil believe that their approach of using technology to support continuous improvement represents an effective way to address the urgent need to protect the key infrastructure.