TY - GEN
T1 - Verifying MSMAS model using CIFF
AU - Elakehal, Emad Eldeen
AU - Montali, Marco
AU - Padget, Julian
PY - 2013/10/9
Y1 - 2013/10/9
N2 - MSMAS is a software development methodology that facilities the design and development of complex distributed systems based on the multiagent systems paradigm. MSMAS explicitly supports the institutional organisational structure and follows a declarative modelling style to specify behavioural restrictions on the members of the institution, their roles, the business processes regulating their behavior and the communication protocols regulating their mutual interactions. All these aspects are visually represented, by adapting the DECLARE graphical language, proposed for the declarative specification of constraint-based business processes. In this paper we discuss the main elements of MSMAS, and show how they can be equipped with a formal, expectation-based semantics, tailored to the CIFF Abductive Logic Programming-based framework. In particular, we show how the MSMAS constructs can be formalized in CIFF, and then exploit this correspondence to specify and verify formal properties over MSMAS models, by leveraging on the CIFF reasoning capabilities.
AB - MSMAS is a software development methodology that facilities the design and development of complex distributed systems based on the multiagent systems paradigm. MSMAS explicitly supports the institutional organisational structure and follows a declarative modelling style to specify behavioural restrictions on the members of the institution, their roles, the business processes regulating their behavior and the communication protocols regulating their mutual interactions. All these aspects are visually represented, by adapting the DECLARE graphical language, proposed for the declarative specification of constraint-based business processes. In this paper we discuss the main elements of MSMAS, and show how they can be equipped with a formal, expectation-based semantics, tailored to the CIFF Abductive Logic Programming-based framework. In particular, we show how the MSMAS constructs can be formalized in CIFF, and then exploit this correspondence to specify and verify formal properties over MSMAS models, by leveraging on the CIFF reasoning capabilities.
UR - http://www.scopus.com/inward/record.url?scp=84885007585&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-40776-5-7
DO - 10.1007/978-3-642-40776-5-7
M3 - Chapter in a published conference proceeding
AN - SCOPUS:84885007585
SN - 9783642407758
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 44
EP - 58
BT - Multiagent System Technologies - 11th German Conference, MATES 2013, Proceedings
T2 - 11th German Conference on Multiagent System Technologies, MATES 2013
Y2 - 16 September 2013 through 20 September 2013
ER -