Recent Publications

Cledou G, Nakajima S.  2019.  A Net-Based Formal Framework for Causal Loop Diagrams. Complex Systems Design {&} Management Asia. :1–12. Abstractcsdm2018.pdf

Causal Loop Diagrams (CLDs) are a modeling tool employed in Business Dynamics. Such a diagram consists of many tightly coupled loops to capture dynamic behavior of systems. Intuitive operational semantics, describing how changes are propagated among the loops, provide a basis for model animation or manual inspection. They are, however, not precise enough to enable automated property checking. This paper proposes and defines a net-based formal framework, showing true concurrency, so that automated analysis is made possible.

Santos A, Cunha A, Macedo N.  2019.  Static-time Extraction and Analysis of the ROS. Abstractros_model.pdf

The Robot Operating System (ROS) is one of the most popular open source robotic frameworks, and has contributed significantly to the fast development of robotics. Even though ROS provides many ready-made components, a robotic system is inherently complex, in particular regarding the architecture and orchestration of such components. Availability and analysis of a system’s architecture at compile time is fundamental to ease comprehension and development of higher-quality software. However, ROS developers have to overcome this complexity relying mostly on testing and runtime visualisers. This work aims to enhance static-time support by proposing, firstly, a metamodel to describe the software architecture of ROS systems (the ROS Computation
Graph) and, secondly, model extraction and visualisation tools for such architectural models. The provided tools allow users to specify custom-made queries over these models, enabling the static verification of relevant properties that had to be (manually) checked at runtime before.

Lourenço CB, Frade MJ, Pinto JS.  2019.  A generalized program verification workflow based on loop elimination and {SA} form. Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE 2019, Montreal, QC, Canada, May 27, 2019.. :75–84. Abstractmain.pdf

This paper presents a minimal model of the func- tioning of program verification and property checking tools based on (i) the encoding of loops as non-iterating programs, either conservatively, making use of invariants and assume/assert commands, or in a bounded way; and (ii) the use of an intermediate single-assignment (SA) form. The model captures the basic workflow of tools like Boogie, Why3, or CBMC, building on a clear distinction between operational and axiomatic semantics. This allows us to consider separately the soundness of program annotation, loop encoding, translation into SA form, and verification condition (VC) generation, as well as appropriate notions of completeness for each of these processes.
To the best of our knowledge, this is the first formalization of a bounded model checking of software technique, including soundness and completeness proofs using Hoare logic; we also give the first completeness proof of a deductive verification tech- nique based on a conservative encoding of invariant-annotated loops with assume/assert in SA form, as well as the first soundness proof based on a program logic.

Cledou G, Proença J, Sputh BHC, Verhulst E.  2019.  Coordination of Tasks on a Real-Time OS. Coordination Models and Languages. :250–266. Abstract

VirtuosoNext{\$}{\$}^{\{}{\backslash}text {\{}TM{\}}{\}}{\$}{\$}is a distributed real-time operating system (RTOS) featuring a generic programming model dubbed Interacting Entities. This paper focuses on these interactions, implemented as so-called Hubs. Hubs act as synchronisation and communication mechanisms between the application tasks and implement the services provided by the kernel as a kind of Guarded Protected Action with a well defined semantics. While the kernel provides the most basic services, each carefully designed, tested and optimised, tasks are limited to this handful of basic hubs, leaving the development of more complex synchronization and communication mechanisms up to application specific implementations. In this work we investigate how to support a programming paradigm to compositionally build new services, using notions borrowed from the Reo coordination language, and relieving tasks from coordination aspects while delegating them to the hubs. We formalise the semantics of hubs using an automata model, identify the behaviour of existing hubs, and propose an approach to build new hubs by composing simpler ones. We also provide tools and methods to analyse and simplify hubs under our automata interpretation. In a first experiment several hub interactions are combined into a single more complex hub, which raises the level of abstraction and contributes to a higher productivity for the programmer. Finally, we investigate the impact on the performance by comparing different implementations on an embedded board.

Bernardeschi C, Masci P, Santone A.  2018.  Data Leakage in Java applets with Exception Mechanism. Proceedings of Italian Conference on Cyber-Security (ITASEC18). CEUR Workshop Proceedings (2018, to appear)santone.pdf
Bernardeschi C, Masci P, Caramella D, Dell'Osso R.  2018.  The benefits of using interactive device simulations as training material for clinicians: an experience report with a contrast media injector used in CT. Medical Cyber Physical Systems Workshop 2018. SIGBED Review newsletter (2018, to appear)stellant-v3.pdf
Silva CC, Masci P, Zhang Y, Jones P, Campos JC.  2018.  A Use Error Taxonomy for Improving Human-Machine Interface Design in Medical Devices. Medical Cyber Physical Systems Workshop 2018. SIGBED Review newsletter (2018, to appear)mcps-taxonomy-v3g.pdf
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.