TY - JOUR
T1 - Standard type soundness for agents and artifacts
AU - Damiani, Ferruccio
AU - Giannini, Paola
AU - Ricci, Alessandro
AU - Viroli, Mirko
PY - 2012
Y1 - 2012
N2 - Formal models, core calculi, and type systems, are important tools for rigorously stating the more subtle details of a language, as well as characterizing and studying its features and the correctness properties of its programs. In this paper we present FAAL (Featherweight Agent and Artifact Language), a formal calculus modelling the agent and artifact program abstractions provided by the simpA agent framework. The formalisation is largely inspired by Featherweight Java. It is based on reduction rules applied in certain evaluation contexts, properly adapted to the concurrency nature of simpA. On top of this calculus we introduce a standard type system and prove its soundness, so as to guarantee that the execution of a well-typed program does not get stuck. Namely, all primitive mechanisms of agents (activity execution), artifacts (field/property access and step execution), and their interaction (observation and invocation) are guaranteed to be used in a way that is structurally compliant with the corresponding definitions: hence, there will not be run-time errors due to FAAL distinctive primitives.
AB - Formal models, core calculi, and type systems, are important tools for rigorously stating the more subtle details of a language, as well as characterizing and studying its features and the correctness properties of its programs. In this paper we present FAAL (Featherweight Agent and Artifact Language), a formal calculus modelling the agent and artifact program abstractions provided by the simpA agent framework. The formalisation is largely inspired by Featherweight Java. It is based on reduction rules applied in certain evaluation contexts, properly adapted to the concurrency nature of simpA. On top of this calculus we introduce a standard type system and prove its soundness, so as to guarantee that the execution of a well-typed program does not get stuck. Namely, all primitive mechanisms of agents (activity execution), artifacts (field/property access and step execution), and their interaction (observation and invocation) are guaranteed to be used in a way that is structurally compliant with the corresponding definitions: hence, there will not be run-time errors due to FAAL distinctive primitives.
KW - Concurrency
KW - Multi-agent systems
KW - Type systems
UR - http://www.scopus.com/inward/record.url?scp=84870320100&partnerID=8YFLogxK
U2 - 10.7561/SACS.2012.2.267
DO - 10.7561/SACS.2012.2.267
M3 - Article
SN - 1843-8121
VL - 22
SP - 267
EP - 326
JO - Scientific Annals of Computer Science
JF - Scientific Annals of Computer Science
IS - 2
ER -