Conference Papers

Cledou G, Barbosa L.  Submitted.  Modeling Families of Public Licensing Services: A Case Study. FME Workshop on Formal Methods in Software Engineering (FormaliSE). formalise2017.pdf
Neves F, Vilaça R, Pereira JO, Oliveira R.  Submitted.  Prepared Scan: Efficient Retrieval of Structured Data from HBase. {Proceedings of the Symposium on Applied Computing, Sac 2017, Marrakech, Morocco, April 3-7, 2017}. {Part F128005}:{462-464}. Abstractp462-neves.pdf

n/a

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

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