Abstract
The IVY workbench is a model-based tool for the formal modelling and verification of interactive systems. The tool uses model checking to carry out the verification step. The goal is not to replace, but to complement more exploratory and iterative user-centred design approaches. However, the need for formal and rigorous modelling and reasoning raises challenges for the integration of both approaches. This paper presents a new plugin that aims to provide support for the integration of the formal methods based analysis supported by the tool, with user-centred design. The plugin is described, and an initial validation of its functionalities presented.

Abstract

Abstract
This document presents the case study for the ABZ 2023 conference. The case study introduces a safety critical interactive system called AMAN (Arrival MANager), which is a partly-autonomous scheduler of landing sequences of aircraft in airports. This interactive systems interleaves Air Traffic Controllers activities with automation in AMAN. While some AMAN systems are currently deployed in airports, we consider here only a subset of functions which represent a challenge in modelling and verification.

Abstract
For the average programmer, adjunctions are (if at all known) more respected than loved. At best, they are regarded as an algebraic device of theoretical interest only, not useful in common practice. This paper is aimed at showing the opposite: that adjunctions underlie most of the work we do as programmers, in particular those using the functional paradigm. However, functions alone are not sufficient to express the whole spectrum of programming, with its dichotomy between specifications—what is (often vaguely) required—and implementations—how what is required is (hopefully well) implemented. For this, one needs to extend functions to relations. Inspired by the pioneering work of Ralf Hinze on “adjoint (un)folds”, the core of the so-called (relational) Algebra of Programming is shown in this paper to arise from adjunctions. Moreover, the paper also shows how to calculate recursive programs from specifications expressed by Galois connections—a special kind of adjunction. Because Galois connections are easier to understand than adjunctions in general, the paper adopts a tutorial style, starting from the former and leading to the latter (a path usually not followed in the literature). The main aim is to reconcile the functional programming community with a concept that is central to software design as a whole, but rarely accepted as such. © 2023, Springer Nature Switzerland AG.

Abstract
The notion of a difunction was introduced by Jacques Riguet in 1948. Since then it has played a prominent role in database theory, type theory, program specification and process theory. The theory of difunctions is, however, less known in computing than it perhaps should be. The main purpose of the current paper is to give an account of difunction theory in relation algebra, with the aim of making the topic more mainstream.As is common with many important concepts, there are several different but equivalent characterisations of difunctionality, each with its own strength and practical significance. This paper compares different proofs of the equivalence of the characterisations. A well-known property is that a difunction is a set of completely disjoint rectangles. This property suggests the introduction of the (general) notion of the core of a relation; we use this notion to give a novel and, we believe, illuminating characterisation of difunctionality as a bijection between the classes of certain partial equivalence relations.& COPY; 2023 The Authors. Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons .org /licenses /by /4 .0/).

Abstract
There is a growing demand for persistent data in IoT, edge and similar resource-constrained devices. However, standard FLASH memory-based solutions present performance, energy, and reliability limitations in these applications. We propose MRAM persistent memory as an alternative to FLASH based storage. Preliminary experimental results show that its performance, power consumption, and reliability in typical database workloads is competitive for resource-constrained devices. This opens up new opportunities, as well as challenges, for small-scale database systems. MRAM is tested for its raw performance and applicability to key-value and relational database systems on resource-constrained devices. Improvements of as much as three orders of magnitude in write performance for key-value systems were observed in comparison to an alternative NAND FLASH based device. © 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).