Muffy Calder

Muffy Calder, Marion Oswald, Elizabeth McClory-Tiarks et al.

There is growing interest in the use of Large Language Models (LLMs) in policing, but there are potential risks. We have developed a practical approach to identifying risks, grounded in the policing and legal system of England and Wales. We identify 15 policing tasks that could be implemented using LLMs and 17 risks from their use, then illustrate with over 40 examples of impact on case progression. As good practice is agreed, many risks could be reduced. But this requires effort: we need to address these risks in a timely manner and define system wide impacts and benefits.

Oana Andrei, Muffy Calder, Matthew Chalmers et al.

We present a study using new computational methods, based on a novel combination of machine learning for inferring admixture hidden Markov models and probabilistic model checking, to uncover interaction styles in a mobile app. These styles are then used to inform a redesign, which is implemented, deployed, and then analysed using the same methods. The data sets are logged user traces, collected over two six-month deployments of each version, involving thousands of users and segmented into different time intervals. The methods do not assume tasks or absolute metrics such as measures of engagement, but uncover the styles through unsupervised inference of clusters and analysis with probabilistic temporal logic. For both versions there was a clear distinction between the styles adopted by users during the first day/week/month of usage, and during the second and third months, a result we had not anticipated.

Blair Archibald, Muffy Calder, Michele Sevegnani et al.

Human-autonomy teaming (HAT) scenarios feature humans and autonomous agents collaborating to meet a shared goal. For effective collaboration, the agents must be transparent and able to share important information about their operation with human teammates. We address the challenge of transparency for Belief-Desire-Intention agents defined in the Conceptual Agent Notation (CAN) language. We extend the semantics to model agents that are observable (i.e. the internal state of tasks is available), and attention-directing (i.e. specific states can be flagged to users), and provide an executable semantics via an encoding in Milner's bigraphs. Using an example of unmanned aerial vehicles, the BigraphER tool, and PRISM, we show and verify how the extensions work in practice.

Muffy Calder, Simon Dobson, Michael Fisher et al.

Sensor-driven systems are increasingly ubiquitous: they provide both data and information that can facilitate real-time decision-making and autonomous actuation, as well as enabling informed policy choices by service providers and regulators. But can we guarantee these system do what we expect, can their stake-holders ask deep questions and be confident of obtaining reliable answers? This is more than standard software engineering: uncertainty pervades not only sensors themselves, but the physical and digital environments in which these systems operate. While we cannot engineer this uncertainty away, through the use of models we can manage its impact in the design, development and deployment of sensor network software. Our contribution consists of two new concepts that improve the modelling process: frames of reference bringing together the different perspectives being modelled and their context; and the roles of different types of model in sensor-driven systems. In this position paper we develop these new concepts, illustrate their application to two example systems, and describe some of the new research challenges involved in modelling for assurance.

Oana Andrei, Muffy Calder, Matthew Chalmers et al.

This paper sets out a process of app analysis intended to support understanding of use but also redesign. From usage logs we infer activity patterns - Markov models - and employ probabilistic formal analysis to ask questions about the use of the app. The core of this paper's contribution is a bridging of stochastic and formal modelling, but we also describe the work to make that analytic core utile within a design team. We illustrate our work via a case study of a mobile app presenting analytic findings and discussing how they are feeding into redesign. We had posited that two activity patterns indicated two separable sets of users, each of which might benefit from a differently tailored app version, but our subsequent analysis detailed users' interleaving of activity patterns over time - evidence speaking more in favour of redesign that supports each pattern in an integrated way. We uncover patterns consisting of brief glances at particular data and recommend them as possible candidates for new design work on widget extensions: small displays available while users use other apps.

Oana Andrei, Muffy Calder, Matthew Higgs et al.

Software developers cannot always anticipate how users will actually use their software as it may vary from user to user, and even from use to use for an individual user. In order to address questions raised by system developers and evaluators about software usage, we define new probabilistic models that characterise user behaviour, based on activity patterns inferred from actual logged user traces. We encode these new models in a probabilistic model checker and use probabilistic temporal logics to gain insight into software usage. We motivate and illustrate our approach by application to the logged user traces of an iOS app.