PHD/Thèse Proposal Integration of a modelling language and a distributed programming language

Integration of a modelling language and a distributed programming language
PhD Proposal

 

Supervisors: Dominique Méry and Horatiu Cirstea LORIA UMR 7503, ́equipe MOSEL Requests: dominique.mery@loria.fr

in cooperation with Rosemary Mohanan
Principles of Programming
Dept of Computer Science, Maynooth University Rosemary.Monahan@mu.ie

 

 

Context

Distributed systems and more especially distributed algorithms, are considered to be as difficult to design as to verify. In recent work, we have studied problems related to distributed systems, to include the leader election problem [3, 12], the naming problem [6], the graph coloring problem and the self-stabilizing problem [9]. These studies all led us to a general framework of refinement, based on the incremental process for constructing abstract models corresponding to the current problem.

In previous work, two modeling techniques have been used, either in an exclusive way or in combination. These techniques are the Event-B [2] modelling language and the local computation model VISIDIA [24]. Notably the interaction between the COQ proof assistant [13, 11] and VISIDIA assists with proving the non-existence of solutions for a given problem. The integration of both modelling languages [26] is interesting since we gain the benefit of both environments. In addition, VISIDIA provides a way of visualising the resulting algorithms [24]. In VISIDIA a program is a set of rewriting rules applied to a finite graph representing the set of sites of the network. The main question is how to obtain a distributed executable model from an Event-B formal model. To achieve this, Event-B models must be localised through refinement. An event is local to a given node, whenever its behavior is controlled by the local variables. The challenge is to locate strategies for refinement that result in local events which can be translated into local processes; i.e. we wish to translate those local Event-B models into an executable distributed programming language in a simple way for users. Andriamiarina [4] developed such a methodology, based on the extension of Event-B scope by Mery and Poppleton [23].

From an historical point of view, approaches like UNITY [14] provide new perspectives for integrating formal methods in the design of concurrent and distributed programs. However, the main challege so far has been the provision of powerful and well designed support tools (such as provers and their interfaces). A further challenge is the provision of modelling languages that provide abstractions and expressive properties for distributed programs.

The quest is to develop a distributed programming language with high levels of abstrac- tion, with facilities for expressing communication between processes and with a rich assertion language capable of expressing critical properties of distributed systems. The quest is of im- mense interest to the community of distributed programmers, requiring usable environments which shield them from the intricacies of formal modelling.

The programming language DistAlgo[19] proposes an abstract notation for distributed algorithms while producing an implementation in C++ or Java. However, no framework for verification was proposed. Our integrated development framework[15] for implementing abstract Event B models brings together the strengths of the refinement based approaches and verification based approaches to software development. In particular, our framework supports:

  1. Splitting the abstract specification to be solved into its component specifications.
  2. Refining these specifications into a concrete model using Event B and the RODIN platform.
  3. Transforming the concrete model into algorithms that can be directly implemented as real source code using graph visualisation and applying code generation transforma- tions.
  4. Verifying the iterative algorithm in the automatic program verification environment of Spec#.

The environment implements a methodology developed by Mery[22] by EB2RC (Tool for Translating Event-B models to Recursive Code). In the case of EB2RC, we have used target programming languages like C, C++ and C#. We now aim to expand these languages to include MPI[1] and DistAlgo[19], where programns are generated from Event-B models that are local abstract models of a given distributed problem.

Description of project

After having detailed the context of the PhD, we list the main stages of the research pro- gramme.

A first stage is to get expertise in using the modelling language Event-B together with the associated Rodin toolset. It is also the time for studying DistAlgo and its programming environment. This stage will develop classical and original case studies to showcase the modelling and programming languages. The central focus will be the clear identification of local models and the transformation rules required to produce distributed executable code in MPI or DistAlgo. The PhD student will move from the status of user to the status of expert in Event-B and distributed programming and he or she will become an expert user of tools related to the topics.

In the second stage of this research programme, the objective is to confirm the patterns and transformations discovered in stage 1. The list of transformations will be proved correct and the semantics of the different objects will be researched. A difficult phase will be the comparison of the operational semantics of Event-B and DistAlgo. In this work the semantics of Event-B and modularisation techniques provided by Farrell[16, 18, 17] will be the key.

Finally, the production of a plugin for the Rodin platform will complete the PhD and the previous case studies will be used for validating the plugin and the translation itself.

The research builds upon previous PhD dissertations [16, 25, 10, 4], on methodological guidelines [20, 21] for sequential algorithms and on the products of the RIMEL project [6, 7, 8, 9, 5].

Required Skills and Knowledge

The candidate should have or be about to obtain a masters degree in computer science. The technical skills and/or interests should include:

• Programming languages and models of computation.
• Formal methods (semantics, verification, static analysis, …). • Distributed algorithms.
• Experience in using a proof assistant.

