Publications

Corsini P, Masci P, Vecchio A.  2006.  VirtuS: a configurable layer for post-deployment adaptation of sensor network. ICWMC. :8. Abstract

Post-deployment adaptation of sensor networks is usually a necessity for several reasons, ranging from trivial deterioration of sensing hardware to unsatisfactory implementation of application logic. In this paper we present the architecture of VirtuS, a software component that can be incorporated into existing applications and remotely programmed to customize the behavior of sensor networks after deployment. Scenarios of use and experimental validation of the architecture are also included.

Avvenuti M, Corsini P, Masci P, Vecchio A.  2006.  Increasing the efficiency of preamble sampling protocols for wireless sensor networks. Proceedings of the First Mobile Computing and Wireless Communication International Conference, 2006. MCWC 2006.. :117–122. Abstract

Applications designed for event driven monitoring represent a challenging class of applications for wireless sensor networks. They are a special kind of monitoring applications, since they usually need low data rates, but also require mechanisms for low latency and asynchronous communication. In this paper we will focus on optimizations at the MAC layer that enable low energy consumption when contention-based protocols are adopted. We present B-MAC+, an enhanced version of a widely adopted MAC protocol, and we show that substantial improvements, in terms of network lifetime, can be reached over the original protocol.

Corsini P, Masci P, Vecchio A.  2006.  Experiences with the TinyOS Communication Library. Wireless Information Systems. :47-55. Abstract

TinyOS is a useful resource for developers of sensor networks. The operating system includes ready-made software components that enable rapid generation of complex software architectures. In this paper we describe the lessons gained from programming with the TinyOS communication library. In particular, we try to rationalize existing functionalities, and we present our solutions in the form of a communication library, called TComm-Lib.

Masci P.  2006.  Detecting data leakage in malicious Java applets. ReSIST Student Seminar. :81–84. Abstract

Web applets are programs dynamically loaded and executed inside the Internet browser of users' machine. They are used to extend the functionalities of web pages. Web applets can be associated with specific profiles granting access to information of users. As a consequence, web applets may possibly disclose, intentionally or by error, confidential information on public channels. We propose a technique to analyze the compiled code of web applets before execution. The technique is based on abstract interpretation. Data is associated with security levels and an iterative analysis is performed to trace information flows.

Bernardeschi C, Martini L, Masci P.  2004.  Java bytecode verification with dynamic structures. IASTED Conf. on Software Engineering and Applications. :559-564. Abstract

Java applets run on a Virtual Machine that checks code's integrity and correctness before execution using a module called Bytecode Verifier. Java Card technology allows Java applets to run on smart cards. Large memory space requirements of the verification process do not allow the implementation of a Bytecode Verifier embedded in the Java Card Virtual Machine. To address this feasibility problem, we propose a modified verification algorithm that optimizes the use of system memory. The algorithm, inspired to compilers techniques, partitions the code of the methods into control regions. In this way data structures can be dynamically allocated and the verification process can be applied locally to a subset of instructions.

Harrison M, Masci P, Campos JC.  2018.  Verification templates for the analysis of user interface software design. IEEE Transactions on Software Engineering (to appear). Abstractnewtemplates-r1v7b.pdfhttps://doi.org/10.1109/TSE.2018.2804939

The paper describes templates for model-based analysis of usability and safety aspects of user interface software design. The templates crystallize general usability principles commonly addressed in user-centred safety requirements, such as the ability to undo user actions, the visibility of operational modes, and the predictability of user interface behavior. These requirements have standard forms across different application domains, and can be instantiated as properties of specific devices. The modeling and analysis process is carried out using the Prototype Verification System (PVS), and is further facilitated by structuring the specification of the device using a format that is designed to be generic across interactive systems. A concrete case study based on a commercial infusion pump is used to illustrate the approach. A detailed presentation of the automated verification process using PVS shows how failed proof attempts provide precise information about problematic user interface software features.

Bernardeschi C, Domenici A, Masci P.  2017.  A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems. IEEE Transactions on Software Engineering. (In Press) Abstract07900400.pdfhttps://doi.org/10.1109/TSE.2017.2694423

