@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: bib2bib -c 'keywords : "runtime-verification"' /home/davide/latex/bibinputs/allMine.bib}}
@comment{{This file has been generated by Pybliographer}}
@inproceedings{AnconaEtAl16,
author = {Ancona, D. and
Ferrando, A. and
Mascardi, V.},
title = {Comparing Trace Expressions and Linear Temporal Logic for Runtime
Verification},
booktitle = {Theory and Practice of Formal Methods - Essays Dedicated to Frank
de Boer on the Occasion of His 60th Birthday},
pages = {47--64},
year = {2016},
abstract = {{Trace expressions are a compact and expressive formalism, initially devised
for runtime verification of agent interactions in multiagent systems, which has been
successfully employed to model real protocols, and to generate monitors for mainstream multiagent system platforms,
and generalized to support runtime verification of different kinds of properties and systems.
In this paper we formally compare the expressive power of trace expressions with
the Linear Temporal Logic (LTL), a formalism widely adopted in runtime verification.
We show that any LTL formula can be translated into a trace expression
which is equivalent from the point of view of runtime verification.
Since trace expressions are able to express and verify sets of traces that
are not context-free, we can derive that in the context of runtime verification
trace expressions are more expressive than LTL.
}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaEtAlFdB16.pdf},
keywords = {agents, behavioral-types,runtime-verification}
}
@inproceedings{AnconaBFMT14,
author = {Ancona, Davide and
Briola, Daniela and
El Fallah{-}Seghrouchni, Amal and
Mascardi, Viviana and
Taillibert, Patrick},
title = {Exploiting Prolog for Projecting Agent Interaction Protocols},
booktitle = {Proceedings of the 29th Italian Conference on Computational Logic,
Torino, Italy, June 16-18, 2014.},
pages = {30--45},
year = {2014},
abstract = {{Constrained global types are a powerful means to represent agent interaction protocols. In our recent research we demonstrated that they can be used to represent complex protocols in a very compact way, and we exploited them to dynamically verify correct implementation of a protocol in a real MAS framework, Jason.
The main drawback of our previous approach is the full centralization of the monitoring activity which is delegated to a unique monitor agent.
This approach works well for MASs with few agents, but could become unsuitable in communication-intensive and highly-distributed MASs where hundreds of agents should be monitored.
In this paper we define an algorithm for projecting a constrained global type onto a set of agents Ags,
by restricting it to the interactions involving agents in Ags, so that the outcome of the algorithm is
another constrained global type that can be safely used for verifying the compliance of the sub-system Ags to the protocol specified by the original constrained global type.
The projection mechanism is implemented in SWI Prolog and is the first step towards distributing the monitoring activity, making it safer and more efficient: the compliance of a MAS to a protocol could be dynamically verified by suitably partitioning the agents of the MAS into small sets
of agents, and by assigning to each partition Ags a local monitor agent which checks all interactions involving Ags against the projected constrained global type.
We leave for further investigation the problem of finding suitable partitions of agents in a MAS, to guarantee that
verification through projected types and distributed agents is equivalent to verification
performed by a single centralized monitor with a unique global type.}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaBFMT14.pdf},
keywords = {agents, behavioral-types,runtime-verification}
}
@inproceedings{AnconaEtAl13a,
booktitle = {{ACM Symposium on Applied Computing (SAC 2013)}},
keywords = {{agents, behavioral-types,runtime-verification}},
note = {{Poster paper}},
author = {Ancona, D. and Barbieri, M. and Mascardi, V.},
title = {{Constrained Global Types for Dynamic Checking of Protocol Conformance in Multi-Agent Systems}},
pages = {1-3},
year = {2013},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ABM-SAC13.pdf},
abstract = {Global types are behavioral types for specifying and verifying multiparty
interactions between distributed components, inspired by the process algebra approach.
In this paper we extend the formalism of global types in multi-agent systems resulted from our previous work with a mechanism for easily expressing constrained shuffle of message sequences; accordingly, we extend the semantics to include the newly introduced feature, and show the expressive power of these ``constrained global types''.
}
}
@inproceedings{ABM-ICTCS12,
author = {Ancona, D. and Barbieri, M. and Mascardi, V.},
title = {Global {T}ypes for {D}ynamic {C}hecking of {P}rotocol
{C}onformance of {M}ulti-{A}gent {S}ystems ({E}xtended
{A}bstract)},
booktitle = {13th {I}talian {C}onference on {T}heoretical
{C}omputer {S}cience ({ICTCS} 2012)},
editor = {Massazza, P.},
pages = {39--43},
abstract = {In this paper we investigate the theoretical
foundations of global types for dynamic checking of
protocol compliance in multi-agents systems and we
extend the formalism by introducing a concatenation
operator that allows a significant enhancement of the
expressive power of global types. As examples, we show
how two non trivial protocols can be compactly
represented in the formalism: a ping-pong protocol, and
an alternating bit protocol, in the version proposed by
Deni\backslash{}'elou and Yoshida. Both protocols
cannot be specified easily (if at all) by other global
type frameworks, while in our approach they can be
expressed by two deterministic types (in a sense made
precise in the sequel) that can be effectively employed
for dynamic checking of the conformance to the
protocol.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ABM-ICTCS12.pdf},
keywords = {agents, behavioral-types,runtime-verification},
year = 2012
}
@inproceedings{ADM-DALT12,
author = {Ancona, D. and Drossopoulou, S. and Mascardi, V.},
title = {{Automatic Generation of Self-Monitoring MASs from
Multiparty Global Session Types in Jason}},
booktitle = {Declarative agent languages and technologies (DALT
2012).},
pages = {1--20},
publisher = {Springer},
abstract = {Global session types are behavioral types designed for
specifying in a compact way multiparty interactions
between distributed components, and verifying their
correctness. We take advantage of the fact that global
session types can be naturally represented as cyclic
Prolog terms - which are directly supported by the
Jason implementation of AgentSpeak - to allow simple
automatic generation of self-monitoring MASs: given a
global session type specifying an interaction protocol,
and the implementation of a MAS where agents are
expected to be compliant with it, we define a procedure
for automatically deriving a self-monitoring MAS. Such
a generated MAS ensures that agents conform to the
protocol at run-time, by adding a monitor agent that
checks that the ongoing conversation is correct w.r.t.
the global session type. The feasibility of the
approach has been experimented in Jason for a
non-trivial example involving recursive global session
types with alternative choice and fork type
constructors. Although the main aim of this work is the
development of a unit testing framework for MASs, the
proposed approach can be also extended to implement a
framework supporting self-recovering MASs.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ADM-DALT12.pdf},
keywords = {agents, behavioral-types, runtime-verification},
year = 2012
}
@inproceedings{BriolaMascardiAnconaIDC14,
author = {Briola, D. and
Mascardi, V. and
Ancona, D.},
title = {Distributed Runtime Verification of {JADE} Multiagent Systems},
booktitle = {Intelligent Distributed Computing {VIII} - Proceedings of the 8th
International Symposium on Intelligent Distributed Computing, {IDC}
2014, Madrid, Spain, September 3-5, 2014},
pages = {81--91},
year = {2014},
abstract = {{Verifying that agent interactions in a multiagent system (MAS) are compliant to a given global protocol is of paramount importance for most systems, and is mandatory for safety-critical applications. Runtime verification requires a proper formalism to express such a protocol, a possibly non intrusive mechanism for capturing agent interactions, and a method for verifying that captured interactions are compliant to the global protocol. Projecting the global protocol onto agents' subsets can improve efficiency and fault tolerance by allowing the distribution of the verification mechanism. Since many real MASs are based on JADE, a well known open source platform for MAS development, we implemented a monitor agent that achieves all the goals above using the "Attribute Global Types" (AGT) formalism for representing protocols. Using our JADE monitor we were able to verify FYPA, an extremely complex industrial MAS currently used by Ansaldo STS for allocating platforms and tracks to trains inside Italian stations, besides the Alternating Bit and the Iterated Contract Net protocols which are well known in the distributed systems and MAS communities. Depending on the monitored MAS, the performances of our monitor are either comparable or slightly worse than those of the JADE Sniffer because of the logging of the verification activities. Reducing the log files dimension, re-implementing the monitor in a way independent from the JADE Sniffer, and heavily exploiting projections are the three directions we are pursuing for improving the monitor's performances, still keeping all its features. }},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/IDC2014.pdf},
keywords = {runtime-verification, agents,behavioral-types}
}
@inproceedings{MascardiBriolaAnconaAIIA13,
author = {Mascardi, V. and
Briola, D. and
Ancona, D.},
title = {On the Expressiveness of Attribute Global Types: The Formalization
of a Real Multiagent System Protocol},
booktitle = {AI*IA 2013: Advances in Artificial Intelligence - XIIIth International
Conference of the Italian Association for Artificial Intelligence,
Turin, Italy, December 4-6, 2013. Proceedings},
pages = {300--311},
year = {2013},
abstract = {{Attribute global types are a formalism for specifying and dynamically verifying multi-party agents interaction protocols. They allow the multiagent system designer to easily express synchronization constraints among protocol branches and global constraints on sub-sequences of the allowed protocol traces. FYPA (Find Your Path, Agent!) is a multiagent system implemented in Jade currently being used by Ansaldo STS for allocating platforms and tracks to trains inside Italian stations. Since information on the station topology and on the current resource allocation is fully distributed, FYPA involves complex negotiation among agents to find a solution in quasi-real time. In this paper we describe the FYPA protocol using both AUML and attribute global types, showing that the second formalism is more concise than the first, besides being unambiguous and amenable for formal reasoning. Thanks to the Prolog implementation of the transition function defining the attribute global type semantic, we are able to generate a large number of protocol traces, and to manually inspect a subset of them to empirically validate that the protocol's formalization is correct. The integration of the Prolog verification mechanism into a Jade monitoring agent extending the Sniffer Agent is under way and will be used to verify the compliance of the actual conversation with the protocol. Keywords: multiagent systems, attribute global types, negotiation, dynamic verification of protocol compliance. }},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AIIA2013.pdf},
keywords = {runtime-verification, agents,behavioral-types}
}
@article{Betty16,
author = {Ancona, D. and
Bono, V. and
Bravetti, M. and
Campos, J. and
Castagna, G. and
Deni{\'{e}}lou, P.~M. and
Gay, S.~J. and
Gesbert, N. and
Giachino, E. and
Hu, R. and
Johnsen, E.~B. and
Martins, F. and
Mascardi, V. and
Montesi, F. and
Neykova, R. and
Ng, N. and
Padovani, L. and
Vasconcelos, V.T. and
Yoshida, N.},
title = {Behavioral Types in Programming Languages},
journal = {Foundations and Trends in Programming Languages},
volume = {3},
number = {2-3},
pages = {95--230},
year = {2016},
url = {http://dx.doi.org/10.1561/2500000031},
doi = {10.1561/2500000031},
keywords = {runtime-verification, agents,behavioral-types},
abstract = {{
A recent trend in programming language research is to use behavioral type theory to ensure various correctness properties of largescale, communication-intensive systems. Behavioral types encompass concepts such as interfaces, communication protocols, contracts, and choreography. The successful application of behavioral types requires a solid understanding of several practical aspects, from their representation in a concrete programming language, to their integration with other programming constructs such as methods and functions, to design and monitoring methodologies that take behaviors into account. This survey provides an overview of the state of the art of these aspects, which we summarize as the pragmatics of behavioral types.
}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/behavioralTypes.pdf}
}
@inproceedings{AnconaFerrandoMascardi17,
author = {Ancona, D. and
Ferrando, A. and
Mascardi, V.},
title = {Parametric Runtime Verification of Multiagent Systems},
booktitle = {Proceedings of the 16th Conference on Autonomous Agents and MultiAgent
Systems, {AAMAS} 2017, S{\~{a}}o Paulo, Brazil, May 8-12, 2017},
pages = {1457--1459},
year = {2017},
keywords = {runtime-verification, agents,behavioral-types},
abstract = {{
Parametricity is an important feature of a monitoring
system for making runtime verification (RV) more effective,
since, typically, correctness of traces depends on the specific
data values that are carried by the monitored events of the
trace, and that, in general, cannot be predicted statically.
Typically, the correctness of an interaction protocol may
depend on the values exchanged by agents; protocols may
also be parametric in the involved agents, and resources, and
this parametricity is naturally reflected on the data carried
by values.
In this work we propose parametric trace expressions, an
extension to trace expressions, expressly designed for
parametric RV of multiagent systems. Such an extension is
achieved by introducing variables in trace expressions that
are substituted with data values at runtime, when events are
matched during monitoring.
}},
http = {http://www.disi.unige.it/person/AnconaD/papers/AnconaFerrandoMascardiAAMAS17Parametric.pdf}
}
This file was generated by bibtex2html 1.98.