Abstract
The IVY workbench is a model-based tool that supports the formal verification of interactive computing systems. It adopts a plugin-based architecture to support a flexible development model. Over the years the chosen architectural solution revealed a number of limitations, resulting both from technological deprecation of some of the adopted solutions and a better understanding of the verification process to support. This paper presents the redesign and implementation of the original plugin infrastructure, originating a new version of the tool: IVY 2. It describes the limitations of the original solutions and the new architecture, which resorts to the Java module system in order to solve them.

Abstract
Formal verification has the potential to provide a level of evidence based assurance not possible by more traditional development approaches. For this potential to be fulfilled, its integration into existing practices must be achieved. Starting from this premise, the position paper discusses the opportunities created and the challenges faced by the use of formal verification in the analysis of critical interactive computing systems. Three main challenges are discussed: the accessibility of the modelling stage; support for expressing relevant properties; the need to provide analysis results that are comprehensible to a broad range of expertise including software, safety and human factors. Copyright © 2019 for this paper by its authors.

Abstract
Cyber-Physical Systems, as distributed systems of computational elements interacting with the physical world, are highly complex systems. They can, in many instances, be considered safety critical interactive systems, as errors in interaction can have disastrous consequences (consider the case of autonomous vehicles or integrated clinical environments). High assurance is, then, an underlying requirement, also at their user interface. In this position paper we identify five challenges to be solved both in the short and in the long term, regarding the modelling of (1) distributed and (2) heterogeneous interactive systems, (3) the analysis and relation between the different abstraction layers of Cyber-Physical Systems, (4) the modelling of real time/hybrid systems, and (5) the modelling of the dynamic nature of such systems. Solutions for these challenges are not presented, but possible directions are discussed. Copyright © 2019 for this paper by its authors.

Abstract

Abstract
The IVY Workbench is a tool that supports the modeling and formal verification of interactive systems. The tool features a set of plugins that support the modeling and analysis process, including a models editor, a properties checker, and a models animator. The latter, allows visualizing and interacting with a model, but does not support associating it with a prototype of the system. Interaction with the model facilitates its validation by modelling experts. It does not, however, facilitate communication with domain experts and users, to whom a prototype would be a more effective means of communication. This article presents the work done to remedy this gap in IVY. The article details the preliminary research carried out, architectural decisions and the obtained end result.

Abstract
Use error is one of the leading causes of medical device incidents. It is crucial for all stakeholders to have a unified means to better understand, classify, communicate, and prevent/avoid medical device use errors. In this paper, we present our ongoing work on developing a new use error taxonomy for medical devices that has the potential to enable fine-grained analysis of use errors and their root causes in system design. Our ultimate goal is to create a generic framework that can be used by medical device designers to better identify effective design solutions to mitigating use errors.