Wednesday , April 24 2024

Modelling a Multi-Agent System Relating to
Liveness Properties in Event-B

Lorina NEGREANU
University POLITEHNICA of Bucharest
313, Splaiul Independentei, Bucharest, 060042, Romania lorina.negreanu@cs.pub.ro

Abstract: Safety and liveness are properties of a formal model that ensure the correct and continuous progress of the model. The aim of this paper is to present a formal modelling and proof of correctness for a multi-agent system for requesting services, with respect to liveness properties – fairness and starvation freedom. The model is specified and verified using the Event-B formalism and the Rodin platform – an Eclipse plug-in meant to allow the writing and checking specification correctness. Event-B is a formal method based on first-order logic and set theory as an underlying mathematical notation used to model and reason about complex and discrete systems. One central mechanism of Event-B modelling is the concept of refinement that allows building a model in a step by step fashion, by adding more details to an initially abstract model, in order to reduce the level of abstraction, thus making it closer to reality. In our development we used refinement techniques, constructing an ordered sequence of embedded models, where each of them is a refinement of the one preceding it in the sequence.

Keywords: multi-agent systems, formal methods, Event-B, refinement, liveness, validation.

>>Full text
CITE THIS PAPER AS:
Lorina NEGREANU, Modelling a Multi-Agent System Relating to Liveness Properties in Event-B, Studies in Informatics and Control, ISSN 1220-1766, vol. 23 (4), pp. 351-358, 2014. https://doi.org/10.24846/v23i4y201405

  1. Introduction

We strongly believe that the rigorous development of complex systems should be based on mathematical models which can be analyzed by doing proofs. The obvious target is to reduce the number of design faults. The model of a system has a declarative semantics that allows us to prove that the defined properties of the system are consistent and will be present in it.

Multi-agent systems are complex, distributed, reactive systems that are quite difficult to specify formally. Event-B has been used to model multi-agent systems with a focus on concepts such as mobility and trust [5] or autonomy and interaction with a common environment [7]. Our aim is to model some other important properties of such systems.

This paper presents a formal modelling of liveness properties of a multi-agent system for requesting services, that will be integrated in an ambient intelligent system. The model is built using the Event-B [1], [3] formal specification method and machine checked using the Rodin tool [12], [13]. This should be read as an extension of the model we previously specified in [9] and [10]. The paper emphasises on the further refinements of the model (2nd and 3rd refinements) that enable us to check the liveness properties of the multi-agent system.

Safety and liveness are properties of a formal model that ensure the correct and continuous progress of the model at hand. While a safety property specifies that something bad will never happen [6] – “the system never reaches a bad state” – for example, some property holds throughout the execution (deadlock freedom, mutual exclusion), a liveness property specifies that something desirable will eventually happen [6] – “there is progress in the system” – some actions occur infinitely often. Our interest is in modelling liveness properties of a given system, more precisely, fairness and starvation freedom [4]. Fairness properties state that “if something is enabled sufficiently often, then it must eventually happen”.

We consider the typical fairness assumption (strong fairness) that enforces an event to be taken sufficiently often, but also the property that rather prevents a particular choice from being taken sufficiently often [14].

This becomes important in our model when the requests are satisfied. It is possible that a request cannot be satisfied for an indefinite period of time while other requests continue normally, which may occur if the satisfying scheme of the requests is unfair. On the other hand the availability time of a service may be insufficient and subsequently lead to starvation due to timeouts.

Liveness in an Event-B model is based on deadlock and live-lock freedom.

Since the Event-B language does not provide any facility to state liveness properties [8], we require liveness assumptions over some events to obtain a deadlock and live-lock-free model.

The paper is organized as follows: Section 2 describes the multi-agent system under scrutiny, Section 3 presents the Event-B specification of the initial model as well as further refinements which are done with respect to liveness properties. Section 4 contains the model validation. Section 5 lists the conclusions.

REFERENCES

  1. ABRIAL, J.-R., The B Book, Cambridge University Press, 1996.
  2. ABRIAL, J.-R., D., CANSELL, D. MERY, Refinement and Reachability in Event-B, Lecture Notes in Computer Science, 3455: Formal Specification and Development in Z and B, 2005, pp. 129-148.
  3. ABRIAL, J.-R., Modelling in Event-B: System and Software Engineering, Cambridge Press, 2010.
  4. BANDYOPADHYAY, A. K., Modelling Fairness and Starvation in Concurrent Systems, ACM SIGSOFT Software Engineering Notes, Volume 32, Number 6, November 2007.
  5. ILIASOV, A., L. LAIBINIS, A. ROMANOVSKY. E. TROIBITSYNA, Rigorous development of fault-tolerant agent systems, Technical Report 776, Turku Centre for Computer Science, 2006.
  6. LAMPORT, L., Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, Vol. 3, No. 2, 1977, pp. 125-143.
  7. LANOIX, A., Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles, 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2008), Jun 2008, France, 8 p.
  8. MERY, D., Requirements for a Temporal B Assigning Temporal Meaning to Abstract Machines … and to Abstract Systems, in A. Galloway and K. Taguchi, eds, IFM`99 Integrated Formal Methods 1999, YORK, 1999.
  9. MOCANU I., L. NEGREANU, A. M. FLOREA, Agents Modelling under Fairness Assumption in Event-B, IDC 2013, September 2013, Prague.
  10. NEGREANU, L., I. MOCANU, Formal Verification of Service Requests in a Multi-Agent System using Event-B Method, 8th Workshop on Workshop Knowledge Engineering and Software Engineering (KESE2012), ECAI 2012 Montpellier, France, Technical Report TR-2012/1, University of Almeria, Almeria, Spain, 2012, pp. 62-65.
  11. Pro-B – http://www.stups.uni-duesseldorf. de/ProB/index.php5/Main_Page.
  12. Rodin User`s Handbook v.2.5 – http://handbook.event-b.org/current/html/ index.html.
  13. Rodin Platform – http://wiki.event-b.org/index.php/Rodin_Platform.
  14. VOLZER, H., D. VARACCA, E. KINDLER, Defining Fairness, Proceedings CONCUR 2005 (16th Int. Conference on Concurrency Theory), LNCS 3653, Springer, 2005, pp. 458-472.
Designed by | ICI Bucharest
© Copyright 2024, All Rights Reserved