|
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-01
A paper titled Improved
device driver reliability through hardware verification
reuse has been accepted for publication in the
16th
ASPLOS Conference. The paper is the result of a
collaboration with Intel (Hillsboro, OR) lead by SSRG
researcher Leonid Ryzhyk.
|
|
A further 150K external funding was approved for
AURIN/HTS project to integrate HTS data on the national
map
|
|
2013-12-17: Seminar Bourke (INRIA & ENS - Paris) on
Mechanization of a mesh network routing protocol & the
proof of its loop freedom in Isabelle/HOL
|
|
This talk describes recently completed work to transfer a
formal but pencil-and-paper model and analysis of a
wireless mesh network protocol (AODV) into the proof
assistant Isabelle/HOL. The nodes of such networks are
reactive systems that cooperate to provide a global
service (the sending of messages from node to node)
satisfying certain correctness properties (messages are
never sent in circles).
|
