Verifying MSMAS model using S CIFF

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.