Title: A formalism and a framework for distributed runtime verification of multiagent systems
Speaker: Viviana Mascardi
Authors: Daniela Briola, Viviana Mascardi, Davide Ancona
Abstract: Verifying properties of interactions taking place inside open, complex, distributed, dynamic systems is of paramount importance for most applications and is mandatory for safety-critical ones. Verification can take place at design time (offline or static verification) or at runtime (online or dynamic). For runtime verification some layer between the monitor executing the verification engine and the system under monitoring must exist, so that actual interactions can be intercepted and the compliance of each one against the protocol can be checked. A common way to improve efficiency and fault tolerance of the runtime verification is to distribute it among many monitors. This requires that the protocol is projected onto subsets of participants. If the system has been engineered as a multiagent system (MAS), which is a good option when openness, complexity, distribution, dynamics are characterizing features, then the choice of either JADE, http://jade.tilab.com, or Jason http://jason.sourceforge.net/, as the platform for implementing it may be a very natural one. In this presentation we discuss the framework for distributed runtime verification of MASs that we designed and implemented. The framework consists of: (1) a formalism for describing agent interaction protocols (AIPs) based on constrained global types and their extension with attributes; (2) a mechanism for projecting AIPs onto subsets of agents, obtaining a new protocol in the same formalism of constrained global types; (3) a mechanism for verifying that interactions are compliant with the AIP; and (4) a mechanism for intercepting messages involving the agents under monitoring, be them JADE or Jason ones.
D. Ancona, M. Barbieri, and V. Mascardi. Constrained global types for dynamic checking of protocol conformance in multi-agent systems. In SAC. ACM, 2013.
D. Ancona, D. Briola, A. E. F. Seghrouchni, V. Mascardi, and P. Taillibert. Efficient verification of MASs with projections. In EMAS Pre-proceedings, 2014.
D. Ancona, S. Drossopoulou, and V. Mascardi. Automatic generation of self- monitoring MASs from multiparty global session types in Jason. In DALT X, volume 7784 of LNAI. Springer, 2012.
D. Briola, V. Mascardi, and D. Ancona. Distributed runtime verification of JADE multiagent systems. In IDC, Studies in Computational Intelligence. Springer, 2014.
V. Mascardi and D. Ancona. Attribute global types for dynamic checking of protocols in logic-based multiagent systems. TPLP, 13(4-5-Online-Supplement), 2013.
V. Mascardi, D. Briola, and D. Ancona. On the expressiveness of attribute global types: The formalization of a real multiagent system protocol. In AI*IA, 2013.