This paper presents a methodology, with supporting tool, for formal modeling and analysis of software components in cyber-physical systems. Using our approach, developers can integrate a simulation of logic-based specifications of software components and Simulink models of continuous processes. The integrated simulation is useful to validate the characteristics and functionalities of discrete system components early in the development process. The same logic-based specifications can also be formally verified using the Prototype Verification System (PVS), to gain additional confidence that the software design is compliant with specific safety requirements. Modeling patterns are defined for generating the logic-based specifications from the more familiar automata-based formalism. The ultimate aim of this work is to facilitate the introduction of formal verification technologies in the software development process of cyber-physical systems, which typically requires the integrated use of different formalisms and tools. A case study from the medical domain is used throughout the paper to illustrate the approach. A PVS model of a pacemaker is interfaced with a Simulink model of the human heart. The overall cyber-physical system is co-simulated to validate design requirements through exploration of relevant test scenarios. Formal verification with the PVS theorem prover is demonstrated for the pacemaker model for specific safety aspects of the pacemaker design.

Harrison MD, Masci P, Campos JC, Curzon P.  2017.  Verification of User Interface Software: the Example of Use-Related Safety Requirements and Programmable Medical Devices. IEEE Transactions on Human-Machine Systems. Abstractmedthmsv10.pdfhttps://doi.org/10.1109/THMS.2017.2717910

One part of demonstrating that a device is acceptably safe, often required by regulatory standards, is to show that it satisfies a set of requirements known to mitigate hazards. This paper is concerned with how to demonstrate that a user interface software design is compliant with use-related safety requirements. A methodology is presented based on the use of formal methods technologies to provide guidance to developers about addressing three key verification challenges: 1) how to validate a model, and show that it is a faithful representation of the device; 2) how to formalize requirements given in natural language, and demonstrate the benefits of the formalization process; and 3) how to prove requirements of a model using readily available formal verification tools. A model of a commercial device is used throughout the paper to demonstrate the methodology. A representative set of requirements are considered. They are based on US Food and Drug Administration (FDA) draft documentation for programmable medical devices, and on best practice in user interface design illustrated in relevant international standards. The methodology aims to demonstrate how to achieve the FDA’s agenda of using formal methods to support the approval process for medical devices.

Harrison M, Campos JC, Masci P.  2015.  Reusing models and properties in the analysis of similar interactive devices. Innovations in Systems and Software Engineering. 11:95-111. Abstractharros.pdf

The paper is concerned with the comparative analysis of interactive devices. It compares two devices by checking systematically a set of template properties that are designed to explore important interface characteristics. The two devices are designed to support similar tasks in a clinical setting. The devices differ as a result of judgements based on a range of considerations including software. Variations between designs are often relatively subtle and do not always become evident through even relatively thorough user testing. Notwithstanding their subtlety, these differences may be important to the safety or usability of the device. The illustrated approach uses formal techniques to provide the analysis. This means that similar analysis can be applied systematically.

Furniss D, Masci P, Curzon P, Mayer A, Blandford A.  2015.  Exploring medical device design and use through layers of Distributed Cognition: How a glucometer is coupled with its context. Journal of Biomedical Informatics. 53:330-341. Abstractexploring-medical-device-use.pdfhttps://doi.org/10.1016/j.jbi.2014.12.006

Medical devices are becoming more interconnected and complex, and are increasingly supported by fragmented organizational systems, e.g. through different processes, committees, supporting staff and training regimes. Distributed Cognition has been proposed as a framework for understanding the design and use of medical devices. However, it is not clear that it has the analytic apparatus to support the investigation of such complexities. This paper proposes a framework that introduces concentric layers to DiCoT, a method that facilitates the application of Distributed Cognition theory. We use this to explore how an inpatient blood glucose meter is coupled with its context. The analysis is based on an observational study of clinicians using a newly introduced glucometer on an oncology ward over approximately 150h (11 days and 4 nights). Using the framework we describe the basic mechanics of the system, incremental design considerations, and larger design considerations. The DiCoT concentric layers (DiCoT-CL) framework shows promise for analyzing the design and use of medical devices, and how they are coupled with their context.

Masci P, Curzon P, Furniss D, Blandford A.  2015.  Using PVS to support the analysis of distributed cognition systems. Innovations in Systems and Software Engineering. 11(2):113-130. Abstractusing-pvs-for-dc.pdfhttps://doi.org/10.1007/s11334-013-0202-2

