Recent Publications

Broccia G, Masci P, Milazzo P.  2018.  Modeling and Analysis of Human Memory Load in Multitasking Scenarios. 10th ACM SIGCHI Symposium on Engineering Interactive Computing Systems (EICS 2018). Abstracteics18d-camera-ready.pdf

This paper presents on-going work developing a formal framework for the model-based analysis of human-machine interaction in multiple critical systems. The framework builds on classical results from applied psychology on selective attention and working memory. The framework is intended for developers of interactive critical systems to identify plausible human multitasking strategies that are likely to be adopted by operators when using multiple interactive systems at the same time, and to estimate the memory load necessary to complete concurrent tasks. This type of analysis is especially useful at the early stages of system design, to better understand the effort necessary to operate the system when an implementation or a prototype of the system is unavailable. The analysis can also be used retrospectively, to analyse already implemented systems and complement results from user studies. An example based on infusion pumps, used in chemotherapy to infuse doses over a period, is employed to demonstrate the utility of the framework. The framework makes it possible to model the interactive tasks necessary to configure the pumps and start the infusion. The results of the analysis indicate situations where the operator is unable to carry out the task because of omission errors. These results are in line with experimental results reported in the literature, and may provide more detailed hypotheses that can be validated experimentally.

Shoker A.  2018.  Brief Announcement: Sustainable Blockchains through Proof of eXercise.. ACM Symposium on Principles of Distributed Computing (PODC). Abstractpox-podc.pdf

n/a

Masci P, Harrison MD, Campos JC.  2018.  Formal modelling as a component of user centred design. Workshop on Formal Methods for Interactive Systems (FMIS-2018), Springer LNCS, to appear. Abstractfmis18rev2-camera-ready.pdf

User centred design approaches typically focus understanding on context and producing sketch designs. These sketches are often non functional (e.g., paper) prototypes. They provide a means of exploring candidate design possibilities using techniques such as cooperative evaluation. This paper describes a further step in the process using formal analysis techniques. The sketch design of a device is enhanced into a specification that is then analysed using formal techniques, thus providing a systematic approach to checking plausibility and consistency during early design stages. Once analysed, a further prototype is constructed using an executable form of the specification, providing the next candidate for evaluation with potential users. The technique is illustrated through an example based on a pill dispenser.

Anzivino S, Quaini G, Pisetta V, Masci P, Bertoldi A, Nollo G.  2018.  Implementation of a multi-specialized electronic health record for managing cardiological rehabilitation paths. Italian Forum of Ambient Assisted Living (ForItALL). Abstractforitaal_2018_paper_6.pdf

Cardiac Rehabilitation (CR) is an intervention for managing the post-acute phase of the disease.
According to international guidelines, it includes three consecutive phases: the first phase, during
the acute period, in the hospital; the second, during a hospitalization or in outpatient, in order to
evaluate and modify the patient's risk factors; the third, outside the hospital setting, is carried out to
change, support and promote a correct lifestyle. To guarantee that all patients have access to the
most appropriate rehabilitation track, it is necessary to create structured paths on the territory and
under a multi-professional patient monitoring. The elective tool for patient-centered management is
the Integrated Care Pathway (ICP). It is oriented to the communication and integration of all actors
involved in patient’s management, requires the identification of a case manager and a team of
health professionals able to manage complexity and comorbidities, and supports patient
involvement. Care pathways as complex as these can be better supported if traditional paper-
based approaches are transformed into interactive systems that use Information and
Communication Technologies (ICT). The introduction of ICP and ICT implies the reconfiguration of
the clinical record that from a repository of the data becomes a multi-accessible tool for the
management of visits and the visualization of the results of instrumental examinations. In order to
translate this concept in the field of the CR at patient’s home, we created a multi-specialist
electronic health record accessible to both professionals (cardiologist, nurse, dietician,
psychologist, sanitary assistant) that make diagnosis, prescribe therapies and physical exercise,
monitor patient’s parameters, and patients, to allow them to consult therapies and results of clinical
exams. We used Agile Methodology to develop this Medical Device (MD) compliant, by design,
with the European laws on MD, Privacy, and Usability. To avoid malfunctions due
to incorrect or incomplete collection of requirements, and to optimize development time, the Agile
continuous process of revision and brainstorming were performed by applying simulation
technologies [6] that allowed us to accelerate substantially the identification and validation of user
interface requirements and to identify and fix potential functional errors. The virtual prototypes
reproducing the functionalities and the visual appearance of the system were subjected to the CR’s
multidisciplinary team of Azienda Provinciale per i Servizi Sanitari di Trento (professionals,
engineers, etc.) involved in the project during several “sprint phases” as an alternative tool to the
static mock-ups. All this led to the implementation of a MD validated by design.

