Distributed Runtime Verification of JADE and Jason Multiagent Systems with Prolog

Verifying that interactions taking place inside a multiagent system (MAS) are compliant to the expected ones is of paramount importance for most systems and is mandatory for safety-critical applications. Runtime verification requires that the global protocol modeling interactions among agents is represented in a formal way, that interactions taking place among agents can be sniffed, possibly in a not intrusive way, and that a mechanism for verifying that a sniffed interaction is compliant to the global protocol exists. Projecting the global protocol onto agents' subsets can further improve efficiency and fault tolerance by allowing the distribution of the verification mechanism. We implemented monitor agents for both the JADE and the Jason well known agent frameworks, able to achieve all the goals above using the ``attribute global types'' formalism for representing protocols. The algorithms for monitoring and projection are entirely implemented in Prolog. They are integrated into Jason directly, as Jason agents can integrate Prolog knowledge natively, and into JADE by means of the JLP library providing a bidirectional interface between Java and SWI Prolog.