Publications

Avvenuti M, Bernardeschi C, Francesco ND, Masci P.  2009.  A tool for checking secure interaction in Java Cards. Proceedings of the 12th European Workshop on Dependable Computing, EWDC 2009 12th European Workshop on Dependable Computing, EWDC 2009. :8pages. Abstract

We present an approach based on a multilevel security policy and the theory of abstract interpretation for checking secure interaction between applications in Java Cards. The security policy is defined by the user, which assigns security levels to Java Card applications. Actual values are abstracted into security levels, and an abstract interpreter executes the bytecode of applications in the abstract domain. We show JCSI, a tool that implements the presented approach. JCSI can be used to check the binary code of Java Card.

Bernardeschi C, Masci P, Pfeifer H.  2009.  Analysis of Wireless Sensor Network Protocols in Dynamic Scenarios. SSS09, the 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems. 5873:105–119. Abstract

We describe an approach to the analysis of protocols for wireless sensor networks in scenarios with mobile nodes and dynamic link quality. The approach is based on the theorem proving system PVS and can be used for formal specification, automated simulation and verification of the behaviour of the protocol. In order to demonstrate the applicability of the approach, we analyse the reverse path forwarding algorithm, which is the basic technique used for diffusion protocols for wireless sensor networks.

Masci P, Tedeschi A.  2009.  Modelling and Evaluation of a Game-Theory Approach for Airborne Conflict Resolution in Omnet++. 2nd International Conference on Dependability (DEPEND09). :162–165. Abstract

Airborne self-separation is an air-traffic management concept in which pilots are allowed to select the optimal route for the aircraft in real time. In such environments, pilots are assisted by an airborne system that detects possible route conflicts with neighbouring aircraft and gives advice for maneuvering solutions to avoid conflicts. In this paper, we evaluate a game-theory approach for conflict resolutions between aircraft.We modelled the aircraft in a well established simulation framework. Preliminary results give an insight into the dependability of the approach when dealing with the lossy nature of the wireless environment.

Bernardeschi C, Masci P, Pfeifer H.  2008.  Early Prototyping of Wireless Sensor Network Algorithms in PVS. SAFECOMP. :346–359. Abstract

We describe an approach of using the evaluation mechanism of the specification and verification system PVS to support formal design exploration of WSN algorithms at the early stages of their development. The specification of the algorithm is expressed with an extensible set of programming primitives, and properties of interest are evaluated with ad hoc network simulators automatically generated from the formal specification. In particular, we build on the PVSio package as the core base for the network simulator. According to requirements, properties of interest can be simulated at different levels of abstraction. We illustrate our approach by specifying and simulating a standard routing algorithm for wireless sensor networks.

Masci P, Moniz H, Tedeschi A.  2008.  Services for fault-tolerant conflict resolution in air traffic management. SERENE '08: Proceedings of the 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems. :121–125. Abstract

Airborne Self-Separation is a new concept of dynamic management of air traffic flow, where pilots are allowed to select their flight paths in real-time. In this new operational concept, each aircraft is guided by an automated decision procedure and, based on the available information, enters into negotiations with surrounding aircraft in order to coordinate actions and avoid collisions. In this work, we explore the possibility of combining an approach based on Satisficing Game Theory together with fault-tolerant protocols to obtain a robust approach for conflict resolution and air traffic optimization in the context of Airborne Self-Separation.

Avvenuti M, Corsini P, Masci P, Vecchio A.  2007.  Opportunistic computing for wireless sensor networks. Mobile Adhoc and Sensor Systems, 2007. MASS 2007. IEEE Internatonal Conference on. :1–6. Abstract

Wireless sensor networks are moving from academia to real world scenarios. This will involve, in the near future, the design and production of hardware platforms characterized by low-cost and small form factor. As a consequence, the amount of resources available on a single node, i.e. computing power, storage, and energy, will be even more constrained than today. This paper faces the problem of storing and executing an application that exceeds the memory resources available on a single node. The proposed solution is based on the idea of partitioning the application code into a number of opportunistically cooperating modules. Each node contributes to the execution of the original application by running a subset of the application tasks and providing service to the neighboring nodes.

Corsini P, Masci P, Vecchio A.  2006.  Configuration and tuning of sensor network applications through virtual sensors. PerCom Workshops. :316–320. Abstract

Writing software for sensor networks requires full understanding of the physical phenomenon under observation. Nevertheless, in many cases knowing the details of the area of operation is difficult or unfeasible. This leads to the necessity of configuring and tuning the application executed on the sensor nodes even after the network has been deployed. We present a solution where a layer of computation is inserted between the application and the sensing equipment. This layer acts like a tiny interpreter and can be used to customize the behavior of already running applications. Experimental validation of the architecture and examples of use are also shown.

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.

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.