Towards (decentralised) Runtime verification of multi-agent systems using trace expressions

24^th January 2019, 13:00
Angelo Ferrando

Abstract

Runtime verification (RV) is a method based on dynamic analysis to ensure correctness of a system by checking its event traces against a specification. In this talk I am going to present the RV approach which I have been studying and developing during my Ph.D. at the University of Genova (Italy). I will discuss how we can use the Trace Expression formalism to define complex specifications and how these can be verified dynamically. After having presented the formalism and its possible applications on black-box systems, I am going to present its use for the verification of more challenging scenarios, such as multi-agents systems (MAS). More specifically, I will show how to overcome the intrinsic decentralisation of MAS proposing a more scalable decentralised version of our RV approach. Finally, I will conclude with a demo of the IDE (https://github.com/AngeloFerrando/trace_expression_plugin_eclipse) developed for supporting the RV of MAS implemented using the JADE framework (http://jade.tilab.com/).

Additional Materials

• https://github.com/AngeloFerrando/trace_expression_plugin_eclipse