Recent Publications

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.
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

Coelho F, Matos M, Pereira JO, Oliveira R.  2017.  Similarity Aware Shuffling for the Distributed Execution of SQL Window Functions : BPA. Distributed Applications and Interoperable Systems - 17th IFIP WG 6.1 International Conference, DAIS 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 1. :3–18. Abstract

n/a

Maia F, Paulo J, Coelho F, Neves F, Pereira JO, Oliveira R.  2017.  DDFlasks: Deduplicated Very Large Scale Data Store. Distributed Applications and Interoperable Systems - 17th IFIP WG 6.1 International Conference, DAIS 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 1. :51–66. Abstract

n/a

Masci P, Zhang Y, Jones P, Campos JC.  2017.  A Hazard Analysis Method for Systematic Identification of Safety Requirements for User Interface Software in Medical Devices. 15th International Conference on Software Engineering and Formal Methods (SEFM 2017). LNCS, volume 10469, Springer Abstractsefm17-cameraready.pdf

Formal methods technologies have the potential to verify the usability and safety of user interface (UI) software design in medical devices, enabling significant reductions in use errors and consequential safety incidents with such devices. This however depends on comprehensive and verifiable safety requirements to leverage these techniques for detecting and preventing flaws in UI software that can induce use errors. This paper presents a hazard analysis method that extends Leveson's System Theoretic Process Analysis (STPA) with a comprehensive set of causal factor categories, so as to provide developers with clear guidelines for systematic identification of use-related hazards associated with medical devices, their causes embedded in UI software design, and safety requirements for mitigating such hazards. The method is evaluated with a case study on the Gantry-2 radiation therapy system, which demonstrates that 1) as compared to standard STPA, our method allowed us to identify more UI software design issues likely to cause use-related hazards; and 2) the identified UI software design issues facilitated the definition of precise, verifiable safety requirements for UI software, which could be readily formalized in verification tools such as Prototype Verification System (PVS).