TS News

News

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-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-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.

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.

A further 150K external funding was approved for AURIN/HTS project to integrate HTS data on the national map
2014-01-01 A paper titled Improved device driver reliability through hardware verification reuse has been accepted for publication in the 16^th ASPLOS Conference. The paper is the result of a collaboration with Intel (Hillsboro, OR) lead by SSRG researcher Leonid Ryzhyk.

Show older articles

Trustworthy Systems

News