 |
Angelo FERRANDO
Ricercatore t.d. art. 24 c. 3 lett. B
Dipartimento di Scienze Fisiche, Informatiche e Matematiche sede ex-Matematica
|
Home |
Didattica |
Pubblicazioni
2024
- Implementing Multiblock Techniques in a full-scale plant scenario: On-line Prediction of Quality Parameters in a Continuous Process for Different Acrylonitrile Butadiene Styrene (ABS) Products
[Articolo su rivista]
Tanzilli, Daniele; Strani, Lorenzo; Bonacini, Francesco; Ferrando, Angelo; Cocchi, Marina; Durante, Caterina
abstract
Background
The study explores the challenges of handling multiblock data of different natures (process and NIR sensors) for on-line quality prediction in a full-scale plant scenario, namely a plant operating in continuous on an industrial scale and producing different grade Acrylonitrile Butadiene Styrene (ABS) products. This environment is an ideal scenario to evaluate the use of multiblock data analysis methods, which can enhance data interpretation, visualization, and predictive performances. In particular, a novel multiblock extension of Locally Weighted PLS has been proposed by the authors, namely Locally Weighted Multiblock Partial Least Squares (LW-MB-PLS). Response-Oriented Sequential Alternation (ROSA) has also been employed to evaluate the diverse block relevance for the prediction of two quality parameters associated with the polymer. Data are split in blocks both according to sensor type and different plant sections, and different models have been built by incremental addition of data blocks to evaluate if early estimation of product quality is feasible.
Results
ROSA method showed promising predictive performance for both quality parameters, highlighting the most influential plant sections through the selection of data blocks. The results suggested that both early and late-stage sensors play crucial roles in predicting product quality. A reasonable estimation of quality parameters before production completion has been achieved. On the other hand, the proposed LW-MB-PLS, while comparable in predictive performances, allowed reducing systematic prediction errors for specific products.
Significance
This study contributes valuable insights for continuous production processes, aiding plant operators and paving the way for advancements in online quality prediction and control. Furthermore, it is implemented as a locally weighted extension of MB-PLS.
2023
- AGAMAS: A New Agent-Oriented Traffic Simulation Framework for SUMO
[Relazione in Atti di Convegno]
Sadeghi Garjan, Mahyar; Chaanine, Tommy; Pasquale, Cecilia; Paolo Pastore, Vito; Ferrando, Angelo
abstract
2023
- An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information
[Articolo su rivista]
Belardinelli, F.; Ferrando, A.; Malvone, V.
abstract
2023
- Exploiting Logic Programming for Runtime Verification: Current and Future Perspectives
[Capitolo/Saggio]
Ancona, D.; Ferrando, A.; Mascardi, V.
abstract
In this paper we discuss how Logic Programming can be exploited for Runtime Verification, an activity where a monitor is in charge for checking whether an observed event is allowed in the current state. If this is the case, the monitor moves to the successive state, observes another event, and so on, until either a violation is detected, or the stream of events ends. If the system emitting events is expected to run forever, so does the monitor. Being a semi-formal method, Runtime Verification must rely on a formal specification of the states of the observed system, and on a precise, formal description of the monitor’s behavior. These requirements, and the raising need to deal with partial observability of events, make the adoption of Logic Programming in the Runtime Verification domain extremely suitable, flexible and powerful.
2023
- Failure Handling in BDI Plans via Runtime Enforcement
[Relazione in Atti di Convegno]
Ferrando, Angelo; Cardoso, Rafael C.
abstract
2023
- How to Find Good Coalitions to Achieve Strategic Objectives
[Relazione in Atti di Convegno]
Ferrando, Angelo; Malvone, Vadim
abstract
2023
- HyperMonitor: {A} Python Prototype for Hyper Predictive Runtime Verification
[Relazione in Atti di Convegno]
Ferrando, Angelo; Delzanno, Giorgio
abstract
2023
- Incrementally predictive runtime verification
[Articolo su rivista]
Ferrando, Angelo; Delzanno, Giorgio
abstract
2023
- Integrating Ontologies and Cognitive Conversational Agents in On2Conv
[Relazione in Atti di Convegno]
Namakizadeh Esfahani, Zeinab; Cristina Engelmann, Débora; Ferrando, Angelo; Margarone, Massimiliano; Mascardi, Viviana
abstract
Multiagent systems have been successfully used in many domains. Being social, they are expected to communicate with human users in natural language. Nevertheless, the natural interaction between agents and humans is still challenging. Chatbot technologies are a key enabler to boost the communication between humans and software agents, but few technical solutions exist that make the agents’ reasoning capabilities easily accessible by a human user via a chatbot and, on the other hand, the chatbot’s answers more controllable and explainable. Dial4JaCa is one of such tools. It creates a bridge between Dialogflow and the JaCaMo cognitive-oriented and symbolic AI-based framework: the user’s interface is a Dialogflow chatbot allowing the user to interact in natural language, and the backend implementing the reasoning and performing required actions is a JaCaMo agent. However, in Dial4JaCa the consistency between data that feed the JaCaMo agent and those that feed the Dialogflow chatbot must be guaranteed by the developer via an error-prone and tedious manual process. By taking an ontology describing the domain of interest in input and generating both the skeleton for the JaCaMo agent’s behaviour and the intents for the Dialogflow chatbot, On2Conv improves Dial4JaCa robustness and reliability, and moves one step towards an explainable integration of agents and chatbots.
2023
- RV4JaCa—Towards Runtime Verification of Multi-Agent Systems and Robotic Applications
[Articolo su rivista]
Engelmann, D. C.; Ferrando, A.; Panisson, A. R.; Ancona, D.; Bordini, R. H.; Mascardi, V.
abstract
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 is achieved keeping in mind possible safety-critical uses of the MAS, such as robotic applications. 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. In this paper, we mainly focus on MAS when 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. The latter may be a problem and undermine the development of the software agents. In this paper, we tackle this problem by proposing and demonstrating the implementation of a framework that aims to control the dialogue flow in a MAS; especially when the MAS communicates with the user through natural language to aid decision-making in a hospital bed allocation scenario.
2023
- RV4Rasa: {A} Formalism-Agnostic Runtime Verification Framework for
Verifying ChatBots in Rasa
[Relazione in Atti di Convegno]
Ferrando, Angelo; Gatti, Andrea; Mascardi, Viviana
abstract
2023
- Runtime Verification of Hash Code in Mutable Classes
[Relazione in Atti di Convegno]
Ancona, D.; Ferrando, A.; Mascardi, V.
abstract
Most mainstream object-oriented languages provide a notion of equality between objects which can be customized to be weaker than reference equality, and which is coupled with the customizable notion of object hash code. This feature is so pervasive in object-oriented code that incorrect redefinition or use of equality and hash code may have a serious impact on software reliability and safety. Despite redefinition of equality and hash code in mutable classes is unsafe, many widely used API libraries do that in Java and other similar languages. When objects of such classes are used as keys in hash tables, programs may exhibit unexpected and unpredictable behavior. In this paper we propose a runtime verification solution to avoid or at least mitigate this issue. Our proposal uses RML, a rewriting-based domain specific language for runtime verification which is independent from code instrumentation and the programming language used to develop the software to be verified.
2023
- Scalable Verification of Strategy Logic through Three-Valued Abstraction
[Relazione in Atti di Convegno]
Belardinelli, Francesco; Ferrando, Angelo; Jamroga, Wojciech; Malvone, Vadim; Murano, Aniello
abstract
2023
- Special issue for the 23rd workshop "from objects to agents" (WOA 2022)
[Recensione in Rivista]
Ferrando, A.; Mascardi, V.
abstract
2023
- Towards the Verification of Strategic Properties in Multi-Agent Systems
with Imperfect Information
[Relazione in Atti di Convegno]
Ferrando, Angelo; Malvone, Vadim
abstract
2023
- Using a {BDI} Agent to Represent a Human on the Factory Floor of the
{ARIAC} 2023 Industrial Automation Competition
[Relazione in Atti di Convegno]
Buss Becker, Leandro; Downs, Anthony; Schlenoff, Craig; Albrecht, Justin; Kootbally, Zeid; Ferrando, Angelo; Cardoso, Rafael C.; Fisher, Michael
abstract
2022
- Coding Maps: A Planetary Journey into Computational Thinking and Digital Skills
[Abstract in Atti di Convegno]
Delzanno, Giorgio; Guerrini, Giovanna; Pusceddu, Matteo; Zanone, Giovanni; Ferrando, Angelo
abstract
2022
- Exploiting Probabilistic Trace Expressions for Decentralized Runtime Verification with Gaps
[Relazione in Atti di Convegno]
Ancona, D.; Ferrando, A.; Mascardi, V.
abstract
Multiagent Systems (MASs) are distributed systems composed by autonomous, reactive, proactive, heterogeneous communicating entities. In order to dynamically verify the behavior of such complex systems, a decentralized solution able to scale with the number of agents is necessary. When, for physical, infrastructural, or legal reasons, the monitor is not able to observe all the events emitted by the MAS, gaps are generated. In this paper we present a runtime verification decentralized approach to handle observation gaps in a MAS.
2022
- Formal Modelling and Runtime Verification of Autonomous Grasping for
Active Debris Removal
[Articolo su rivista]
Farrell, Marie; Mavrakis, Nikos; Ferrando, Angelo; Dixon, Clare; Gao, Yang
abstract
2022
- Implementing Ethical Governors in {BDI}
[Relazione in Atti di Convegno]
Cardoso, Rafael C.; Ferrando, Angelo; Dennis, Louise A.; Fisher, Michael
abstract
2022
- Journal-First: Formal Modelling and Runtime Verification of Autonomous Grasping for Active Debris Removal
[Relazione in Atti di Convegno]
Farrell, M.; Mavrakis, N.; Ferrando, A.; Dixon, C.; Gao, Y.
abstract
Verifying that autonomous space robotic software behaves correctly is crucial, particularly since such software is often mission-critical, that is, a software failure can lead to mission failure. In this paper, we describe the process that we used to verify the autonomous grasp generation and capturing operation of a spent rocket stage in space. This paper summarises a publication by the same authors in the journal Frontiers in Robotics and AI (2022) which harnesses multiple formal and non-formal methods to verify an autonomous grasping system.
2022
- RV4JaCa - Runtime Verification for Multi-Agent Systems
[Relazione in Atti di Convegno]
Engelmann, D. C.; Ferrando, A.; Panisson, A. R.; Ancona, D.; Bordini, R. H.; Mascardi, V.
abstract
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.
2022
- RVPLAN: Runtime Verification of Assumptions in Automated Planning
[Relazione in Atti di Convegno]
Ferrando, Angelo; Cardoso, Rafael C.
abstract
2022
- Runtime Verification with Imperfect Information Through Indistinguishability Relations
[Relazione in Atti di Convegno]
Ferrando, A.; Malvone, V.
abstract
Software systems are hard to trust, especially when autonomous. To overcome this, formal verification techniques can be deployed to verify such systems behave as expected. Runtime Verification is one of the most prominent and lightweight approaches to verify the system behaviour at execution time. However, standard Runtime Verification is built on the assumption of perfect information over the system, that is, the monitor checking the system can perceive everything. Unfortunately, this is not always the case, especially when the system under analysis contains rational/autonomous components and is deployed in real-world environments with possibly faulty sensors. In this work, we present an extension of the standard Runtime Verification of Linear Temporal Logic properties to consider scenarios with imperfect information. We present the engineering steps necessary to update the verification pipeline, and we report the corresponding implementation when applied to a case study involving robotic systems.
2022
- Safety Shields, an Automated Failure Handling Mechanism for {BDI}
Agents
[Abstract in Atti di Convegno]
Ferrando, Angelo; Cardoso, Rafael C.
abstract
2022
- Smart balancing of E-scooter sharing systems via deep reinforcement learning: a preliminary study
[Articolo su rivista]
Losapio, G.; Minutoli, F.; Mascardi, V.; Ferrando, A.
abstract
Nowadays, micro-mobility sharing systems have become extremely popular. Such systems consist in fleets of dockless electric vehicles which are deployed in cities, and used by citizens to move in a more ecological and flexible way. Unfortunately, one of the issues related to such technologies is its intrinsic load imbalance, since users can pick up and drop off the electric vehicles where they prefer. In this paper we present ESB-DQN, a multi-agent system for E-Scooter Balancing (ESB) based on Deep Reinforcement Learning where agents are implemented as Deep Q-Networks (DQN). ESB-DQN offers suggestions to pick or return e-scooters in order to make the fleet usage and sharing as balanced as possible, still ensuring that the original plans of the user undergo only minor changes. The main contributions of this paper include a careful analysis of the state of the art, an innovative customer-oriented rebalancing strategy, the integration of state-of-the-art libraries for deep Reinforcement Learning into the existing ODySSEUS simulator of mobility sharing systems, and preliminary but promising experiments that suggest that our approach is worth further exploration.
2022
- Smart rogaining for computer science orientation
[Articolo su rivista]
Chessa, M.; Delzanno, G.; Ferrando, A.; Gelati, L.; Guerrini, G.; Mascardi, V.; Noceti, N.; Odone, F.; Vitali, F.
abstract
In this paper, we address the problem of designing new formats of computer science orientation activities to be offered during high school students internships in Computer Science Bachelor degrees. In order to cover a wide range of computer science topics as well to deal with soft skills and gender gap issues, we propose a teamwork format, called smart rogaining, that offer engaging introductory activities to prospective students in a series of checkpoints dislocated along the different stages of a rogaine. The format is supported by a smart mobile and web application. Our proposal is aimed at stimulating the interest of participants in different areas of computer science and at improving digital and soft skills of participants and, as a side effect, of staff members (instructors and university students). In the paper, we introduce the proposed format and discuss our experience in the editions organized at the University of Genoa before the COVID-19 pandemic (2019 and 2020 waves).
2022
- StreamB: {A} Declarative Language for Automatically Processing Data
Streams in Abstract Environments for Agent Platforms
[Relazione in Atti di Convegno]
Ferrando, Angelo; Papacchini, Fabio
abstract
2022
- Towards the Combination of Model Checking and Runtime Verification on Multi-agent Systems
[Relazione in Atti di Convegno]
Ferrando, A.; Malvone, V.
abstract
2021
- Agents and robots for reliable engineered autonomy: A perspective from the organisers of area 2020
[Articolo su rivista]
Cardoso, R. C.; Ferrando, A.; Briola, D.; Menghi, C.; Ahlbrecht, T.
abstract
Multi-agent systems, robotics and software engineering are large and active research areas with many applications in academia and industry. The First Workshop on Agents and Robots for reliable Engineered Autonomy (AREA), organised the first time in 2020, aims at encouraging cross-disciplinary collaborations and exchange of ideas among researchers working in these research areas. This paper presents a perspective of the organisers that aims at highlighting the latest research trends, future directions, challenges, and open problems. It also includes feedback from the discussions held during the AREA workshop. The goal of this perspective is to provide a high-level view of current research trends for researchers that aim at working in the intersection of these research areas.
2021
- Agile Tasking of Robotic Systems with Explicit Autonomy
[Relazione in Atti di Convegno]
Cardoso, Rafael C.; Michaloski, John L.; Schlenoff, Craig; Ferrando, Angelo; Dennis, Louise A.; Fisher, Michael
abstract
Task agility is an increasingly desirable feature for
robots in application domains such as manufacturing.
The Canonical Robot Command Language (CRCL) is
a lightweight information model built for agile tasking
of robotic systems. CRCL replaces the underlying complex proprietary robot programming interface with a
standard interface. In this paper, we exchange the automated planning component that CRCL used in the past
for a rational agent in the GWENDOLEN agent programming language, thus providing greater possibilities for
formal verification and explicit autonomy. We evaluate
our approach by performing agile tasking in a kitting
case study
2021
- An overview of verification and validation challenges for inspection
[Articolo su rivista]
Fisher, R. M.; Cardoso, R. C.; Collins, E. C.; Dadswell, C.; Dennis, L. A.; Dixon, C.; Farrell, M.; Ferrando, A.; Huang, X.; Jump, M.; Kourtis, G.; Lisitsa, A.; Luckcuck, M.; Luo, S.; Page, V.; Papacchini, F.; Webster, M.
abstract
The advent of sophisticated robotics and AI technology makes sending humans into hazardous and distant environments to carry out inspections increasingly avoidable. Being able to send a robot, rather than a human, into a nuclear facility or deep space is very appealing. However, building these robotic systems is just the start and we still need to carry out a range of verification and validation tasks to ensure that the systems to be deployed are as safe and reliable as possible. Based on our experience across three research and innovation hubs within the UK’s “Robots for a Safer World” programme, we present an overview of the relevant techniques and challenges in this area. As the hubs are active across nuclear, offshore, and space environments, this gives a breadth of issues common to many inspection robots.
2021
- Automated Planning and {BDI} Agents: {A} Case Study
[Relazione in Atti di Convegno]
Cardoso, Rafael C.; Ferrando, Angelo; Papacchini, Fabio
abstract
2021
- Bridging the gap between single- and multi-model predictive runtime verification
[Articolo su rivista]
Ferrando, Angelo; Cardoso, Rafael C.; Farrell, Marie; Luckcuck, Matt; Papacchini, Fabio; Fisher, Michael; Mascardi, Viviana
abstract
This paper presents an extension of the Predictive Runtime Verification (PRV) paradigm to consider multiple models of the System Under Analysis (SUA). We call this extension Multi-Model PRV. Typically, PRV attempts to predict the satisfaction or violation of a property based on a trace and a (single) formal model of the SUA. However, contemporary node- or component-based systems (e.g. robotic systems) may benefit from monitoring based on a model of each component. We show how a Multi-Model PRV approach can be applied in either a centralised or a compositional way (where the property is compositional), as best suits the SUA. Crucially, our approach is formalism-agnostic. We demonstrate our approach using an illustrative example of a Mars Curiosity rover simulation and evaluate our contribution via a prototype implementation.
2021
- Combine Model Checking and Runtime Verification in Multi-Agent Systems
[Relazione in Atti di Convegno]
Ferrando, Angelo; Malvone, Vadim
abstract
2021
- Declarative Parameterized Verification of Distributed Protocols via
the Cubicle Model Checker
[Articolo su rivista]
Conchon, Sylvain; Delzanno, Giorgio; Ferrando, Angelo
abstract
2021
- Increasing confidence in autonomous systems
[Relazione in Atti di Convegno]
Fisher, Michael; Ferrando, Angelo; Cardoso, Rafael C.
abstract
2021
- Incrementally Predictive Runtime Verification
[Relazione in Atti di Convegno]
Ferrando, Angelo; Delzanno, Giorgio
abstract
2021
- MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest
[Relazione in Atti di Convegno]
Cardoso, R. C.; Ferrando, A.; Papacchini, F.; Luckcuck, M.; Linker, S.; Payne, T. R.
abstract
In this paper, we describe the strategies used by our team, MLFC, that led us to achieve the 2nd place in the 15th edition of the Multi-Agent Programming Contest. The scenario used in the contest is an extension of the previous edition (14th ) “Agents Assemble” wherein two teams of agents move around a 2D grid and compete to assemble complex block structures. We discuss the languages and tools used during the development of our team. Then, we summarise the main strategies that were carried over from our previous participation in the 14th edition and list the limitations (if any) of using these strategies in the latest contest edition. We also developed new strategies that were made specifically for the extended scenario: cartography (determining the size of the map); formal verification of the map merging protocol (to provide assurances that it works when increasing the number of agents); plan cache (efficiently scaling the number of planners); task achievement (forming groups of agents to achieve tasks); and bullies (agents that focus on stopping agents from the opposing team). Finally, we give a brief overview of our performance in the contest and discuss what we believe were our shortcomings.
2021
- RML: Theory and practice of a domain specific language for runtime verification
[Articolo su rivista]
Ancona, Davide; Franceschini, Luca; Ferrando, Angelo; Mascardi, Viviana
abstract
Runtime verification (RV) is an approach to verification consisting in dynamically checking that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specification of its expected correct behavior. RML (Runtime Monitoring Language) is a simple but powerful Domain Specific Language (DSL) for RV which is able to express non context-free properties. When designing RML, particular care has been taken to favor abstraction and simplicity, to better support reusability and portability of specifications and interoperability of the monitors generated from them; this is mainly achieved by decoupling the two problems of property specification and event generation, and by minimizing the available primitive constructs. The formalization and implementation of RML is based on a trace calculus with a fully deterministic rewriting semantics. The semantics of RML is defined by translation into such a calculus, which, in fact, is used as intermediate representation (IR) by the RML compiler. The effectiveness of RML and its methodological impact on RV are presented through interesting patterns that can be adapted to different contexts requiring verification of standard properties. A collection of tested examples is provided, together with benchmarks showing that the deterministic semantics and the performed dynamic optimizations based on the laws of the trace calculus significantly improve the performances of the generated monitors.
2021
- Smart Balancing of E-scooter Sharing Systems via Deep Reinforcement
Learning
[Relazione in Atti di Convegno]
Losapio, Gianvito; Minutoli, Federico; Mascardi, Viviana; Ferrando, Angelo
abstract
2021
- Special issue: Agents and robots for reliable engineered autonomy
[Articolo su rivista]
Cardoso, R. C.; Ferrando, A.; Briola, D.; Menghi, C.; Ahlbrecht, T.
abstract
2021
- Strategy {RV:} {A} Tool to Approximate {ATL} Model Checking under
Imperfect Information and Perfect Recall
[Relazione in Atti di Convegno]
Ferrando, Angelo; Malvone, Vadim
abstract
2021
- Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems
[Articolo su rivista]
Ferrando, Angelo; Dennis, Louise A.; Cardoso, Rafael C.; Fisher, Michael; Ancona, Davide; Mascardi, Viviana
abstract
When applying formal verification to a system that interacts with the real world we must use a model of the environment. This model
represents an abstraction of the actual environment, so it is necessarily incomplete and hence presents an issue for system verification.
If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction
captured by the model, then we cannot guarantee that the system is well-behaved. A solution to this problem consists in exploiting
the model of the environment used for statically verifying the system’s behaviour and, if the verification succeeds, using it also for
validating the model against the real environment via runtime verification. The paper discusses this approach and demonstrates its
feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. A high-level
Domain Specific Language is used to model the environment in a user-friendly way; the latter is then compiled to trace expressions
for both static formal verification and runtime verification. To evaluate our approach, we apply it to two different case studies, an
autonomous cruise control system, and a simulation of the Mars Curiosity rover.
2021
- Towards Partial Monitoring: It is Always too Soon to Give Up
[Relazione in Atti di Convegno]
Ferrando, Angelo; Cardoso, Rafael C.
abstract
2021
- Towards a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems
[Articolo su rivista]
Ferrando, Angelo; Dennis, Louise; Cardoso, Rafael; Fisher, Michael; Ancona, Davide; Mascardi, Viviana
abstract
When applying formal verification to a system that interacts with the
real world we must use a model of the environment. This model represents an abstraction of the actual environment, so it is necessarily incomplete and hence presents an issue for
system verification. If the actual environment matches the model, then
the verification is correct; however, if the environment falls outside
the abstraction captured by the model, then we cannot guarantee that the
system is well-behaved.
A solution to this problem consists in exploiting the model of the environment used for statically verifying the system's behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification.
The paper discusses this approach and demonstrates its feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. A high-level Domain Specific Language is used to model the environment in a user-friendly way; the latter is then compiled to trace expressions for both static formal verification and runtime verification.
To evaluate our approach, we apply it to two different case studies, an autonomous cruise control system, and a simulation of the Mars Curiosity rover.
2021
- {RVPLAN:} a general purpose framework for replanning using runtime
verification
[Relazione in Atti di Convegno]
Ferrando, Angelo; Cardoso, Rafael C.
abstract
2020
- An Interface for Programming Verifiable Autonomous Agents in {ROS}
[Relazione in Atti di Convegno]
Cardoso, Rafael C.; Ferrando, Angelo; Dennis, Louise A.; Fisher, Michael
abstract
2020
- Can determinism and compositionality coexist in RML?
[Relazione in Atti di Convegno]
Ancona, Davide; Ferrando, Angelo; Mascardi, Viviana
abstract
Runtime verification (RV) consists in dynamically verifying that the event traces generated by single runs of a system under scrutiny (SUS) are compliant with the formal specification of its expected properties. RML (Runtime Monitoring Language) is a simple but expressive Domain Specific Language for RV; its semantics is based on a trace calculus formalized by a deterministic rewriting system which drives the implementation of the interpreter of the monitors generated by the RML compiler from the specifications. While determinism of the trace calculus ensures better performances of the generated monitors, it makes the semantics of its operators less intuitive. In this paper we move a first step towards a compositional semantics of the RML trace calculus, by interpreting its basic operators as operations on sets of instantiated event traces and by proving that such an interpretation is equivalent to the operational semantics of the calculus.
2020
- Heterogeneous Verification of an Autonomous Curiosity Rover
[Relazione in Atti di Convegno]
Cardoso, Rafael C.; Farrell, Marie; Luckcuck, Matt; Ferrando, Angelo; Fisher, Michael
abstract
The Curiosity rover is one of the most complex systems successfully deployed in a planetary exploration mission to date. It was sent by NASA to explore the surface of Mars and to identify potential signs of life. Even though it has limited autonomy on-board, most of its decisions are made by the ground control team. This hinders the speed at which the Curiosity reacts to its environment, due to the communication delays between Earth and Mars. Depending on the orbital position of both planets, it can take 4–24 min for a message to be transmitted between Earth and Mars. If the Curiosity were controlled autonomously, it would be able to perform its activities much faster and more flexibly. However, one of the major barriers to increased use of autonomy in such scenarios is the lack of assurances that the autonomous behaviour will work as expected. In this paper, we use a Robot Operating System (ROS) model of the Curiosity that is simulated in Gazebo and add an autonomous agent that is responsible for high-level decision-making. Then, we use a mixture of formal and non-formal techniques to verify the distinct system components (ROS nodes). This use of heterogeneous verification techniques is essential to provide guarantees about the nodes at different abstraction levels, and allows us to bring together relevant verification evidence to provide overall assurance.
2020
- Lfc: Combining autonomous agents and automated planning in the multi-agent programming contest
[Relazione in Atti di Convegno]
Cardoso, R C; Ferrando, A; Papacchini, F
abstract
The 2019 Multi-Agent Programming Contest introduced a new scenario, Agents Assemble, where two teams of agents move around a 2D grid and compete to assemble complex block structures. In this paper, we describe the strategies used by our team that led us to achieve first place in the contest. Our strategies tackle some of the major challenges in the 2019 contest: how to explore and build a map when agents only have access to local vision and no global coordinates; how to move around the map efficiently even though there are dynamic events that can change the cells in the grid; and how to assemble and submit complex block structures given that the opposing team may try to sabotage us. To implement our strategies, we use the multi-agent systems development platform JaCaMo to program our agents and the Fast Downward planner to plan the movement of the agent in the grid. We also provide a brief discussion of our matches in the contest and give our analysis of how our team performed in each match.
2020
- On enactability of agent interaction protocols: Towards a unified approach
[Relazione in Atti di Convegno]
Ferrando, A.; Winikoff, M.; Cranefield, S.; Dignum, F.; Mascardi, V.
abstract
Interactions between agents are usually designed from a global viewpoint. However, the implementation of a multi-agent interaction is distributed. It is well known that this difference between the specification and the implementation levels can introduce problems, allowing designers to specify protocols from a global viewpoint that cannot be implemented as a collection of individual agents. This leads naturally to the question of whether a given (global) protocol is enactable, namely, whether it can be implemented in a distributed way. We consider this question in the powerful setting of trace expressions, considering a range of message ordering interpretations (specifying what it means to say that an interaction step occurs before another), and a range of possible constraints on the semantics of message delivery, corresponding to different properties of the underlying communication middleware. We provide a definition of enactability, along with an implementation of the definition that is applied to a number of example protocols.
2020
- ROSMonitoring: A Runtime Verification Framework for ROS
[Relazione in Atti di Convegno]
Ferrando, A.; Cardoso, R. C.; Fisher, M.; Ancona, D.; Franceschini, L.; Mascardi, V.
abstract
Recently, robotic applications have been seeing widespread use across industry, often tackling safety-critical scenarios where software reliability is paramount. These scenarios often have unpredictable environments and, therefore, it is crucial to be able to provide assurances about the system at runtime. In this paper, we introduce ROSMonitoring, a framework to support Runtime Verification (RV) of robotic applications developed using the Robot Operating System (ROS). The main advantages of ROSMonitoring compared to the state of the art are its portability across multiple ROS distributions and its agnosticism w.r.t. the specification formalism. We describe the architecture behind ROSMonitoring and show how it can be used in a traditional ROS example. To better evaluate our approach, we apply it to a practical example using a simulation of the Mars curiosity rover. Finally, we report the results of some experiments to check how well our framework scales.
2020
- Runtime Verification of the {ARIAC} Competition: Can a Robot be Agile
and Safe at the same time?
[Relazione in Atti di Convegno]
Ferrando, Angelo; Kootbally, Zeid; Piliptchak, Pavel; Cardoso, Rafael C.; Schlenoff, Craig; Fisher, Michael
abstract
2020
- Slow Rogaining: An Innovative Teamwork Model for Computer Science Education
[Relazione in Atti di Convegno]
Delzanno, G; Guerrini, G; Mascardi, V; Gelati, L; Petito, V; Vitali, F; Ferrando, A; Ancona, D; Chessa, M; Noceti, N; Odone, F
abstract
We present a novel teamwork model based on rogaining that since 2018 we have successfully applied in several events of our University. Our model, named Slow Rogaining, exploits gamification principles in order to engage participants, divided in teams, in a rogaine built on top of compelling activities related to computer science. The term slow (inspired by the slow food philosophy) is used to emphasize the difference with standard outdoor rogaines. Indeed, Slow Rogaining is mainly designed as an indoor navigational activity with a limited time duration (3-4 hours). In the paper, we provide a multi-layer analysis of our model in terms of soft skill development for participants and mentors, orienteering goals, computer science disciplinary teaching goals. We will also discuss the benefits of introducing a technology support activities developed according to this model both in practice (on the field) and in theory (in the design phase).
2020
- The DigForSim Agent Based Simulator of People Movements in Crime Scenes
[Relazione in Atti di Convegno]
Biagetti, A; Ferrando, A; Mascardi, V
abstract
Evidence analysis is one of the Digital Forensics tasks and involves examining fragmented incomplete knowledge and reasoning on it, in order to reconstruct plausible crime scenarios. After more than one year of activity within the DigForASP COST Action, the lack of real data about movements of people in crime scenes emerged as a major limitation to the need of testing the DigForASP prototypes that exploit Artificial Intelligence and Automated Reasoning for evidence analysis.
In this paper we present DigForSim, an Agent Based Modeling and Simulation tool aimed at producing synthetic, controllable data on the movements of agents in the crime scene, in form of files logging the agents’ position at given time points. These log files serve as benchmarks for the DigForASP reasoning prototypes.
2019
- A deterministic event calculus for effective runtime verification
[Relazione in Atti di Convegno]
Ancona, D.; Franceschini, L.; Ferrando, A.; Mascardi, V.
abstract
Runtime verification (RV) is an effective technique for dynamically monitoring, even after deployment, properties that could be hardly verified statically. To this aim, specification formalims for RV have to reconcile expressive power and monitoring efficiency. We present an event calculus which provides a basis for the semantics and the implementation of RML, a domain specific language (DSL) for RV. The semantics of the calculus is based on a deterministic reduction strategy which allows concise specifications of non context-free properties, and their efficient verification at runtime.
2019
- Declarative parameterized verification of topology-sensitive distributed protocols
[Relazione in Atti di Convegno]
Conchon, Sylvain; Delzanno, Giorgio; Ferrando, Angelo
abstract
We show that Cubicle [9], an SMT-based infinite-state model checker, can be applied as a verification engine for GLog, a logic-based specification language for topology-sensitive distributed protocols with asynchronous communication. Existential coverability queries in GLog can be translated into verification judgements in Cubicle by encoding relational updates rules as unbounded array transitions. We apply the resulting framework to automatically verify a distributed version of the Dining Philosopher mutual exclusion protocol formulated for an arbitrary number of nodes and communication buffers.
2019
- Engineering Multi-Agent Systems: State of Affairs and the Road Ahead
[Articolo su rivista]
Mascardi, Viviana; Weyns, Danny; Ricci, Alessandro; Benac Earle, Clara; Casals, Arthur; Challenger, Moharram; Chopra, Amit; Ciortea, Andrei; Dennis, Louise; Díaz, Álvaro Fernández; El Fallah-Seghrouchni, Amal; Ferrando, Angelo; Fredlund, Lars-Åke; Giunchiglia, Eleonora; Guessoum, Zahia; Günay, Akın; Hindriks, Koen V; Iglesias, Carlos Ángel; Logan, Brian; Kampik, Timotheus; Kardas, Geylani; Koeman, Vincent J; Larsen, John Bruntse; Mayer, Simon; Méndez, Tasio; Nieves, Juan Carlos; Seidita, Valeria; Teze, Baris Tekin; Varga, László Zsolt; Winikoff, Michael
abstract
The continuous integration of software-intensive systems together with the ever-increasing computing power offer a breeding ground for intelligent agents and multi-agent systems (MAS) more than ever before. Over the past two decades, a wide variety of languages, models, techniques and methodologies have been proposed to engineer agents and MAS. Despite this substantial body of knowledge and expertise, the systematic engineering of large-scale and open MAS still poses many challenges. Researchers and engineers still face fundamental questions regarding theories, architectures, languages, processes, and platforms for designing, implementing, running, maintaining, and evolving MAS. This paper reports on the results of the 6th International Workshop on Engineering Multi-Agent Systems (EMAS 2018, 14th-15th of July, 2018, Stockholm, Sweden), where participants discussed the issues above focusing on the state of affairs and the road ahead for researchers and engineers in this area.
2019
- On Enactability of Agent Interaction Protocols: Towards a Unified
Approach
[Relazione in Atti di Convegno]
Ferrando, Angelo; Winikoff, Michael; Cranefield, Stephen; Dignum, Frank; Mascardi, Viviana
abstract
Interactions between agents are usually designed from a global viewpoint. However, the implementation of a multi-agent interaction is distributed. This difference can introduce problems. For instance, it is possible to specify protocols from a global viewpoint that cannot be implemented as a collection of individual agents. This leads naturally to the question of whether a given (global) protocol is enactable. We consider this question in a powerful setting (trace expressions), considering a range of message ordering interpretations (specifying what it means to say that an interaction step occurs before another), and a range of possible constraints on the semantics of message delivery, corresponding to different properties of the underlying communication middleware.
2019
- Smart RogAgent: Where Agents and Humans Team Up
[Capitolo/Saggio]
Capone, C.; Bordini, R. H.; Mascardi, V.; Delzanno, G.; Ferrando, A.; Gelati, L.; Guerrini, G.
abstract
The increasing diffusion of team building as a means to enhance social relations and define roles within teams, and the cost of setting up a real team building event, raises the pressing need of simulating team building activities in order to assess the effectiveness of different formats, run in different contexts and under different conditions, before one is selected for a particular scenario. The selection of a software platform employing software abstractions which are close to the real entities involved in a team building event, including human beings and their roles, goals, and organisations, paves the way to substituting some simulated entity with its real counterpart, moving from simulation to a hybrid application where real entities and their software “alter egos” can co-exist. We present the design of Smart RogAgent, a JaCaMo multi-agent system aimed at simulating rogaining, a special kind of team building activity. Once fully developed, Smart RogAgent will have the potential to allow artificial intelligent agents to enter human teams, and vice versa, providing the technological support for the creation of hybrid human-agent teams in a principled way.
2019
- The early bird catches the worm: First verify, then monitor!
[Articolo su rivista]
Ferrando, Angelo
abstract
Trace expressions are a compact and expressive formalism, initially devised for runtime verification of agent interactions in multiagent systems, which has been successfully employed to model real-world protocols, and to generate monitors for mainstream multiagent system platforms, and generalized to support runtime verification of different kinds of properties and systems. In this paper, we propose an algorithm to check Linear Temporal Logic (LTL) properties satisfiability on trace expressions. To do this, we show how to translate a trace expression into a Büchi Automaton in order to realize an Automata-Based Model Checking. We show that this translation generates an over-approximation of our trace expression leading us to obtain a sound procedure to verify LTL properties. Once we have statically checked a set of LTL properties, we can conclude that: (1) our trace expression is formally correct (2) since we use this trace expression to generate monitors checking the runtime behavior of the system, the LTL properties verified by this trace expression are also verified by the monitored system.
2019
- Timed trace expressions
[Relazione in Atti di Convegno]
Ciccone, L.; Ferrando, A.; Ancona, D.; Mascardi, V.
abstract
Trace expressions are a compact and expressive formalism initially devised for runtime verication of multiagent systems, and then adopted for runtime verication of object oriented systems and of Internet of Things applications.
In this paper we survey different logics to cope with time intervals, and we exploit the ideas underlying these logics to extend the trace expressions formalism with the explicit management of time
2019
- Towards Integrating Formal Verification of Autonomous Robots with
Battery Prognostics and Health Management
[Relazione in Atti di Convegno]
Zhao, Xingyu; Osborne, Matt; Lantair, Jenny; Robu, Valentin; Flynn, David; Huang, Xiaowei; Fisher, Michael; Papacchini, Fabio; Ferrando, Angelo
abstract
2019
- Verifying and validating autonomous systems: Towards an integrated approach
[Relazione in Atti di Convegno]
Ferrando, A.; Dennis, L. A.; Ancona, D.; Fisher, M.; Mascardi, V.
abstract
When applying formal verification to a system that interacts with the real world we must use a model of the environment. This model represents an abstraction of the actual environment, but is necessarily incomplete and hence presents an issue for system verification. If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction captured by the model, then we cannot guarantee that the system is well-behaved. A solution to this problem consists in exploiting the model of the environment for statically verifying the system’s behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification. The paper discusses this approach and demonstrates its feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. Trace expressions are used to model the environment for both static formal verification and runtime verification.
2018
- Agents interoperability via conformance modulo mapping
[Relazione in Atti di Convegno]
Ancona, Davide; Ferrando, Angelo; Mascardi, Viviana
abstract
We present an algorithm for establishing a flexible conformance relation between two local agent interaction protocols (LAIPs) based on mappings involving agents and messages, respectively. Conformance is in fact computed "modulo mapping": two LAIPs τ and τ may involve different agents and use different syntax for messages, but may still be found to be conformant provided that a given map from entities appearing in τ to corresponding entities in τ is applied. LAIPs are modelled as trace expressions whose high expressive power allows for the design of protocols that could not be specified using finite state automata or equivalent formalisms. This expressive power makes the problem of stating if τ conforms to τ undecidable. We cope with this problem by over-approximating trace expressions that may lead to infinite computations, obtaining a sound but not complete implementation of the proposed conformance check.
2018
- Coping with bad agent interaction protocols when monitoring partially observable multiagent systems
[Relazione in Atti di Convegno]
Ancona, Davide; Ferrando, Angelo; Franceschini, Luca; Mascardi, Viviana
abstract
Interaction Protocols are fundamental elements to provide the entities in a system, be them actors, agents, services, or other communicating pieces of software, a means to agree on a global interaction pattern and to be sure that all the other entities in the system adhere to it as well. These “global interaction patterns” may serve different purposes: if the system does not yet exist, they may specify the allowed interactions in order to drive the system’s implementation and execution. If the system exists before and independently from the protocol, the protocol may still specify the allowed interactions, but it cannot be used to implement them. Its purpose in this case is to monitor that the actual system does respect the rules (runtime verification). Tagging some protocols as good ones and others as bad is common to all the research communities where interaction is crucial, and it is not surprising that some protocol features are recognized as bad ones everywhere. In this paper we analyze the notion of good, bad and ugly protocols in the MAS community and outside, and we discuss the role that bad protocols, despite being bad, may play in a runtime verification scenario where not all the events and interaction channels can be observed.
2018
- Improving flexibility and dependability of remote patient monitoring with agent-oriented approaches
[Articolo su rivista]
Ancona, Davide; Ferrando, Angelo; Mascardi, Viviana
abstract
Context: Remote Patient Monitoring (RPM) enables physicians to perform diagnosis and/or treatment remotely through sensors connected via a
communication network. Dependability and flexibility are recognized as two key technological requirements for RPM take off. Research question: We address the questions of how RPM systems designed and implemented as multiagent systems (MASs) can ensure flexibility and dependability, and which agent-oriented approach – if any – is more suitable to achieve this goal. Method: We analyzed five state-of-the-art agent-oriented approaches suitable to
engineer dependable and/or flexible systems. We planned to adopt the “winner” approach to realize a working prototype able to show the potential of an agent-oriented approach to RPM.
Results: No approach among the five dominates the others w.r.t. all the ten features that drove our analysis. In absence of a winner, we selected the approach we are more familiar with, namely parametric trace expressions. We used them to verify properties modeling existing medical guidelines and to developed a prototype where newborns suffering from hypoglycemia must be continuously monitored at home.
Conclusions: Parametric trace expressions proved to be suitable for engineering flexible and dependable RPM systems. This finding can be generalized: agent-oriented approaches showing features similar to those of parametric trace expressions can serve to achieve the same goal.
2018
- Managing bad AIPs with RIVERtools
[Relazione in Atti di Convegno]
Ancona, Davide; Ferrando, Angelo; Franceschini, Luca; Mascardi, Viviana
abstract
We present the RIVERtools integrated development environment for specifying Agent Interaction Protocols (AIPs) modelled as trace expressions, and for statically verifying some of their properties. In particular, this demonstration paper aims at showing why a “good” AIP can become a “bad” one because of unreliability of some communication channels, and how RIVERtools can cope with such bad AIPs, suggesting to the developer possible ways to dynamically verify them in a partially decentralized way.
2018
- RIVERtools: An IDE for RuntIme VERification of MASs, and beyond
[Relazione in Atti di Convegno]
Ferrando, A.
abstract
This work introduces RIVERtools, an IDE supporting the use of the "trace expressions" formalism by users that want to perform runtime verification of their own system.
2018
- Recognising assumption violations in autonomous systems verification
[Relazione in Atti di Convegno]
Ferrando, A.; Dennis, L. A.; Ancona, D.; Fisher, M.; Mascardi, V.
abstract
When applying formal verification to a system that interacts with the real world we must use a model of the environment. This model represents an abstraction of the actual environment, but is necessarily incomplete and hence presents an issue for system verification. If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction captured by the model, then we cannot guarantee that the system is well-behaved. A solution to this problem consists in exploiting the model of the environment for statically verifying the system's behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification. The paper reports on a demonstration of the feasibility of this approach using the Agent Java Pathfinder model checker. Trace expressions are used to model the environment for both static formal verification and runtime verification.
2017
- Decentralizing MAS Monitoring with DecAMon
[Relazione in Atti di Convegno]
Ferrando, Angelo; Ancona, Davide; Mascardi, Viviana
abstract
We describe DecAMon, an algorithm for decentralizing the monitoring of the MAS communicative behavior described via an Agent Interaction Protocol (AIP). If some agents in the MAS are grouped together and monitored by the same monitor, instead of individually, a partial decentralization of the monitoring activity can still be obtained even if the "unique point of choice" (a.k.a. local choice) and "connectedness for sequence" (a.k.a. causality) coherence conditions are not satisfied by the protocol.
Given an AIP specification, DecAMon outputs a set of "Monitoring Safe Partitions" of the agents, namely partitions P which ensure that having one monitor in charge for each group of agents in P allows detection of all and only the protocol violations that a fully centralized monitor would detect.
In order to specify AIPs we use "trace expressions": this formalism can express event traces that are not context-free and can model both synchronous and asynchronous communication just by changing the underlying notion of event.
2017
- Hackmytown: An educational experience on smart cities
[Articolo su rivista]
Del Fatto, Vincenzo; Dodero, Gabriella; Bernhard, Armin; Ferrando, Angelo; Ancona, Davide; Mascardi, Viviana; Laurini, Robert; Roccasalva, Giuseppe
abstract
This paper describes the preparation and the execution of an educational experience consisting of a challenge, called Hackmytown, among five different teams composed by university students, aimed at experiencing challenges in the definition of "smart" services for a city. Glurns/Glorenza, the smallest city of South Tirol (Italy), was chosen as the ideal location to verify the application of the concept of Smart City in a small community by adopting a bottom-up approach involving local stakeholders and Municipality.
2017
- Parametric Runtime Verification of Multiagent Systems
[Relazione in Atti di Convegno]
Ancona, Davide; Ferrando, Angelo; Mascardi, Viviana
abstract
2017
- Parametric trace expressions for runtime verification of Java-like programs
[Relazione in Atti di Convegno]
Ancona, Davide; Ferrando, Angelo; Franceschini, Luca; Mascardi, Viviana
abstract
Parametric trace expressions are a formalism expressly designed for parametric runtime verification (RV) which has been introduced and successfully employed in the context of runtime monitoring of multiagent systems. Trace expressions are built on the general notion of event type, which allows them to be adopted in different contexts. In this paper we show how trace expressions can be used for conveniently specifying the expected behavior of a Java-like program to be monitored at runtime. Furthermore, we investigate the basic properties of the primitive operators on which trace expressions are coinductively defined in terms of a labeled transition system; this provides a basis for formal reasoning about equivalence of trace expressions and for adopting useful optimization techniques to speed up runtime verification.
2016
- Automatic Partitions Extraction to Distribute the Runtime Verification
of a Global Specification
[Relazione in Atti di Convegno]
Ferrando, Angelo
abstract
2016
- Comparing trace expressions and linear temporal logic for runtime verification
[Capitolo/Saggio]
Ancona, Davide; Ferrando, Angelo; Mascardi, Viviana
abstract
Trace expressions are a compact and expressive formalism, initially devised for runtime verification of agent interactions in multiagent systems, which has been successfully employed to model real protocols, and to generate monitors for mainstream multiagent system platforms, and generalized to support runtime verification of different kinds of properties and systems. In this paper we formally compare the expressive power of trace expressions with the Linear Temporal Logic (LTL), a formalism widely adopted in runtime verification. We show that any LTL formula can be translated into a trace expression which is equivalent from the point of view of runtime verification. Since trace expressions are able to express and verify sets of traces that are not context-free, we can derive that in the context of runtime verification trace expressions are more expressive than LTL.
2016
- FRIENDLY & KIND with your health: Human-friendly knowledge-INtensive dynamic systems for the e-health domain
[Relazione in Atti di Convegno]
Aielli, Federica; Ancona, Davide; Caianiello, Pasquale; Costantini, Stefania; De Gasperis, Giovanni; Di Marco, Antinisca; Ferrando, Angelo; Mascardi, Viviana
abstract
This paper presents our approach for addressing “Human-friendly Knowledge-INtensive Dynamic Systems” (FRIENDLY & KIND systems) from a methodological point of view, also providing tools and languages for their design, implementation and testing. FRIENDLY & KIND systems are an evolution of multiagent systems and represent a good option for engineering complex and dynamic applications like those in the e-Health domain. We will demonstrate the suitability of our approach by designing and implementing a Remote Monitoring System for oncological patients.
2016
- Identification of disease symptoms in multilingual sentences: An ontology-driven approach
[Relazione in Atti di Convegno]
Ferrando, Angelo; Beux, Silvio; Mascardi, Viviana; Rosso, Paolo
abstract
In this paper we present a Multilingual Ontology-Driven framework for Text Classification (MOoD-TC). This framework is highly modular and can be customized to create applications based on Multilingual Natural Language Processing for classifying domain-dependent contents. In order to show the potential of MOoD-TC, we present a case study in the e-Health domain.
2016
- MAS-DRiVe: A practical approach to decentralized runtime verification of agent interaction protocols
[Relazione in Atti di Convegno]
Ancona, Davide; Briola, Daniela; Ferrando, Angelo; Mascardi, Viviana
abstract
We address the problem of decentralized runtime verification of interaction protocols in multiagent systems by means of MAS-DRiVe, an algorithm for partitioning a multiagent system (MAS) into sub-MASs which can be monitored independently. Given a global interaction protocol named AIP (for "Agent Interaction Protocol") describing all the interactions which can take place in the MAS, the MAS-DRiVe algorithm extracts the interaction graph from AIP, identifies the clusters of agents which cannot be split during the decentralized monitoring as the interactions they are involved in are not independent, collapses each of those clusters into a single node in the interaction graph, and finally partitions the collapsed graph obtained so far. Although the "unsplittable agents identification" stage is still in its early design and prototyping phases and requires a better formalization and a deeper analysis, the MAS-DRiVe algorithm pipeline has been fully implemented and demonstrated on two simple MASs. Once the independently monitorable sub-MASs have been identified by MAS-DRiVe, the global interaction protocol AIP can be projected onto the subsets of agents belonging to each graph partition, thus obtaining local versions of AIP which can be monitored in a decentralized way.
2016
- Monitoring patients with hypoglycemia using self-adaptive protocol-driven agents: A case study
[Relazione in Atti di Convegno]
Ferrando, Angelo; Ancona, Davide; Mascardi, Viviana
abstract
Trace expressions are a compact and expressive formalism for specifying complex patterns of actions. In this paper they have been used to model medical protocols and to generate agents able to execute them, also adapting to the context dynamics. To this aim, we extended our previous work on “self-adaptive agents driven by interaction protocols” by allowing agents to be guided by trace expressions instead of the less concise and less powerful “constrained global types”. This extension required a limited effort, which is an advantage of the previous work as it is relatively straightforward to adapt it to accommodate new requirements arising in sophisticated domains.
2016
- Simulation of autonomous systems in the extended marine domain
[Articolo su rivista]
Tremori, Alberto; Agresta, Matteo; Ferrando, Angelo
abstract
This paper is focused on characteristics and goals of an integrated architecture which aims at reproducing joint interoperability among autonomous systems. The paper proposes an experimentation over a scenario developed for the maritime context that uses an innovative simulator. The authors' goal, during such research, consists of identifying requirements related to these simulators so that they accurately keep into account the most important elements affecting real operative context. This analysis is addressing training (Kennedy, 2010), engineering and it could be further developed for supporting or operation supervision. General architecture devoted to integrate such simulators within a federation, together with the approach that has been used in order to carry out this operation, represent the subjects of this paper; the mission environment has been created with the only goal to test the federation, and similarly simulation architecture and conceptual models are validated through proposed preliminary activities.
2015
- Computational thinking for beginners: {A} successful experience using
Prolog
[Relazione in Atti di Convegno]
Beux, Silvio; Briola, Daniela; Corradi, Andrea; Delzanno, Giorgio; Ferrando, Angelo; Frassetto, Federico; Guerrini, Giovanna; Mascardi, Viviana; Oreggia, Marco; Pozzi, Francesca; Solimando, Alessandro; Tacchella, Armando
abstract
2015
- Global protocols as first class entities for self-adaptive agents
[Relazione in Atti di Convegno]
Ancona, Davide; Briola, Daniela; Ferrando, Angelo; Mascardi, Viviana
abstract
We describe a framework for top-down centralized self-adaptive MASs where adaptive agents are "protocol-driven" and adaptation consists in runtime protocol switch.
Protocol specifications take a global, rather than a local, perspective and each agent, before starting to follow a new (global) protocol, projects it for obtaining a local version. If all the agents in the MAS are driven by the same global protocol, the compliance of the MAS execution to the protocol is obtained by construction.
2015
- Parametric protocol-driven agents and their integration in {JADE}
[Relazione in Atti di Convegno]
Ferrando, Angelo
abstract
2015
- Runtime verification of fail-uncontrolled and ambient intelligence systems: A uniform approach
[Articolo su rivista]
Ancona, Davide; Briola, Daniela; Ferrando, Angelo; Mascardi, Viviana
abstract
We propose an approach for designing, formalizing and implementing, on top of existing MultiAgent Systems and without interfering with them, sentinels that detect errors in fail-uncontrolled multiagent systems , and controllers that identify particular situations in ambient intelligence (AmI) systems . The formalism we use for representing the expected patterns of actions is that of trace expressions extended with features for dealing with exceptions, timeouts, and their handlers. In this paper we provide the syntax and semantics of the extended trace expressions formalism and examples of their use, in the different contexts of fail-uncontrolled and AmI systems.
2014
- Development planning based on interoperable agent driven simulation
[Articolo su rivista]
Massei, M; Poggi, S; Agresta, Matteo; Ferrando, Angelo
abstract
Abstract
The paper presents the potential of using interoperable agent driven simulation to support development planning; indeed the use of simulation represents a strong benefit to improve planning of infrastructures and plants devoted to disaster relief, civil protection and/or support to country development; the paper describes models used to face these challenges and last updates in population modeling for these applications. The proposed models include population characteristics, need as well as their social networks. In humanitarian support operations and country reconstruction there is a huge potential to use simulators; the paper describes how these models should be designed to support training as well operational planning. The models should be able to consider the impacts of contingencies as well as to guarantee the quick responsiveness requirements for humanitarian crisis management. The authors propose a simulator to be shared and used among Armed Forces and Civil Agencies for addressing Crisis Management, Humanitarian Missions, Country Reconstruction and Development considering joint operations (i.e. Civil Military Cooperation); indeed the paper outlines the importance of training people devoted to guarantee interoperability among civil organization and military units in this sector. The paper describes the models based on interoperable simulation as well as the agents driving the entities during the simulation to create quickly complex scenarios able to consider the impact on population and communities of the different actions by including human behavioral models. The proposed approach guarantees interoperability among different simulators within an HLA (High Level Architecture) federation in order to recreate crisis scenarios combining detailed simulation of multiple factors. The proposed approach is verified and validated by proposing an experimental analysis where it is evaluated a set of construction projects (i.e. digging wells) in a stabilization area and their effectiveness both in terms of direct result (i.e. water availability) as well as of population consensus and disaster relief (i.e. stress mitigation, trustiness respect supporting players). (C) 2014 Published by Elsevier B.V.