References

  1. [1]  Using MPI: Portable Parallel Programming with the Message-Passing Interface (Scientific and Engineering Computation). MIT, 2014.
  2. [2]  Jean-Raymond Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
  3. [3]  Jean-Raymond Abrial, Dominique Cansell, and Dominique M ́ery. A mechanically proved and incremental development of IEEE 1394 tree identify protocol. Formal Asp. Comput., 14(3):215–227, 2003.
  4. [4]  Manamiary Bruno Andriamiarina. D ́eveloppement d’algorithmes r ́epartis corrects par con- struction. Th`ese, Universit ́e de Lorraine ; Loria & Inria Grand Est, October 2015.
  5. [5]  Projet ANR-RIMEL. Probabilistic incremental proof-based development. Technical report.

    [6] Projet ANR-RIMEL. D ́eveloppement d’algorithmes r ́epartis. Livrable rimel, LORIA, Jan- vier/F ́evrier 2008.

    [7]ProjetANR-RIMEL. Int ́egrationdutempsdansled ́eveloppementincr ́ementalprouv ́e. Livrable rimel, LORIA, Juillet 2008.

    1. [8]  Projet ANR-RIMEL. Proof-based design patterns. Livrable rimel, LORIA, Juillet 2008.
    2. [9]  Projet ANR-RIMEL. Formal system engineering. Livrable rimel, LORIA, Juillet 2009.
    3. [10]  Nazim Benaissa. PhD thesis, Universit ́e Henri poincar ́e Nancy 1, Mai 2010.
    4. [11]  Yves Bertot and Pierre Cast ́eran. Interactive Theorem Proving and Program Development – Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004.
    5. [12]  Dominique Cansell and Dominique M ́ery. Formal and incremental construction of distributed algorithms: On the distributed reference counting algorithm. Theor. Comput. Sci., 364(3):318– 337, 2006.
    6. [13]  Pierre Cast ́eran and Vincent Filou. Tasks, types and tactics for local computation systems. Stud. Inform. Univ., 9(1):39–86, 2011.
    7. [14]  K. M. Chandy and J. Misra. Parallel Program Design A Foundation. Addison-Wesley Pub- lishing Company, 1988. ISBN 0-201-05866-9.
    8. [15]  Zheng Cheng, Dominique M ́ery, and Rosemary Monahan. On two friends for getting correct programs – automatically translating event B specifications to recursive algorithms in rodin. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques – 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I, volume 9952 of Lecture Notes in Computer Science, pages 821–838, 2016.
    9. [16]  Marie Farrell. Event-B in the Institutional Framework: Defining a Semantics, Modularisa- tion Constructs and Interoperability for a Specification Language. PhD thesis, Department of Computer Science, Maynooth University, Ireland, 2017.
    10. [17]  Marie Farrell, Rosemary Monahan, and James F. Power. A logical framework for integrating software models via refinement. In British Colloquium for Theoretical Computer Science, BCTCS, 2016.
    11. [18]  Marie Farrell, Rosemary Monahan, and James F. Power. Providing a semantics and modulari- sation constructs for Event-B using institutions. In 23rd International Workshop on Algebraic Development Techniques, WADT, 2016.
    12. [19]  Yanhong A. Liu, Scott D. Stoller, and Bo Lin. From clarity to efficiency for distributed algorithms. ACM Trans. Program. Lang. Syst., 39(3):12:1–12:41, 2017.
    13. [20]  Dominique M ́ery. Refinement-based guidelines for algorithmic systems. International Journal of Software and Informatics, 3(2-3):197–239, June/September 2009.4
    1. [21]  Dominique M ́ery. A simple refinement-based method for constructing algorithms. ACM SIGCSE Bulletin, 41(2):51–59, 2009-06.
    2. [22]  Dominique M ́ery. Refinement-based guidelines for algorithmic systems. International Journal of Software and Informatics, 3(2-3):197–239, 2009-09.
    3. [23]  Dominique M ́ery and Mike Poppleton. Towards An Integrated Formal Method for Verification of Liveness Properties in Distributed Systems. Software and Systems Modeling (SoSyM), December 2015.
    4. [24]  Mohammed Mosbah. Visidia. http://visidia.labri.fr, 2009.
    5. [25]  Joris Rehm. Gestion du temps par le raffinement. PhD thesis, Universit ́e Henri poincar ́e Nancy 1, Decembre 2009.
    6. [26]  M. Tounsi, A. Hadj Kacem, M. Mosbah, and D.M ́ery. A refinement approach for proving distributed algorithms:examples of spanning tree problems. In Workshop on Integration of Model-based Formal Methods and Tools, 2009. 16-19 February, Germany.

Logo du CNRS

Logo d'Inria

Logo Université de Lorraine