Palmieri M, Bernardeschi C, Masci P.  2018.  A Flexible Framework for FMI-based Co-Simulation of Human-Centred Cyber-Physical Systems. 2nd Workshop on Formal Co-Simulation of Cyber-Physical Systems (CoSim-CPS-18), Springer LNCS, 2018 (to appear). Abstractcosim-cps-18_paper_4-full.pdf

This paper presents our on-going work on developing a flexible framework for formal co-simulation of human-centred cyber-physical systems. The framework builds on and extends an existing prototyping toolkit, adding novel functionalities for automatic generation of user interface prototypes equipped with a standard FMI-2 co-simulation interface. The framework is developed in JavaScript, and uses a flexible templating mechanism for converting stand-alone device prototypes into Functional Mockup Units (FMUs) capable of exchanging commands and data with any FMI-compliant co-simulation engine. Two concrete examples are presented to demonstrate the capabilities of the framework.

Bessa R, Coelho F, Rodrigues X, Alonso A, Soares T, Pires G, Matos P, Prates I, Shahrokni H, Mäkivierikko A.  2018.  GRID AND MARKET HUB: EMPOWERING LOCAL ENERGY COMMUNITIES IN INTEGRID.
Lourenço CB, Frade MJ, Nakajima S, Pinto JS.  2018.  A Generalized Approach to Verification Condition Generation. 2018 {IEEE} 42nd Annual Computer Software and Applications Conference, {COMPSAC} 2018, Tokyo, Japan, 23-27 July 2018, Volume 1. :194–203. Abstractmain.pdf

In a world where many human lives depend on the correct behavior of software systems, program verification as- sumes a crucial role. Many verification tools rely on an algorithm that generates verification conditions (VCs) from code annotated with properties to be checked. In this paper, we revisit two major methods that are widely used to produce VCs: predicate transformers (used mostly by deductive verification tools) and the conditional normal form transformation (used in bounded model checking of software). We identify three different aspects in which the methods differ (logical encoding of control flow, use of contexts, and semantics of asserts), and show that, since they are orthogonal, they can be freely combined. This results in six new hybrid verification condition generators (VCGens), which together with the fundamental methods constitute what we call the VCGen cube. We consider two optimizations implemented in major program verification tools and show that each of them can in fact be applied to an entire face of the cube, resulting in optimized versions of the six hybrid VCGens. Finally, we compare all VCGens empirically using a number of benchmarks. Although the results do not indicate absolute superiority of any given method, they do allow us to identify interesting patterns.

Harrison M, Masci P, Campos JC, Curzon P.  2017.  Demonstrating that medical devices satisfy user related safety requirements. Software Engineering in Healthcare (FHIES/SEHC 2014). 9062 Abstractharrison-fhies14.pdf

One way of contributing to a demonstration that a medical device is acceptably safe is to show that the device satisfies a set of requirements known to mitigate hazards. This paper describes experience using formal techniques to model an IV infusion device and to prove that the modelled device captures a set of requirements. The requirements chosen for the study are based on a draft proposal developed by the US Food and Drug Administration (FDA). A major contributor to device related errors are (user) interaction errors. For this reason the chosen models and requirements focus on user interface related issues.

Fayollas C, Martinie C, Palanque P, Masci P, Harrison M, Campos JC, Silva SR.  2017.  Evaluation of formal IDEs for human-machine interface design and analysis: the case of CIRCUS and PVSio-web. Proceedings of the Third Workshop on Formal Integrated Development Environment. 240:1-19. Abstract1701.08465.pdf

n/a

Coelho F, Paulo J, Vilaça R, Pereira JO, Oliveira R.  2017.  HTAPBench: Hybrid Transactional and Analytical Processing Benchmark. Proceedings of the 8th ACM/SPEC on International Conference on Performance Engineering. :293–304. Abstract
n/a
Enes V, Moreno CB, Almeida PS, Leitão J.  2017.  Borrowing an Identity for a Distributed Counter. PaPoC '17 Proceedings of the 3rd Workshop on the Principles and Practice of Consistency for Distributed Data. a5-enes.pdf
Younes G, Almeida PS, Moreno CB.  2017.  Compact Resettable Counters through Causal Stability. PaPoC '17 Proceedings of the 3rd Workshop on the Principles and Practice of Consistency for Distributed Data. a3-younes.pdf
Cledou G, Proença J, Barbosa L.  2017.  Composing Families of Timed Automata. 7th IPM International Conference on Fundamentals of Software Engineering. Abstractifta.pdf

n/a