Publications

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.

Zhang Y, Jones P, Masci P.  2015.  Model Based Design and Safety Analysis of Medical Device User Interfaces. Abstract

Plain Language Synopsis: This research applies model based engineering techniques to develop novel verification and hazard analysis methods, which help manufacturers establish the quality and safety in medical device user interface designs. Artifacts produced by these methods provide evidence for regulators to quickly and objectively assess the safety of devices' interaction with users.

Abstract: Designs of medical device Human Computer Interfaces (HCI) need to be robust and appropriately reactive to user actions. There is evidence that the HCI design of some devices on the market can cause use errors and erroneously process user input, which may subsequently lead to serious patient harm. Model based engineering (MBE) technology can be used to model HCI design decisions with mathematical precision. This technology can facilitate the development of HCI models that clearly define the device's interaction behavior with users; offering a formal (mathematical) basis to reason about and verify the safety of the design. Automatic tool support is available to facilitate such reasoning and verification activities. Tool artifacts provide manufacturers and regulators an objective and scientific basis for assessing the safety of medical device user interfaces. The authors have successfully applied MBE techniques to the analysis of medical device user interfaces in two studies. In the first study, automatic model extraction was applied to the user interface software of a marketed infusion pump to produce a model that resembles the pump's use interaction behavior. Automated formal proving on the model uncovered several design flaws in the pump's user interface that could lead to severe consequences including the pump ignoring key presses that might cause patient overdose. In the second study, the authors captured the user interface software design common in medical devices with a generic user interface model. Based on this generic model, a hazard analysis technique was proposed that integrates human cognition process models and general interaction design principles to guide more comprehensive and systematic identification of design flaws in user interfaces. Preliminary experiments showed that this hazard analysis technique can identify 3 times more software-related hazards in user interface designs, compared to standard hazard analysis techniques.

Masci P.  2014.  A preliminary hazard analysis for the GIP number entry software. Abstracttechrep-pha.pdf

The results of a preliminary hazard analysis are presented that identify common design errors in infusion pump software that may potentially cause use hazards. Many identified problems apply to other types of interactive medical devices, including ventilators and radiotherapy machines. The identified issues may be used as a basis to define safety requirements that, if satisfied by user interface software, can substantially improve the quality and safety of broad classes of medical devices

Bernardeschi C, Cassano L, Domenici A, Masci P.  2010.  Analysis of FPGAs Using the SAN Formalism. Technical Report, University of Pisa - Department of Information Engineering. Abstract

We describe a model of FPGA based systems realised with the Stochastic Activity Networks (SAN) formalism. The model can be used (i) to debug the FPGA circuit design synthesised from the high level description of the system, and (ii) to calculate the signal probabilities and transition densities of the FPGA circuit design, that can be used for reliability analysis, power consumption estimation and pseudo random testing of digital circuit design. We validate the model by reproducing results presented in other studies for some representative combinatorial circuits, and we explore the applicability of the model in the analysis of real-world devices by studying a circuit for the generation of CRC codes.