Verifying MSMAS model using S CIFF

Emad Eldeen Elakehal, M Montali, J Padget

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding


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 S CIFF Abductive Logic Programming-based framework. In particular, we show how the MSMAS constructs can be formalized in S CIFF, and then exploit this correspondence to specify and verify formal properties over MSMAS models, by leveraging on the S CIFF reasoning capabilities.
Original languageEnglish
Title of host publicationMultiagent System Technologies
Subtitle of host publication11th German Conference, MATES 2013, Koblenz, Germany, September 16-20, 2013. Proceedings
EditorsMatthias Klusch, Matthias Thimm, Marcin Paprzycki
Place of PublicationBerlin
Number of pages15
ISBN (Electronic)9783642407765
ISBN (Print)9783642407758
Publication statusPublished - 2013
Event11th German Conference on Multiagent System Technologies, MATES 2013 - Koblenz, Germany
Duration: 16 Sept 201320 Sept 2013

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Conference11th German Conference on Multiagent System Technologies, MATES 2013


Dive into the research topics of 'Verifying MSMAS model using S CIFF'. Together they form a unique fingerprint.

Cite this