Run-time verification of MSMAS norms using event calculus

Emad Eldeen Elakehal, Marco Montali, Julian Padget

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

Abstract

Modelling Self-managing Multi Agent Systems (MSMAS) is a software development methodology that facilitates designing and developing complex distributed systems based on the multivalent systems paradigm. MSMAS uses a declarative modelling style to capture system requirements by specifying four types of what we call system norms over: the system goals, the system roles, the business activities, and communications. MSMAS utilises system norms to capture system requirements in a formal language which can subsequently be monitored and verified at runtime. In this paper we present the main elements of MSMAS and introduce MSMAS defined norm types. We model the life cycle of MSMAS norms as non-atomic activities and formally express them as Event Calculus (EC) theories. Our acclimatisation of MSMAS system norms as first-order EC allows for reasoning with a metric time representation which we illustrate through a monitoring example of two execution traces to verify the system compliance with its intended design requirements and show how to detect any violation of norms.

Original languageEnglish
Title of host publicationProceedings - 2014 IEEE 8th International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASOW 2014
PublisherIEEE
Pages110-115
Number of pages6
ISBN (Print)9781479963782
DOIs
Publication statusPublished - 2015
Event2014 8th IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASOW 2014 - London, UK United Kingdom
Duration: 8 Sep 201412 Sep 2014

Conference

Conference2014 8th IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, SASOW 2014
CountryUK United Kingdom
CityLondon
Period8/09/1412/09/14

Fingerprint Dive into the research topics of 'Run-time verification of MSMAS norms using event calculus'. Together they form a unique fingerprint.

Cite this