Journal Articles

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) Abstractcosim-tse17-preprint.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.pdf

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: (i) how to validate a model, and show that it is a faithful representation of the device; (ii) how to formalize requirements given in natural language, and demonstrate the benefits of the formalization process; (iii) 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.

Avvenuti M, Bernardeschi C, Francesco ND, Masci P.  2012.  JCSI: A tool for checking secure information flow in Java Card applications. Journal of Systems and Software. 85:2479-2493. Abstract

This paper describes a tool for checking secure information flow in Java Card applications. The tool performs a static analysis of Java Card CAP files and includes a CAP viewer. The analysis is based on the theory of abstract interpretation and on a multi-level security policy assignment. Actual values of variables are abstracted into security levels, and bytecode instructions are executed over an abstract domain. The tool can be used for discovering security issues due to explicit or implicit information flows and for checking security properties of Java Card applications downloaded from untrusted sources.

Bernardeschi C, Cassano L, Domenici A, Masci P.  2011.  Simulation and Test-Case Generation for PVS Specifications of Control Logics. International Journal on Advances in Software. 4 Abstract

We describe a framework for the simulation of control logics specified in the higher-order logic of the Prototype Verification System. The framework offers a library of predefined modules, a method for the composition of more complex modules, and an event-driven simulation engine. A developer defines a system architecture by composing its model out of library modules, possibly introducing new module definitions, and simulates the behaviour of the system model by providing its input waveforms, which are given as functions from time to logic levels. The generation of simulation scenarios (test cases) can be automated by using parametric waveforms that can be instantiated through universal and existential quantifiers. We demonstrate the simulation capabilities of our framework on two simple case studies from a nuclear power plant application. The main feature of this approach is that our formal specifications are executable. Moreover, once the simulation experiments give developers sufficient confidence in the correctness of the specification, the logic models can serve as the basis for its formal verification.

Bernardeschi C, Francesco ND, Lettieri G, Martini L, Masci P.  2008.  Decomposing bytecode verification by abstract interpretation. ACM Transactions on Programming Languages and Systems. 31(1):1-63. Abstract

Bytecode verification is a key point in the security chain of the Java platform. This feature is only optional in many embedded devices since the memory requirements of the verification process are too high. In this article we propose an approach that significantly reduces the use of memory by a serial/parallel decomposition of the verification into multiple specialized passes. The algorithm reduces the type encoding space by operating on different abstractions of the domain of types. The results of our evaluation show that this bytecode verification can be performed directly on small memory systems. The method is formalized in the framework of abstract interpretation.

Avvenuti M, Corsini P, Masci P, Vecchio A.  2007.  An application adaptation layer for wireless sensor networks. Pervasive and Mobile Computing. 3:413–438. Abstract

In wireless sensor networks, poor performance or unexpected behavior may be experienced for several reasons, such as trivial deterioration of sensing hardware, unsatisfactory implementation of application logic, or mutated network conditions. This leads to the necessity of changing the application behavior after the network has been deployed. Such flexibility is still an open issue as it can be achieved either at the expense of significant energy consumption or through software complexity. This paper describes an approach to adapt the behavior of running applications by intercepting the calls made to the operating system services and changing their effects at run-time. Customization is obtained through small fragments of interpreted bytecode, called adaptlets, injected into the network by the base station. Differently from other approaches, where the entire application is interpreted, adaptlets are tied only to specific services, while the bulk of the application is still written in native code. This makes our system able to preserve the compactness and efficiency of native code and to have little impact on the overall application performance. Also, applications must not be rewritten because the operating system interfaces are unaffected. The adaptation layer has been implemented in the context of TinyOS using an instruction set inspired to the Java bytecode. Examples that illustrate the programming of the adaptation layer are presented together with their experimental validation.

Avvenuti M, Corsini P, Masci P, Vecchio A.  2007.  Energy-efficient reception of large preambles in MAC protocols for wireless sensor networks. Electronics Letters. 43:300–301. Abstract

A technique able to significantly reduce the energy consumption of contention-based MAC protocols for wireless sensor networks is presented. Address and timing information is embedded into the packet preamble, allowing receivers to power off their radio during part of the transmission. Analytical and experimental evaluations show a significant extension of the network lifetime.

Bernardeschi C, Lettieri G, Martini L, Masci P.  2006.  Using postdomination to reduce space requirements of data flow analysis. Information Processing Letters. 98:11–18.
Bernardeschi C, Lettieri G, Martini L, Masci P.  2006.  Using Control Dependencies for Space-Aware Bytecode Verification. Computer Journal. 49:234–248. Abstract

Java applets run on a Virtual Machine that checks code integrity and correctness before execution using a module called the Bytecode Verifier. Java Card technology allows Java applets to run on smart cards. The large memory requirements of the verification process do not allow the implementation of an embedded Bytecode Verifier in the Java Card Virtual Machine. To address this problem, we propose a verification algorithm that optimizes the use of system memory by imposing an ordering on the verification of the instructions. This algorithm is based on control flow dependencies and immediate postdominators in control flow graphs.

Bernardeschi C, Lettieri G, Martini L, Masci P.  2005.  A Space-Aware Bytecode Verifier for Java Cards. Electronic Notes in Theoretical Computer Science. 141:237–254. Abstract

The bytecode verification is a key point of the security chain of the Java Platform. This feature is optional in many embedded devices since the memory requirements of the verification process are too high. In this paper we propose a verification algorithm that remarkably reduces the use of the memory by performing the verification during multiple specialized passes. The algorithm reduces the type encoding space by operating on different abstractions of the domain of types. The results of the experiments show that this bytecode verification can be performed directly on small memory systems.