This work introduces RIVERtools, an IDE supporting the use of the “trace expressions” formalism by users that want to perform runtime verification of their own system.
During the development of software systems, it is not rare having the necessity
to state that the implemented system meets our requirements. Generally this
happens in all kind of software systems, but becomes more difficult when we
increase the system complexity. In particular, if we focus on the development
of Multiagent Systems (MASs), it is extremely common to have the need for
checking the agents’ behaviour in order to verify if what we expect in theory
is also correctly achieved by our implementation in practice. When we work
on small and centralized systems we have the chance to use standard formal
approaches, such as Static Verification (for instance Model Checking). In the
MAS community there are many ad-hoc model checking tools such as AJPF
(Agent JavaPathFinder) [
When the MAS becomes larger, model checking it (as well as the environment where it is immersed) becomes quickly intractable. In these scenarios, a valid alternative is Runtime Verification (RV). The main difference with respect to standard static verification is the stage when it is applied, which is execution time. In fact, in RV we do not need to simulate all possible paths that the system may generate during its execution, but we limit the analysis directly to the paths exposed and generated by the system during its real execution. As a consequence, RV could be more suitable and applicable than static verification in black-box scenarios, where there is no access to the source code of the system we want to verify.
Differently from static verification, very few tools expressly meant to runtime
verification of MASs exist. Besides [
As it happened for tools such as Jason2, Cartago3, and Moise4, where the need of a more modular, flexible and standardized framework brought to the creation of JaCaMo5, also for the RV of MAS there is the pressing need of a general purpose framework, with the objective to be modular with respect to the target system (the system must be seen as a black-box) and “programmerfriendly” focusing on the reuse of the developed software. Following this aim we developed RIVERtools, an Integrated Development Environment (IDE) for supporting the automatic generation of code to be used to implement the blackbox RV engine of a generic software systems - focusing on challenging scenarios where the target system is a MAS.
RIVERtools is proposed as a generic, modular and domain independent IDE to achieve the runtime verification of any target system. Rather than other solutions proposed in literature, RIVERtools tries to born as a “multi-target” IDE for the generation of monitors that can be used to achieve the runtime verification of different systems. Obviously we can achieve the same results without using an IDE, but using RIVERtools we have the great advantage to write our specifications once and for all (supported by highlights, syntax and type checking), leaving the technical details at a lower level that can be implemented just one time for each new target system of interest (updating the compiler without changing the high level specification).
The RIVERtools main features can be summarized as follows: – support during the definition of our properties (the formalism presented in
Section 2); – abstraction from the domain specific target, with RIVERtools we can define our specification leaving all technical details to the IDE compiler (presented in Section 4); – automatic integration of the properties inside the runtime verification process; – extensibility since its structure is based on the presence of “connectors-tosomething” (for each new target system to be verified, we define a new “connector-to-target” updating the RIVERtools compiler).
The main objective of RIVERtools is to separate and generalize the writing of monitors to achieve the runtime verification of any possible target system. In this paper we focus on its initial exploitation in the MAS context, in particular in the Jade framework.
First of all we have to present the formalism that we can use inside RIVERtools, in the next section we present briefly its syntax giving the semantics by intuition. 1 https://www.google.it/search?q=runtime+verification+of+multiagent+systems 2 http://jason.sourceforge.net/wp/index.php 3 http://cartago.sourceforge.net 4 http://moise.sourceforge.net 5 http://jacamo.sourceforge.net
Trace expressions are a specification formalism expressly designed for RV; they
are an evolution of multiparty global session types [
A trace expression represents a set of possibly infinite event traces, and is defined on top of the following operators: 1. (empty trace), denoting the singleton set f g containing the empty event trace ; 2. #: (prefix ), denoting the set of all traces whose first event e matches the event type6 # (e 2 #), and the remaining part is a trace of ; 3. 1 2 (concatenation), denoting the set of all traces obtained by concatenating the traces of 1 with those of 2; 4. 1^ 2 (intersection), denoting the intersection of the traces of 1 and 2; 5. 1_ 2 (union), denoting the union of the traces of 1 and 2; 6. 1j 2 (shuffle), denoting the set obtained by shuffling the traces of 1 with the traces of 2; 7. # (filter ), a derived operator denoting the set of all traces contained in , when deprived of all events that do not match #; 8. <X; > (binder ), binds the free occurrences of X in ; accordingly, the trace expression obtained from by substituting all free occurrences of X 2 dom( ) in with (X).
The semantics of trace expressions is specified by the transition relation T E T, where T and E denote the set of trace expressions and of events, respectively. As it is usual, we write 1 !e 2 to mean ( 1; e; 2) 2 . If the trace expression 1 specifies the current valid state of the system, then an event e is considered valid iff there exists a transition 1 !e 2; in such a case, 2 will specify the next valid state of the system after event e. Otherwise, the event e is not considered to be valid in the current state represented by 1.
Without loss of generality, in the rest of the paper we focus only on communicative events (message exchange). 3
We consider the SWI-Prolog7 implementation of the trace expression formalism; the RV pipeline can be summarized as: 1. the implementation of the operational semantics modeled by
Prolog; 2. the definition of a trace expression in SWI-Prolog; in SWI6 To be more general, trace expressions are built on top of event types (chosen from a set ET), rather than of single events; an event type denotes a subset of E. 7 http://www.swi-prolog.org 3. the implementation of a library to allow the communication between SWIProlog and the target system we want to verify (in the following we will refer to it as the connector); 4. the writing of a “main” file which uses this library; 5. the execution of the “main” file to perform the runtime verification of the target system.
What is extremely important to note is that the components involved in the RV process are: a SWI-Prolog library (1), a trace expression (2), a library to integrate SWI-Prolog with the system (the connector) (3) and a file to start everything correctly (4). But among these, only the trace expression (2) needs to be defined each time by the programmer. In fact, when the target system is chosen, (1) and (3) can be implemented once and for all; and the “main” file (4) can be automatically generated starting from the trace expression (2). Following this intuition, we created an IDE which supports the automatic generation of as much components as possible among the needed ones, and that helps the programmer in correctly representing the trace expression that models the interaction protocol to be verified. 4
RIVERtools has been developed using Xtext 8, a framework for development of programming languages and domain-specific languages which can be integrated as an Eclipse9 plugin. With respect to other frameworks, Xtext has been chosen above all for its support to the Xtend 10 language (a dialect of Java). 8 https://eclipse.org/Xtext/ 9 https://www.eclipse.org 10 http://www.eclipse.org/xtend/ user compile
.pl .java RIVERtools compile τ compile
Jade
Connector .pl .asl .pl .js
Jason Connector
Node Connector
Jade Jason Node.js τ compile RIVERtools
user – syntax checking, – type checking (contractiveness, decentralization), – roles, event types and events definition, and so on.
Referring to the second point, a trace expression is contractive if all its infinite
paths contain the prefix ‘:’ operator [
Keeping in mind the summarization made in Section 3, we have a trace expression defined using RIVERtools, the SWI-Prolog library and the connector to the target system. From these, we need to create the SWI-Prolog representation of the trace expression to be used inside the SWI-Prolog library (where the trace expression operational semantics is implemented), and the “main” file to properly initialize and run the connector. These two files are automatically generated by RIVERtools by compiling the trace expression.
In more detail, the new RV pipeline using the trace expression formalism with the RIVERtools integration can be summarized as: 1. the user writes the trace expression inside RIVERtools and chooses the target system; 2. RIVERtools checks the correctness of the trace expression and, if it is correct, generates the SWI-Prolog representation of the trace expression and the “main” file for the target system; 3. the “main” file, using the SWI-Prolog library and the connector to the target system, can be used by the user to start the RV process. The trace expression structure that is recognized and managed by RIVERtools is expressed by the grammar below. htrace_expressioni ::= ‘interaction_trace_expression’ ‘{’ ‘id:’ hatomi ‘target:’ htarget i ‘body:’ htermi+ ‘roles:’ hrolei* ‘types:’ (htypei ‘:’ ‘{’ (hrolei ‘=>’ hrolei ‘:’ hcontent i (‘[’ (hconditioni)+ ‘]’)?)+ ‘}’ ‘[’ hchannel i ‘]’)* (‘threshold:’ hreliabilityi)? (‘channels:’ (hchannel i (‘[’ hreliabilityi ‘]’)?)+)? ‘}’
We have seven different fields: – id: is the name of the protocol; – target: is the target system to verify; – body: is the collection of terms representing the body of the protocol, it follows the trace expression syntax presented in Section 2; – roles: is the set of roles involved in the event types of the protocol; – types: is the set of event types used in body; – threshold: (optional) is the minimum level for the reliability allowed by the protocol (it will be more cleare after); – channels: (optional) is the set of channels available for the communication between the roles.
We can better understand the syntax through an example.
interaction_trace_expression { id : ping_pong target : jade body :
pingPong < ping : pong : pingPong roles : a l i c e bob types : ping : { a l i c e => bob : h e l l o } [ email ] pong : { bob => a l i c e : world } [ sms ] threshold : 0 . 7 channels : email [ 0 . 8 ] sms } This is a simple representation of a ping-pong protocol. Since the target system is set to jade the roles involved are automatically considered as agents, in particular here we have two agents involved: alice and bob. The protocol identifier is ping_pong. The protocol we want to verify (the body) consists in one ping followed by one pong followed by one ping and so on infinitely. The event types involved in the protocol are explicitly defined: ping corresponds to the interaction event hello sent by alice to bob using the email channel and pong corresponds to the interaction event world sent by bob to alice using the sms channel. These two channels must be also defined with their respective reliabilities, for instance in this case we have that the email channel is more reliable than the sms channel. The threshold level for the channels is also defined.
The threshold field is used to set the level of reliability under which we do
not trust a channel. When the reliability of a channel is under the threshold
RIVERtools automatically considers “optional” all the event types using this
channel. For instance, if we have a channel sms with reliability 0.3, the threshold
set to 0.7, and an event type ping:{alice => bob : hello}[sms], each time
we use ping inside the body field, i.e. ping:t (where t is the continuation of the
trace expression after the prefix operator), RIVERtools automatically compiles it
in ((ping:epsilon)\/(epsilon))*(t) meaning that the event matching ping
can be missing. If we set the threshold to a smaller value, for instance 0.2, we
are relaxing our reliability requirements and since the sms channel has a greater
reliability value, it will not be modified by RIVERtools because we are trusting
all the channels with reliability greater than 0.2. In case of the limit scenario
where the reliability of a channel is 0, RIVERtools will remove from the protocol
all the occurrences of the event types using it. This particular case becomes
interesting when we focus on distribution features, because we can write a correct
protocol in which we explicit all the event interactions but when we exploit it in
a real world we discover that not all events are observable. This issue can bring
to have missing information during the decentralization of our specifications.
Thanks to the explicit representation of such absence of reliability, RIVERtools
can analyze the trace expression considering these kind of unavailability and can
achieve a correct decentralization without losing information (for more details
about how to decentralize properly an agent interaction protocol defined using
a trace expression see [
The channel integration inside the runtime verification process is a task for the connector and it is totally domain dependent.
When a channel is not indicated for an event type, the default one is chosen whose reliability is 1. The same happens for the channels, if the reliability is not given, the reliability is set to 1 (in the ping_pong example the sms channel has reliability 1).
Starting from the trace expression, RIVERtools generates its SWI-Prolog implementation and the system dependent “main” file (in this case a Java file since the target is Jade) to use the Jade-Connector and the SWI-Prolog library. The programmer will provide its own MAS implemented in Jade and using the “main” file it will be possible to perform RV on it. In more details, since Jade is a Java framework used to implement MASs, the Jade-Connector is a Java library containing both all the primitives to sniff the events generated by the agents developed by the programmer and the code necessary to use the SWI-Prolog library containing the trace expression semantics implementation. In this way, the only part that RIVERtools must generate is the SWI-Prolog implementation of the trace expression, all the rest is fixed and can be reused. It will be enough to run the “main” file (Java) providing: – the agents developed by the programmer; – the Jade-Connector library (in the build path); – the SWI-Prolog library (used by the Jade-Connector).
Let us suppose to have a MAS implemented in Jade representing a book-shop scenario. The involved agents are: alice, barbara, carol, dave, emily and frank. The protocol that we want to verify at runtime can be summarized in natural language as follow: 1. the agent alice sends a whatsApp message to the agent barbara asking to buy a book; 2. the agent barbara sends an email message to the agent carol asking to reserve the book in the bookshop; 3. the agent carol sends a whatsApp message to the agent dave asking to check the availability of the book; 4. the agent dave checks the availability of the book, and if the book is available (a) it sends a whatsApp message to the agent emily asking to take the book in the bookshop; (b) the agent emily sends an email message to the agent barbara saying that the book is available in the bookshop. otherwise (a) it sends an email message to the agent frank asking to order the book; (b) the agent frank sends a whatsApp message to the agent barbara saying that the book will be availabel in the bookshop in two days.
The corresponding trace expression representation inside RIVERtools is:
Listing 1.1. Book-shop trace expression written inside RIVERtools. t r a c e _ e x p r e s s i o n { id : book_purchase target : jade body : purchaseBook < buy : r e s e r v e : checkAvail : ( take2Shop : availNow : epsilon \/ order : avail2Days : epsilon ) roles :
a l i c e , barbara , c a r o l , dave , emily , frank
types :
buy : { a l i c e => barbara : buy_me_book} [ whatsApp ]
r e s e r v e : { barbara => c a r o l : reserve_me_book } [ email ]
checkAvail : { c a r o l => dave : i s _ a v a i l a b l e ? } [ whatsApp ]
take2Shop : { dave => emily : send_me_book } [ whatsApp ]
availNow : { emily => barbara : book_available } [ email ]
order : { dave => frank : order_book } [ email ]
avail2Days : { frank => barbara : book_in_2_days } [ whatsApp ]
threshold : 0 . 6
channels :
email [ 0 ]
whatsApp [
In this example we have two kinds of channels used by the agents to communicate: email and whatsApp. We point out the reliability of the two corresponding channels. The whatsApp channel has reliability set to 1, while the email channel has the reliability set to 0. This means that, during RV, we expect the monitor not to be able to observe messages passed on the email channel. This may be due to any reason, for example lack of permissions or unavailability of information. Thanks to the presence of explicitly declared channels, RIVERtools can take into account the channel reliability during the correctness checking for the trace expression. Channel reliability may impact on contractiveness and decentralization of the original trace expression (as observed in Section 4.1): RIVERtools takes channel reliability into account when automatically performs those checks.
Compiling this trace expression, RIVERtools generates the two files book_purchase.pl and BookPurchase.java. Providing the connector library for Jade and the MAS implementation of the book-shop, it will be enough to execute the main method of the BookPurchase class to achieve the RV of a Jade MAS. Once obtained this Java class and the trace expression SWI-Prolog representation, the programmer can simply execute the verifier without adding a single line of code.
Listing 1.2. BookPurchase.java automatically generated by RIVERtools. public c l a s s BookPurchase { public s t a t i c void main ( S t r i n g [ ] a r g s )
throws StaleProxyException , IOException { /∗ Call at the SWI Prolog l i b r a r y ∗/ J P L I n i t i a l i z e r . i n i t ( ) ; /∗ R e g i s t r a t i o n of the t r a c e expression generated by RIVERtools ∗/ TraceExpression tExp = new TraceExpression ( " book_purchase . p l " ) ; /∗ I n i t i a l i z e JADE environment ∗/ jade . c o r e . Runtime runtime = jade . c o r e . Runtime . i n s t a n c e ( ) ; P r o f i l e p r o f i l e = new P r o f i l e I m p l ( ) ; AgentContainer c o n t a i n e r = runtime . createMainContainer ( p r o f i l e ) ; // the same f o r barbara , carol , dave , emily and frank // . . . /∗ Create a s i n g l e c e n t r a l i z e d monitor v e r i f y i n g the t r a c e expression tExp ∗/ S n i f f e r M o n i t o r F a c t o r y . createAndRunCentralizedMonitor ( tExp , c o n t a i n e r , agents ) ; /∗ Channels c r e a t i o n ( here are simulated ) ∗/ Channel . addChannel (new SimulatedChannel ( " email " , 0 ) ) ; Channel . addChannel (new SimulatedChannel ( " whatsapp " , 1 ) ) ; /∗ Run the agents ∗/ for ( Agent agent : agents ) {
agent . s t a r t ( ) ; }
} 5.1
Screenshots In the following we reported screenshots showing some of the typical errors handled by RIVERtools.
The book-shop scenario in RIVERtools: In Figure 2 we have defined inside
RIVERtools the book-shop trace expression presented in Section 5. Even though
the trace expression reported is the same, we can note two new fields that have
been omitted previously, decentralized and partition. These two fields are
used by RIVERtools to generate BookPurchase.java that exploits a
decentralized set of monitors rather than only one centralized (for more details about how
the decentralized algorithm works see [
Partition not valid: In Figure 3 we change the reliability of the email channel
from 1 to 0. Unfortunately, doing in this way we cannot distribute the runtime
verification on each single role because we could lose information. This is handled
by RIVERtools that communicates to the programmer that the current proposed
partition is not allowed (because two critical points are not satisfied [
Event types existence: In Figure 5 we remove an event type from the types field. After that, RIVERtools finds the corresponding use inside the terms consisting the protocol body, and it communicates to the programmer about the use of an event type undefined. In this demo paper we have presented RIVERtools, an IDE that can be used for the integration of the trace expression formalism with any possible target system. Thanks to the presence of connectors that handle all the domain dependent issues, we have showed that RIVERtools allows focusing on a more abstract level leaving all technical details to the connector implementation. In this demo paper we have presented the RIVERtools general structure and we have analyzed its possible use through an example involving a book-shop scenario developed as a MAS in Jade. Since RIVERtools is at the beginning, we have not already tested it on a real scenario, but it is our intention to deploy it in some challenging context where will be necessary to exploit the expressivity of our formalism.
The future directions of our work will include to implement connectors to other target systems. In the MAS context, we plan to add a connector to Jason. Outside the MAS community, we will explore the possibility of an integration with some general purpose system, as Node.js11, which has already been used in fascinating scenarios like the Internet of Things (IoT). 11 https://nodejs.org/ 17. M. Wooldridge, M. Huget, M. Fisher, and S. Parsons. Model checking for multiagent systems: the Mable language and its applications. International Journal on Artificial Intelligence Tools, 15(2):195–226, 2006.