@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.