The rigorous analysis of socio-technical systems is challenging, because people are inherent parts of the system, together with devices and artefacts. In this paper, we report on the use of PVS as a way of analysing such systems in terms of Distributed Cognition. Distributed Cognition is a conceptual framework that allows us to derive insights about plausible user trajectories in socio-technical systems by exploring what information in the environment provides resources for user action, but its application has traditionally required substantial craft skill. DiCoT adds structure and method to the analysis of socio-technical systems from a Distributed Cognition perspective. In this work, we demonstrate how PVS can be used with DiCoT to conduct a systematic analysis. We illustrate how a relatively simple use of PVS can help a field researcher (i) externalise assumptions and facts, (ii) verify the consistency of the logical argument framed in the descriptions, (iii) help uncover latent situations that may warrant further investigation, and (iv) verify conjectures about potential hazards linked to the observed use of information resources. Evidence is also provided that formal methods and empirical studies are not alternative approaches for studying a socio-technical system, but that they can complement and refine each other. The combined use of PVS and DiCoT is illustrated through a case study concerning a real-world emergency medical dispatch system.

Masci P, Rukšėnas R, Oladimeji P, Cauchi A, Gimblett A, Li Y, Curzon P, Thimbleby H.  2015.  The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps. Innovations in Systems and Software Engineering. 11:73-93. Abstractmasci-predictability-isse2015.pdfhttps://doi.org/10.1007/s11334-013-0200-4

A demonstration is presented of how automated reasoning tools can be used to check the predictability of a user interface. Predictability concerns the ability of a user to determine the outcomes of their actions reliably. It is especially important in situations such as a hospital ward where medical devices are assumed to be reliable devices by their expert users (clinicians) who are frequently interrupted and need to quickly and accurately continue a task. There are several forms of predictability. A definition is considered where information is only inferred from the current perceptible output of the system. In this definition, the user is not required to remember the history of actions that led to the current state. Higher-order logic is used to specify predictability, and the Symbolic Analysis Laboratory (SAL) is used to automatically verify predictability on real interactive number entry systems of two commercial drug infusion pumps -- devices used in the healthcare domain to deliver fluids (e.g., medications, nutrients) into a patient’s body in controlled amounts. Areas of unpredictability are precisely identified with the analysis. Verified solutions that make an unpredictable system predictable are presented through design modifications and verified user strategies that mitigate against the identified issues.

Furniss D, Masci P, Curzon P, Mayer A, Blandford A.  2014.  7 Themes for guiding situated ergonomic assessments of medical devices: A case study of an inpatient glucometer. Applied Ergonomics. 45(6):1668-1677. Abstracthttps://doi.org/10.1016/j.apergo.2014.05.012

There is relatively little guidance on the situated ergonomic assessment of medical devices, and few case studies that detail this type of evaluation. This paper reports results of a detailed case study that focuses on the design and use of a modern blood glucose meter on an oncology ward. We spent approximately 150 h in-situ, over 11 days and 4 nights, performing observations and interviews with users. This was complemented by interviews with two staff with oversight and management responsibility related to the device. We identified 19 issues with the design and use of this device. These issues were grouped into 7 themes which can help guide the situated study of medical devices: usability, knowledge gaps and mental models, workarounds, wider tasks and equipment, the patient, connection between services, and policy.

Di Giandomenico F, Itria ML, Masci P, Nostro N.  2014.  Automated synthesis of dependable mediators for heterogeneous interoperable systems. Reliability Engineering & System Safety. 132:220-232. Abstractress.pdf

Approaches to dependability and performance are challenged when systems are made up of networks of heterogeneous applications/devices, especially when operating in unpredictable open-world settings. The research community is tackling this problem and exploring means for enabling interoperability at the application level. The EU project CONNECT has developed a generic interoperability mechanism which relies on the on-the-fly synthesis of CONNECTors, that is software bridges that enable and adapt communication among heterogeneous devices. Dependability and Performance are relevant aspects of the system. In our previous work, we have identified generic dependability mechanisms for enhancing the dependability of CONNECTors. In this work, we introduce a set of generic strategies for automating the selection and application of an appropriate dependability mechanism. A case study based on a global monitoring system for environment and security (GMES) is used as a means for demonstrating the approach.

Harrison M, Campos JC, Masci P.  2013.  Reusing models and properties in the analysis of similar interactive devices. Innovations in Systems and Software Engineering. 2(11):95-111. Abstractharrisoncm15-authorsversion.pdf

The paper is concerned with the comparative analysis of interactive devices. It compares two devices by checking a battery of template properties that are designed to explore important interface characteristics. The two devices are designed to support similar tasks in a clinical setting but differ in a number of respects as a result of judgements based on a range of considerations including software. Variations between designs are often relatively subtle and do not always become evident through even relatively thorough user testing. Notwithstanding their subtlety these differences may be important to the safety or usability of the device. The illustrated approach uses formal techniques to provide the analysis. This means that similar analysis can be applied systematically.