PhD in France
Offers listWhy France ?F.A.Q.Email AlertsPost an offer

Forgot Password ?
Offer Details

Model-based Development of Programmable Electronic Medical Systems
Université de Lorraine, Nancy
Computer Science and IT Systems 
Full Description:

 PhD Topics

While software reliability is essential for society, modern concurrent and distributed software is too complex to validate using traditional techniques such as code inspection and testing only. This PhD research will extend the domain of formal and tool-supported verification techniques for software development to ensure software reliability for concurrent and distributed software systems in the correct-by-construction [?] approach: A software system is a model of a real-world entity or process, which must accurately represent relevant properties from the domain of application, as well as addressing concerns such as robustness, correctness and performance. In software development it is common to model software at different levelsof abstraction. In formal software engineering we can map between these levels of abstraction in a verifiable way through a process known as refinement. This refinement typically happens within a single modelling language (e.g. Event B) and involves transforming an abstract formal model into a more concrete version, so that the resulting concrete version is can be proven to be consistent with the original, a refinement-based approach to program development would envisage a series of such steps from a very abstract design to an actual program [11]. One approach to refinement is the B method [1], which has been developed into the Event-B [2, 7] formalism, centred on the logic specification of state machines. This is supported by the Rodin tool [13], an Eclipse plug- in,which provides for the development of specifications at different levels of abstraction, and the construction [4] of proofs that each concrete layer is consistent with the preceding abstract layer. A number of projects1 have provided implementation frameworks for the ultimate refined concrete model and have resulted in the successful use of Event B in a number of industrial case studies including control systems [6, 12], communications protocols, distributed algorithms [3, 10] and digital circuits [8].

The development of Programmable Electronic Medical Systems (PEMS) is faced with several complex challenges. On the one hand, market forces demand for shorter time for deployment, reduced costs and higher return on investments. On the other hand, regulatory regimes explicitly demand such systems to be proven for stringent safety requirements before being operational. Such processes and development paradigms are therefore required which address these issues in effective and cost-efficient manners.

The current certification standards for PEMS either process-based such as IEC 62304 or product-based such as IEC 60601-1 give the freedom to implementers to alter the process and make software engineering choices that suit their particular needs. However, the problem associated with this freedom is that it often leads to an uncertainty about the appropriateness of software development measures because of lack of concrete technical advice on process and product qualities.

While applying for the approval of a product both manufacturers and certification regimes are affected with this situation. Manufacturers find it hard to argue about their processes in the quality management plan and about the dependability of the product in the associated safety cases. The certification authorities, on the other hand, need to evaluate the dependability of the product and the quality of the process that is not a straight forward task.

The use of rigorous methods and Model-Driven Development (MDD) paradigm can certainly provide assistance in this realm. The formal model of PEMS requirements amenable to verification (mathematical proofs, model-checking) and validation (animation, prototyping) can provide a basis for agreement of both concerned parties. Stringent safety cases associated with products can be modeled and proved in more convincing ways in this fashion. The seamless translation of the formal model into a machine-deployable code will provide an argument for the dependability of the process and the product.

The main aim of this work is to propose a process for modeling and analysis of elements of PEMS that contribute towards their automated translation into machine-deployable code. The translation process is based on transformations of Event-B models which are taking into acoount components of the target software-based system and which are preserving the relationship betwenn the requirements and the resulting system.


[1] Jean-Raymond Abrial. The B book - Assigning Programs to Meanings. Cambridge University Press, 1996.
[2] Jean-Raymond Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
[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]  Jean-Raymond Abrial and Stefan Hallerstede. Refinement, decomposition, and instantiation of discrete models: Application to event-b. Fundamenta Informaticae, 77(1-2):1–28, 2007.

[5]  Dines Bjørner and Martin C. Henson, editors. Logics of Specification Languages. EATCS Textbook in Computer Science. Springer, 2007.

[6]  Dominique Cansell, J. Paul Gibson, and Dominique M ́ery. Refinement: a constructive approach to formal software design for a secure e-voting interface. In Formal Methods for Interactive Systems (FMIS 2006), Macao, 2006.

[7]  Dominique Cansell and Dominique M ́ery. The event-B Modelling Method: Concepts and Case Studies, pages 33–140. Springer, 2007. See [5].

[8]  Dominique Cansell, Dominique M ́ery, and Cyril Proch. System-on-chip design by proof-based refinement. International Journal on Software Tools for Technology Transfer, 11(3):217–238, March 2009. The original publication is available at

[9]  Thai Son Hoang, Andreas Fu ̈rst, and Jean-Raymond Abrial. Event-b patterns and their tool support. Software and System Modeling, 12(2):229–244, 2013.

[10]  Thai Son Hoang, Hironobu Kuruma, David A. Basin, and Jean-Raymond Abrial. Developing topology discovery in event-b. pages 879–899, 2009.

[11]  Dominique M ́ery and Neeraj Kumar Singh. A generic framework: from modeling to code. ISSE, 7(4):227–235, 2011.

[12]  Dominique M ́ery and Neeraj Kumar Singh. Formal specification of medical systems by proof-based refinement. ACM Trans. Embedded Comput. Syst., 12(1)(15), 2013.

[13]  Project RODIN. The RODIN project: Rigorous open development environment for complex systems.

Application Form

Each applicant will file an application in a zip folder with all the items listed below, which constitutes an application. In addition, the original application will be mailed to the graduate school by post. The application must contain the following:

A detailed curriculum vitae which includes a description of the university curriculum and a description of professional experience and internships
Certificate of an eventual Masters degree or a testamur, whose equivalence should be validated by the graduate school in the case of foreign testamurs.
Copies of testamurs and diploma supplements, as well as grades and rankings from the candidate
Dissertations and/or internship reports and/or publications from the candidate
The PhD thesis topic with the name of the Supervisor (it is important that each candidate contact the Supervisor)
A reasoned opinion from the PhD Supervisor on the application which specifies the scientific context
A statement which outlines the PhD Supervisor’s current supervision and co-supervision projects
In the case that the candidate is supervised by a qualified Director and another person who is not qualified or is from outside the graduate school, a specific application for co-supervision must be provided with the submitted application, to be forwarded if appropriate to the Scientific Advisory Board for University enrolment.
Letters of recommendation from a scientist or numerous scientists – the individuals who supervised the Master’s thesis or internship, for example
Any item which demonstrates the candidate's value and ability to prepare a PhD



Posted on: 30 January 2015Deadline to apply: 01 April 2015Start Date: 01 May 2015 Duration: 36 months
The Fund category is Private Funding and the salary is 30-35k€ annual gross
Doctoral School is Informatics - Automatics - Electronics - Electrotechnics - Mathematics in Lorraine (IAEM-Lorraine) in the Lorraine Region.

Please connect to your account to see contact details

Back to offer list

Back to home page

PhD in France Website.
© French Embassy in India, CampusFrance 2014.

Contact us

Related Links