Davide Ancona

Debora C. Engelmann, Angelo Ferrando, Alison R. Panisson et al.

This paper presents a Runtime Verification (RV) approach for Multi-Agent Systems (MAS) using the JaCaMo framework. Our objective is to bring a layer of security to the MAS. This layer is capable of controlling events during the execution of the system without needing a specific implementation in the behaviour of each agent to recognise the events. MAS have been used in the context of hybrid intelligence. This use requires communication between software agents and human beings. In some cases, communication takes place via natural language dialogues. However, this kind of communication brings us to a concern related to controlling the flow of dialogue so that agents can prevent any change in the topic of discussion that could impair their reasoning. We demonstrate the implementation of a monitor that aims to control this dialogue flow in a MAS that communicates with the user through natural language to aid decision-making in hospital bed allocation.

Davide Ancona, Chiara Bassano, Manuela Chessa et al.

Milgram's reality-virtuality continuum applies to interaction in the physical space dimension, going from real to virtual. However, interaction has a social dimension as well, that can go from real to artificial depending on the companion with whom the user interacts. In this paper we present our vision of the Reality-Artificiality bidimensional Continuum (RAC), we identify some challenges in its design and development and we discuss how reliable interactions might be supported inside RAC.

Davide Ancona, Gordon Pace

This volume contains the post-proceedings of the second Workshop on Verification of Objects at RunTime EXecution (VORTEX 2018) that was held in Amsterdam, co-located with the European Conference on Object-Oriented Programming (ECOOP 2018) and the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2018). Runtime verification is an approach to software verification which is concerned with monitoring and analysis of software and hardware system executions. Recently, it has gained more consensus as an effective and promising approach to ensure software reliability, bridging a gap between formal verification, and conventional testing; monitoring a system during runtime execution offers additional opportunities for addressing error recovery, self-adaptation, and other issues that go beyond software reliability. The goal of VORTEX is to bring together researchers working on runtime verification for topics covering either theoretical, or practical aspects, or, preferably, both, with emphasis on object-oriented languages, and systems.

Davide Ancona, Luca Franceschini, Giorgio Delzanno et al.

In the last years Node.js has emerged as a framework particularly suitable for implementing lightweight IoT applications, thanks to its underlying asynchronous event-driven, non blocking I/O model. However, verifying the correctness of programs with asynchronous nested callbacks is quite difficult, and, hence, runtime monitoring can be a valuable support to tackle such a complex task. Runtime monitoring is a useful software verification technique that complements static analysis and testing, but has not been yet fully explored in the context of Internet of Things (IoT) systems. Trace expressions have been successfully employed for runtime monitoring in widespread multiagent system platforms. Recently, their expressive power has been extended to allow parametric specifications on data that can be captured and monitored only at runtime. Furthermore, they can be language and system agnostic, through the notion of event domain and type. This paper investigates the use of parametric trace expressions as a first step towards runtime monitoring of programs developed in Node.js and Node-RED, a flow-based IoT programming tool built on top of Node.js. Runtime verification of such systems is a task that mostly seems to have been overlooked so far in the literature. A prototype implementing the proposed system for Node.js, in order to dynamically check with trace expressions the correct usage of API functions, is presented. The tool exploits the dynamic analysis framework Jalangi for monitoring Node.js programs and allows detection of errors that would be difficult to catch with other techniques. Furthermore, it offers a simple REST interface which can be exploited for runtime verification of Node-RED components, and, more generally, IoT devices.

Davide Ancona, Paola Giannini, Elena Zucca

We define an extension of the simply-typed lambda calculus where two different binding mechanisms, by position and by name, nicely coexist. In the former, as in standard lambda calculus, the matching between parameter and argument is done on a positional basis, hence alpha-equivalence holds, whereas in the latter it is done on a nominal basis. The two mechanisms also respectively correspond to static binding, where the existence and type compatibility of the argument are checked at compile-time, and dynamic binding, where they are checked at run-time.