Abstract

Abstract

Abstract
Use error due to user interface design defects is a major concern in many safety critical domains, for example avionics and health care. Early detection of latent user interface problems can be facilitated by user-centered design methods that integrate formal verification technologies. This article considers the role that formal verification technologies can play in the context of user-centered design by considering the following three existing tools: CIRCUS, PVSio-web, and IVY. These tools have been developed to support the model based analysis of critical user interfaces. They have their foundations in existing formal verification technologies, but each of them is focused towards particular issues relating to user interface design. The article explores the different phases of the user-centered design process and the extent to which each of these tools supports these phases. Criteria are developed for assessing their role at each stage of the design process. The results of the evaluation provide guidance to developers to help choose the most appropriate tool based on their analysis needs while at the same time setting challenges for future developments.

Abstract
We study a simple inductive data type for representing correct-by-construction matrices. Despite its simplicity, it can be used to implement matrix-manipulation algorithms efficiently and safely, performing in some cases faster than existing alternatives even though the algorithms are written in a direct and purely functional style. A rich collection of laws makes it possible to derive and optimise these algorithms using equational reasoning, avoiding the notorious off-by-one indexing errors when fiddling with matrix dimensions. We demonstrate the usefulness of the data type on several examples, and highlight connections to related topics in category theory. © 2020 ACM.

Abstract
A key issue in the performance of modern containerized distributed systems, such as big data storage and processing stacks or micro service based applications, is the placement of each container, or container pod, in virtual and physical servers. Although it has been shown that inter-application traffic is an important factor in placement decisions, as it directly indicates how components interact, it has not been possible to accurately monitor it in an application independent way, thus putting it out of reach of cloud platforms. In this paper we present an efficient black-box monitoring approach for detecting and building a weighted communication graph of collaborating processes in a distributed system that can be queried for various purposes, including adaptive placement. The key to achieving high detail and low overhead without custom application instrumentation is to use a kernel-aided event driven strategy. We evaluate a prototype implementation with micro-benchmarks and demonstrate its usefulness for container placement in a distributed data storage and processing stack (i.e., Cassandra and Spark).

Abstract
This paper presents Alloy4Fun, a web application that enables online editing and sharing of Alloy models and instances (including dynamic ones developed with the Electrum extension), to be used mainly in an educational context. By introducing secret paragraphs and commands in the models, Alloy4Fun allows the distribution and automated assessment of simple specification challenges, a mechanism that enables students to learn the language at their own pace. Alloy4Fun stores all versions of shared and analyzed models, as well as derivation trees that depict how they evolved over time: this wealth of information can be mined by researchers or tutors to identify, for example, learning breakdowns in the class or typical mistakes made by Alloy users. Alloy4Fun has been used in formal methods graduate courses for two years and for the latest edition we present results regarding its adoption by the students, as well as preliminary insights regarding the most common bottlenecks when learning Alloy (and Electrum). © Springer Nature Switzerland AG 2020.