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 (o✏ine 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 eciency 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. JADE, implemented in Java, is the state-of-the-art tool for MAS development and has been used for many real industrial applications. Jason, implemented in Java as well and based on a Prolog engine built from scratch by its developers, is one of the most widely used frameworks when the agents under development are designed according to the Belief, Desire, Intentions (BDI) architecture. Due to the wide range of possible application fields of Jason and to the large amount of real use cases of JADE, being able to verify interactions taking place in MASs implemented in one of these two frameworks is a concrete step towards making MASs more reliable and enhancing their industrial and commercial usability. In this demo we show our contribution for the achievement of this goal. We have in fact designed and implemented a framework for distributed runtime verification of MASs and ad hoc interfaces for monitoring JADE and Jason interactions. The framework consists of four layers: (1) a formalism for describing agent interaction protocols (AIPs) based on constrained global types [1] and their extension with attributes [7]; (2) a mechanism for projecting AIPs onto subsets of agents, obtaining a new protocol in the same formalism of constrained global types [2]; (3) a mechanism for verifying that interactions are compliant
Introduction
? Paper presented at the CILC 2014 Demo Session, based on published material [
The strength of our framework, represented in Figure 1, is its high modularity and potential for code reuse: the first three layers are independent from the actual MAS under monitoring and have been implemented in Prolog. The “protocol representation” and “compliance verification” layers have been tested and improved over time, reaching an almost stable version now, whereas the projection layers works under the assumption that the protocol contains no attributes (namely, it is a “plain” constrained global type) and has not been tested extensively yet. The fourth layer depends on the MAS framework under monitoring: nothing prevents us from adding new agent frameworks at the bottom of our architecture by developing ad hoc mechanisms for message interception, still leaving the first three layers unchanged. By exploiting the components o↵ered by our stacked framework it is possible to implement both monitors external to the MAS, implemented as completely separate processes that do not intervene in the observed system, and agents which are able to monitor the protocol executions and have the power to intervene when they detect a violation. Associating the “compliance verification” capability with an artifact (as in the first case) or with an agent (as in the second case) are two di↵erent design choices, each with pros and cons. We experimented both approaches, as discussed in Section 3 where monitoring is performed by a Java artifact that does not intervene in the MAS activity, and in Section 4 where the Jason agent in charge of the monitoring activity can prevent other agents from sending non compliant messages.
Whatever the choice, compliance verification should be an ecient process. Although eciency issues are still to be explored, distributing the runtime verification by projecting onto subsets of agents could be a way to balance the load of the monitoring activity among more entities. 2
Background
Global types [
SERVER = (receive request,0):(serve request,0):SERVER where SERVER is a logical variable which is unified with a recursive (or cyclic, or infinite) Prolog term consisting of a receive request producer interaction type, followed by a serve request producer interaction type (both requiring 0 consumers), followed by the term itself. This protocol models the (infinite) behavior of a server which is always ready to receive and serve requests; the only valid interaction trace is the infinite sequence receive request serve request receive request serve request ....
By means of attribute global types we were able to concisely represent
protocols which are well known in the concurrent systems and MAS communities
like the Alternating Bit Protocol (en.wikipedia.org/wiki/Alternating bit
protocol) and the FIPA Iterated Contract Net Protocol (fipa.org/specs/fipa00030).
FYPA (Find Your Path, Agent! [
Constrained global types can be easily expressed as a set of Prolog
equations like the one defining SERVER. Attributes and constraints on their values
are represented as additional Prolog facts. In order to allow agents to verify
only a sub-protocol of the global interaction protocol, we designed a
projection algorithm that takes a constrained global type and a set of agents Ags as
input, and returns a constrained global type which contains only interactions
involving agents in Ags as output [
Whatever the protocol to be monitored (global one or projection) and the framework (JADE or Jason), a monitor keeps track of the runtime evolution of the protocol by saving its current state (which is an attribute global type) and checking that each interaction taking place in the MAS is allowed by the current state (namely, can lead to a new state by means of the transition function which defines the semantics of attribute global types, implemented in Prolog). If the interaction is not allowed, an error is reported. The monitor also checks agents responsiveness by means of a time-out whose value can be set by the user: if the current state of the monitor corresponds to the empty protocol (that is, the protocol must terminate), then the monitor reports an error as soon as an interaction is detected (independently of the time-out); if the current state is not final (that is, the protocol is not allowed to terminate), then the monitor reports a warning as soon as the time-out expires, if no interaction is detected (and of course an error is reported in case an invalid interaction is detected before the time-out). 3
Runtime Verification of JADE MASs
In order to verify the interactions taking place in a JADE MAS, we have designed
a monitor meeting the following requirements for non intrusiveness and code
reuse [
To meet requirements 1 and 2 we extended the JADE Sni↵er agent which is able to sni↵ all the messages exchanged during the execution of the MAS in a non intrusive way: JADE is developed under the LGPL (Lesser General Public License) and the Java source code is available to the research community, so we were able to modify it to achieve our goals.
To meet requirements 3 and 4 we exploited the JLP library1 providing a bidirectional interface between Java and SWI Prolog. As all our previous work on attribute global types was implemented in Prolog, allowing our JADE Monitor to consult Prolog programs and to call Prolog predicates was the best way to ensure reusability.
The monitor reads a file containing the Prolog code implementing verification and projection, and a configuration file listing the agents to be monitored, and onto which the protocol projection will be performed. A log file is written as the monitoring goes on. The Prolog file contains definitions for three predicates: – initialize(LogFile, SniffedAgents) which sets LogFile as the file where writing the outcome of the verification, and projects the global protocol - which must be defined by the global type/1 predicate -, onto Sni↵edAgents.
– remember(ParsedMsg) which inserts the Prolog representation of the JADE sni↵ed message into a message list, where messages are ordered by time stamp (if they have a time stamp, which is not mandatory) or in order of arrival.
– verify(CurrentTime) which verifies the compliance of each message remembered in the message list and whose time stamp is lower than CurrentTime to the global protocol.
These predicates are called in di↵erent methods of the monitor code, implementing the wanted behavior.
With this approach no changes are required to the monitored agents and hence existing MASs can be monitored without accessing to their code, but the monitor detects a violation only after it took place and even in case of a protocol violation the MAS execution goes on. 1 http://www.swi-prolog.org/packages/jpl/java api/
Runtime Verification of Jason MASs
Since Jason agents can integrate Prolog facts and rules for defining their
knowledge, the Jason monitor [
The first plan is triggered by the !my send internal goal; my send has the same signature as the .send internal action, but, instead of sending a message with performative Perf and Content to Receiver, it sends a tell message to the monitor with content msg(Sender, Receiver, Perf, Content). When received, this message will be checked by the monitor against the attribute global type representing the protocol, as briefly explained in Section 2.
The second plan is triggered by the reception of the monitor’s message that allows the agent to actually send Content to Receiver. In reaction to the reception of such a message, the agent sends the corresponding message to the expected agent.
With this approach the code of the monitored agents must be conceived and implemented in a way that makes monitoring possible, but the monitor detects a violation prior than the actual message is sent and can stop the agent violating the protocol by not allowing it to send the “wrong” message.