Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems.
Ferrando, A.; Dennis, L. A.; Cardoso, R. C.; Fisher, M.; Ancona, D.; and Mascardi, V.
ACM Trans. Softw. Eng. Methodol., 30(4). May 2021.
![Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems [link]](//bibbase.org/img/filetypes/link.svg "Paper")
Paper
doi
link
bibtex
abstract
7 downloads
@article{Ferrando21,
author = {Ferrando, Angelo and Dennis, Louise A. and Cardoso, Rafael C. and Fisher, Michael and Ancona, Davide and Mascardi, Viviana},
title = {Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems},
year = {2021},
issue_date = {May 2021},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {30},
number = {4},
issn = {1049-331X},
url = {https://doi.org/10.1145/3447246},
doi = {10.1145/3447246},
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 article 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.},
journal = {ACM Trans. Softw. Eng. Methodol.},
month = may,
articleno = {43},
numpages = {43},
keywords = {autonomous systems, model checking, trace expressions, Runtime verification, MCAPL}
}
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 article 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.
Agile Tasking of Robotic Systems with Explicit Autonomy.
Cardoso, R. C.; Michaloski, J. L.; Schlenoff, C.; Ferrando, A.; Dennis, L. A.; and Fisher, M.
In
The International FLAIRS Conference Proceedings, volume 34, 2021.
doi
link
bibtex
@InProceedings{Cardoso21b,
title={Agile Tasking of Robotic Systems with Explicit Autonomy},
volume={34},
DOI={10.32473/flairs.v34i1.128481},
booktitle={The International FLAIRS Conference Proceedings},
author={Cardoso, Rafael C. and Michaloski, John L. and Schlenoff, Craig and Ferrando, Angelo and Dennis, Louise A. and Fisher, Michael},
year={2021}
}
An Overview of Verification and Validation Challenges for Inspection Robots.
Fisher, 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.; and Webster, M.
Robotics, 10(2). 2021.
Paper
doi
link
bibtex
abstract
5 downloads
@article{robotics10020067,
author = {Fisher, Michael and Cardoso, Rafael C. and Collins, Emily C. and Dadswell, Christopher and Dennis, Louise A. and Dixon, Clare and Farrell, Marie and Ferrando, Angelo and Huang, Xiaowei and Jump, Mike and Kourtis, Georgios and Lisitsa, Alexei and Luckcuck, Matt and Luo, Shan and Page, Vincent and Papacchini, Fabio and Webster, Matt},
title = {An Overview of Verification and Validation Challenges for Inspection Robots},
journal = {Robotics},
volume = {10},
year = {2021},
number = {2},
url = {https://www.mdpi.com/2218-6581/10/2/67},
issn = {2218-6581},
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.},
doi = {10.3390/robotics10020067}
}
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.
Agents and Robots for Reliable Engineered Autonomy:A Perspective from the Organisers of AREA 2020.
Cardoso, R. C.; Ferrando, A.; Briola, D.; Menghi, C.; and Ahlbrecht, T.
Journal of Sensor and Actuator Networks, 10(2). 2021.
Paper
doi
link
bibtex
abstract
5 downloads
@article{cardoso21e,
AUTHOR = {Cardoso, Rafael C. and Ferrando, Angelo and Briola, Daniela and Menghi, Claudio and Ahlbrecht, Tobias},
TITLE = {Agents and Robots for Reliable Engineered Autonomy:A Perspective from the Organisers of AREA 2020},
JOURNAL = {Journal of Sensor and Actuator Networks},
VOLUME = {10},
YEAR = {2021},
NUMBER = {2},
ARTICLE-NUMBER = {33},
URL = {https://www.mdpi.com/2224-2708/10/2/33},
ISSN = {2224-2708},
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.},
DOI = {10.3390/jsan10020033}
}
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.
A Review of Verification and Validation for Space Autonomous Systems.
Cardoso, R. C.; Kourtis, G.; Dennis, L. A.; Dixon, C.; Farrell, M.; Fisher, M.; and Webster, M.
Current Robotics Reports. Jun 2021.
Paper
doi
link
bibtex
abstract
7 downloads
@Article{Cardoso21d,
author={Cardoso, Rafael C.
and Kourtis, Georgios
and Dennis, Louise A.
and Dixon, Clare
and Farrell, Marie
and Fisher, Michael
and Webster, Matt},
title={A Review of Verification and Validation for Space Autonomous Systems},
journal={Current Robotics Reports},
year={2021},
month={Jun},
day={18},
abstract={The deployment of hardware (e.g., robots, satellites, etc.) to space is a costly and complex endeavor. It is of extreme importance that on-board systems are verified and validated through a variety of verification and validation techniques, especially in the case of autonomous systems. In this paper, we discuss a number of approaches from the literature that are relevant or directly applied to the verification and validation of systems in space, with an emphasis on autonomy.},
issn={2662-4087},
doi={10.1007/s43154-021-00058-1},
url={https://doi.org/10.1007/s43154-021-00058-1}
}
The deployment of hardware (e.g., robots, satellites, etc.) to space is a costly and complex endeavor. It is of extreme importance that on-board systems are verified and validated through a variety of verification and validation techniques, especially in the case of autonomous systems. In this paper, we discuss a number of approaches from the literature that are relevant or directly applied to the verification and validation of systems in space, with an emphasis on autonomy.
RVPLAN: A General Purpose Framework for Replanning using Runtime Verification.
Ferrando, A.; and Cardoso, R. C.
In
Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21), 2021.
link
bibtex
@inproceedings{FerrandoVortex,
title={RVPLAN: A General Purpose Framework for Replanning using Runtime Verification},
author={Ferrando, Angelo and Cardoso, Rafael C.},
booktitle={Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21)},
year={2021}
}
Increasing Confidence in Autonomous Systems.
Fisher, M.; Ferrando, A.; and Cardoso, R. C.
In
Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21), 2021.
link
bibtex
@inproceedings{fisher2021increasing,
title={Increasing Confidence in Autonomous Systems},
author={Fisher, Michael and Ferrando, Angelo and Cardoso, Rafael C.},
booktitle={Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX'21)},
year={2021}
}
Agile Tasking of Robotic Kitting.
Michaloski, J.; Aksu, M.; Schlenoff, C.; Cardoso, R. C.; and Fisher, M.
In
Proceedings of the ASME 2021 International Mechanical Engineering Congress and Exposition (IMECE2021), 2021.
link
bibtex
@inproceedings{JohnIMECE,
title={Agile Tasking of Robotic Kitting},
author={Michaloski, John and Aksu, Murat and Schlenoff, Craig and Cardoso, Rafael C. and Fisher, Michael},
booktitle={Proceedings of the ASME 2021 International Mechanical Engineering Congress and Exposition (IMECE2021)},
year={2021}
}
Automated Planning and BDI Agents: A Case Study.
Cardoso, R. C.; Ferrando, A.; and Papacchini, F.
In Dignum, F.; Corchado, J. M.; and De La Prieta, F., editor(s),
Advances in Practical Applications of Agents, Multi-Agent Systems, and Social Good. The PAAMS Collection, pages 52–63, Cham, 2021. Springer International Publishing
doi
link
bibtex
abstract
2 downloads
@inproceedings{Cardoso21e,
author="Cardoso, Rafael C.
and Ferrando, Angelo
and Papacchini, Fabio",
editor="Dignum, Frank
and Corchado, Juan Manuel
and De La Prieta, Fernando",
title="Automated Planning and BDI Agents: A Case Study",
booktitle="Advances in Practical Applications of Agents, Multi-Agent Systems, and Social Good. The PAAMS Collection",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="52--63",
abstract="There have been many attempts to integrate automated planning and rational agents. Most of the research focuses on adding support directly within agent programming languages, such as those based on the Belief-Desire-Intention model, rather than using off-the-shelf planners. This approach is often believed to improve the computation time, which is a common requirement in real world applications. This paper shows that even in complex scenarios, such as in the Multi-Agent Programming Contest with 50 agents and a 4 s deadline for the agents to send actions to the server, it is possible to efficiently integrate agent languages with off-the-shelf automated planners. Based on the experience with this case study, the paper discusses advantages and disadvantages of decoupling the agents from the planners.",
isbn="978-3-030-85739-4",
doi={10.1007/978-3-030-85739-4_5}
}
There have been many attempts to integrate automated planning and rational agents. Most of the research focuses on adding support directly within agent programming languages, such as those based on the Belief-Desire-Intention model, rather than using off-the-shelf planners. This approach is often believed to improve the computation time, which is a common requirement in real world applications. This paper shows that even in complex scenarios, such as in the Multi-Agent Programming Contest with 50 agents and a 4 s deadline for the agents to send actions to the server, it is possible to efficiently integrate agent languages with off-the-shelf automated planners. Based on the experience with this case study, the paper discusses advantages and disadvantages of decoupling the agents from the planners.
Special Issue: Agents and Robots for Reliable Engineered Autonomy.
Cardoso, R. C.; Ferrando, A.; Briola, D.; Menghi, C.; and Ahlbrecht, T.
Journal of Sensor and Actuator Networks, 10(3). 2021.
Paper
doi
link
bibtex
abstract
2 downloads
@Article{areaeditorial,
AUTHOR = {Cardoso, Rafael C. and Ferrando, Angelo and Briola, Daniela and Menghi, Claudio and Ahlbrecht, Tobias},
TITLE = {Special Issue: Agents and Robots for Reliable Engineered Autonomy},
JOURNAL = {Journal of Sensor and Actuator Networks},
VOLUME = {10},
YEAR = {2021},
NUMBER = {3},
ARTICLE-NUMBER = {47},
URL = {https://www.mdpi.com/2224-2708/10/3/47},
ISSN = {2224-2708},
ABSTRACT = {The study of autonomous agents is a well-established area that has been researched for decades, both from a design and implementation viewpoint [...]},
DOI = {10.3390/jsan10030047}
}
The study of autonomous agents is a well-established area that has been researched for decades, both from a design and implementation viewpoint [...]
Towards Partial Monitoring: It is Always too Soon to Give Up.
Ferrando, A.; and Cardoso, R. C.
In Farrell, M.; and Luckcuck, M., editor(s),
m̊ Proceedings Third Workshop on Formal Methods for Autonomous Systems, m̊ Virtual, 21st-22nd of October 2021, volume 348, of
Electronic Proceedings in Theoretical Computer Science, pages 38-53, 2021. Open Publishing Association
doi
link
bibtex
@inproceedings{FerrandoFMAS,
author = {Ferrando, Angelo and Cardoso, Rafael C.},
year = {2021},
title = {Towards Partial Monitoring: It is Always too Soon to Give Up},
editor = {Farrell, Marie and Luckcuck, Matt},
booktitle = {{\rm Proceedings Third Workshop on}
Formal Methods for Autonomous Systems,
{\rm Virtual, 21st-22nd of October 2021}},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {348},
publisher = {Open Publishing Association},
pages = {38-53},
doi = {10.4204/EPTCS.348.3},
}
MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest.
Cardoso, R. C.; Ferrando, A.; Papacchini, F.; Luckcuck, M.; Linker, S.; and Payne, T. R.
In Ahlbrecht, T.; Dix, J.; Fiekas, N.; and Krausburg, T., editor(s),
The Multi-Agent Programming Contest 2021, pages 82–107, Cham, 2021. Springer International Publishing
doi
link
bibtex
abstract
2 downloads
@InProceedings{Cardoso21f,
author="Cardoso, Rafael C.
and Ferrando, Angelo
and Papacchini, Fabio
and Luckcuck, Matt
and Linker, Sven
and Payne, Terry R.",
editor="Ahlbrecht, Tobias
and Dix, J{\"u}rgen
and Fiekas, Niklas
and Krausburg, Tabajara",
title="MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest",
booktitle="The Multi-Agent Programming Contest 2021",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="82--107",
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.",
isbn="978-3-030-88549-6",
doi="10.1007/978-3-030-88549-6_4"
}
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.
![ML-MAS: A Hybrid AI Framework for Self-Driving Vehicles [link]](http://bibbase.org/img/filetypes/link.svg "Paper")
Paper
doi
link
bibtex
abstract
20 downloads
![Safety Shields, an Automated Failure Handling Mechanism for BDI Agents [pdf]](//bibbase.org/img/filetypes/pdf.svg "Paper")
Paper
link
bibtex
3 downloads
![Safety Shields, an Automated Failure Handling Mechanism for BDI Agents [pdf]](http://bibbase.org/img/filetypes/pdf.svg "Paper")
Paper
link
bibtex
3 downloads