Publications

Masci P, Curzon P, Huang H, Ruksenas R, Blandford A, Furniss D, Rajkomar A.  2011.  Towards a formal framework for reasoning about the resilience of dynamic interactive systems. Proceedings of the 13th European Workshop on Dependable Computing (EWDC11). :109–110. Abstract

It is well known that systems built with resilient components are not necessarily resilient systems. Nevertheless, when studying the resilience of work systems characterised by continuous inter-operations among humans and devices, analysts generally concentrate only on localised interactions among humans and devices. Consequently they fail to capture the distributed nature of the mechanisms that guide interactions in dynamic interactive systems. In this paper, as a result of work on the resilience of medical systems with respect to human error, we propose a framework for reasoning about the resilience of complex dynamic interactive systems. To do this we exploit concepts from three different areas: the automated synthesis of resilient systems, formal methods for user-centred design, and distributed cognition.

Masci P, Curzon P.  2011.  Checking User-Centred Design Principles in Distributed Cognition Models: A Case Study in the Healthcare Domain. Information Quality in e-Health. 7058:95-108. Abstract

We propose a constructive procedure for building a distribut-ed cognition model of a system out of contextual / ethnographic data. We then show how such a model can be conveniently used for studying, in a repeatable and justifiable way, if a system correctly implements selected user-centred design principles. Our approach thus complements user studies in that it enables reasoning about the situated use of a teamwork system even before direct user involvement. We have applied our procedure to a healthcare case study. In particular, we have re-analysed a well-known adverse incident that led to a fatality and for which a comprehensive investigation report is in the public domain. By reasoning about the distributed cognition model, we identified several issues that were not addressed in the incident report nor in other subsequent analyses.

Masci P, Nostro N, Giandomenico F.  2011.  On Enabling Dependability Assurance in Heterogeneous Networks through Automated Model-Based Analysis. Software Engineering for Resilient Systems. 6968:78-92. Abstract

We present the specification of a basic library of dependability mechanisms that can be used within automated approaches for synthesising dependable connectors in heterogeneous networks. The library builds on classical dependability patterns, such as majority voting and retry, and uses the concept of overlay networks for triggering the synthesis of specific dependability mechanisms in the connector from high-level specifications. We translated such dependability mechanisms into SAN models with the aim to evaluate, through model-based analysis, which dependability mechanisms should be embedded in the synthesised connector for ensuring a given dependability level between networked systems willing to be connected. A case study is also presented to show the application of selected library mechanisms. This work is carried out in the context of connect, a European FET project which is investigating the possibility of enabling long-lasting inter-operation among networked systems by synthesising mediating connectors at run-time.

Bernardeschi C, Cassano L, Domenici A, Masci P.  2010.  Debugging PVS Specifications of Control Logics via Event-driven Simulation. Proc. 1st Intl. Conf. on Computational Logics, Algebras, Programming, Tools, and Benchmarking (ComputationTools2010). Abstract

In this paper, we present a framework aimed at simulating 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 simulates the specified system by providing its input waveforms as functions from time to logic levels. Once the simulation experiments give sufficient confidence in the correctness of the specification, the model can serve as a basis for the formal verification of desired properties of interest. A simple case study from a nuclear power plant application is shown. This paper is a contribution to research aimed at improving the development process of safety-critical systems by integrating simulation and formal specification methods.

Giandomenico FD, Kwiatkowska M, Martinucci M, Masci P, Qu H.  2010.  Dependability analysis and verification for CONNECTed systems. Proceedings of the 4th international conference on Leveraging applications of formal methods, verification, and validation - Volume Part II. :263–277. Abstract

The Connect project aims to enable the seamless composition of heterogeneous networked systems. In this context, Verification and Validation (V&V) techniques are sought to ensure that the Connected system satisfies dependability requirements. Stochastic model checking and state-based stochastic methods are two appealing V&V approaches to accomplish this task. In this paper, we report on the application of the two approaches in a typical Connect scenario. Specifically, we make clear (i) how the two approaches can be employed to enhance the confidence in the correctness of the analysis, and (ii) how the complementarity of these approaches can be fruitfully exploited to extend the analysis.

Masci P, Chiaradonna S, Giandomenico FD.  2010.  Dependability Analysis of Diffusion Protocols in Wireless Networks with Heterogeneous Node Capabilities. Proceedings of the 2010 European Dependable Computing Conference. :145–154. Abstract

Wireless networks are starting to be populated by interconnected devices that reveal remarkable hardware and software differences. This fact raises a number of questions on the applicability of available results on dependability-related aspects of communication protocols, since they were obtained for wireless networks with homogeneous nodes. In this work, we study the impact of heterogeneous communication and computation capabilities of nodes on dependability aspects of diffusion protocols for wireless networks. We build a detailed stochastic model of the logic layers of the communication stack with the SAN formalism. The model takes into account relevant real-world aspects of wireless communication, such as transitional regions and capture effect, and heterogeneous node capabilities. Dependability-related metrics are evaluated with analytical solutions techniques for small networks, while simulation is employed in the case of large networks.

Bertolino A, Di Giandomenico F, Marco DA, Issarny V, Martinelli F, Masci P, Matteucci I, Saadi R, Sabetta A.  2010.  Dependability in dynamic, evolving and heterogeneous systems: the Connect approach. Proc. 2nd International Workshop on Software Engineering for Resilient Systems (SERENE2010). Abstract

The EU Future and Emerging Technologies (FET) Project CONNECT aims at dropping the heterogeneity barriers that prevent the eternality of networking systems through a revolutionary approach: to synthesise on-the-fly the CONNECTors via which networked systems communicate. The CONNECT approach, however, comes at risk from the standpoint of dependability, stressing the need for methods and tools that ensure resilience to faults, errors and malicious attacks of the dynamically CONNECTed system. We are investigating a comprehensive approach, which combines dependability analysis, security enforcement and trust assessment, and is centred around a lightweight adaptive monitoring framework. In this project paper, we overview the research that we are undertaking towards this objective and propose a unifying workflow process that encompasses all the CONNECT dependability/security/trust concepts and models.

Bertolino A, Di Giandomenico F, Marco DA, Masci P, Sabetta A.  2010.  Metrics for QoS analysis in dynamic, evolving and heterogeneous connected systems. Proc 8th International Workshop on Dynamic Analysis (WODA2010). :–. Abstract

Dynamic, evolving systems pose new challenges from the point of view of Quality of Service (QoS) analysis, calling for techniques able to combine traditional offline methods with new ones applied at run-time. Tracking the evolution and updating the assessment consistently with such system evolution require not only advanced analysis methods, but also appropriate metrics well representative of QoS properties in the addressed context. The ongoing European project Connect addresses systems evolution, and aims at bridging technological gaps arising from heterogeneity of networked systems, by synthesising on-the-fly interoperability connectors. Moving from such ambitious goal, in this paper we present a metrics framework, whereby classical dependability/QoS metrics can be refined and combined to characterise Connect applications and to support their monitoring and analysis.

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.