Verifying MSMAS model using S CIFF

Emad Eldeen Elakehal, M Montali, J Padget

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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
PublisherSpringer
Pages44-58
Number of pages15
ISBN (Electronic)9783642407765
ISBN (Print)9783642407758
DOIs
Publication statusPublished - 2013
Event11th German Conference on Multiagent System Technologies, MATES 2013 - Koblenz, Germany
Duration: 16 Sep 201320 Sep 2013

Publication series

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

Conference

Conference11th German Conference on Multiagent System Technologies, MATES 2013
CountryGermany
CityKoblenz
Period16/09/1320/09/13

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

Cite this