13 Feb 2025
Job Information
- Organisation/Company
IMT - Institut Mines-Télécom- Department
INF- Research Field
Computer science » Informatics- Researcher Profile
First Stage Researcher (R1)- Positions
PhD Positions- Country
France- Application Deadline
12 Mar 2025 - 08:00 (Europe/Paris)- Type of Contract
Temporary- Job Status
Full-time- Hours Per Week
37, 40- Offer Starting Date
13 Feb 2025- Is the job funded through the EU Research Framework Programme?
Other EU programme- Reference Number
PhD student - Extending the Event-B Method to Support Modul- Is the Job related to staff position within a Research Infrastructure?
No
Offer Description
ABOUT TELECOM SUDPARIS
Telecom SudParis is a public graduate school for engineering, which has been recognized on the highest level in the domain of digital technology. The quality of its courses is founded on the scientific excellence of its faculty and on teaching techniques that emphasize project management, innovation and intercultural understanding. Telecom SudParis is part of the Institut Mines-Telecom, the number one group of engineering schools in France, under the supervision of the Minister for Industry. Telecom SudParis with Ecole Polytechnique, ENSTA Paris, ENSAE Paris, ENPC and Telecom Paris are co-founders of the Institut Polytechnique de Paris, an institute of Science and Technology with an international vocation.
Its assets include: a personalized course, varied opportunities, the no.3 incubator in France, an ICT research center, an international campus shared with Institut Mines-Telecom Business School and over 60 student societies and clubs.
The formal Event-B method [1] is a mathematical concepts-based approach to build correct-by-design discrete systems. It is supported by the RODIN platform that offers the possibility for plunging provers and model-checkers that help developers verify and validate their developments. The Event-B method has been experienced on several case studies that demonstrate that the refinement, the cornerstone of the method, is very suitable design technique to master the complexity of the underlying systems. However, the resulted development is specification is very large and arduous to comprehend since it is quite monolithic: a single top abstract machine that models the main functionality of the system and a set of successive refinements that aim at incrementally introducing the other functionalities.. This lack of modularization makes the Event-B method unscalable for development of industrial systems. Our project aims to provide an intuitive and user-friendly compositional approach that enables users to build models effectively and systematically. There are some works that have addressed the definition of modules that can be re-used and composed to build specifications that are more complex. In [2], the authors defined a set of generic Event-B components and formal instantiation rules to produce particular ones for developing specific applications. This approach has been defined for both machine and refinement components. In [4, 5], two decomposition approaches are defined to split an Event-B specification into several components sharing either variables or events. The approach most closely aligned with our objective is the interface-based composition approach introduced in [3] for modeling complex systems by decomposing them into several modules that can be independently built.
The main drawback of this approach is that it is very programming oriented since it has been defined in a very particular industrial application. Our aim is to develop more abstract structuration mechanisms for building a system as a combination of a set of Event- B components each of them modeling a specific functionality of the global system. We plan to study particularly the possibility for a machine to merge/refine several machines/events. The contributions of this thesis are as follows: (1) a set of machine constructs to link Event-B machines/refinements, (2) the proof obligations that ensure the correctness of the global system and property preservation, (3) a Rodin plugin that makes the approach workable and its validation on industrial case study. Having such an approach would foster the use of the formal Event-B model in developing secure real-size industrial/critical systems.
Where to apply
- Website
- https://institutminestelecom.recruitee.com/o/doctorat-entre-methode-eventb-inte…
Requirements
- Research Field
- Computer science » Informatics
- Education Level
- Master Degree or equivalent
Skills/Qualifications
Education
- 5 years' higher education/Master degree or equivalent
Skills and aptitudes
- Rigor, project management methods
- Good interpersonal skills with people at all levels, ability to listen and cooperate
- Ability to work as part of a team
- Strict compliance with confidentiality obligations with regard to data used
- Languages
- ENGLISH
- Level
- Basic
- Research Field
- Computer science » Informatics
- Years of Research Experience
- None
Additional Information
Benefits
Further information and application
- Application deadline: March 12, 2025
- Type of contract: 3-year PhD contract
- Job location: Evry-Courcouronnes (91)
- Positions are open to all, with special arrangements for disabled candidates on request.
Working conditions: Telecommuting possible, on-site restaurant and cafeteria, accessibility by public transport (with employer's contribution) or close to main roads, staff association and sports association on campus.
TO APPLY:
Please send :
- a motivation letter
- a resume
- a work notice about our past and future student activitie
- Website for additional job details
https://institutminestelecom.recruitee.com/o/doctorat-entre-methode-eventb-inte…
Work Location(s)
- Number of offers available
- 1
- Company/Institute
- Telecom SudParis
- Country
- France
- State/Province
- Ile-de-France
- City
- Evry-Courcouronnes
- Postal Code
- 91011
- Street
- 9 rue Charles Fourier
- Geofield
Contact
- State/Province
ILE-DE-FRANCE- City
Evry-Courcouronnes- Website
https://institutminestelecom.recruitee.com/o/doctorat-entre-methode-eventb-integrer-modularisatoon- Street
9 rue Charles Charles Fourier- Postal Code
91000
recrutements@imtbs-tsp.eu
STATUS: EXPIRED
- X (formerly Twitter)
More share options- Viadeo
- Gmail
- Blogger
- Qzone
- YahooMail
Similar Positions
-
Ph D: Surface Acoustic Waves For Novel Magnetism Based Devices, European Magnetism Association EMA, France, 23 days ago
Description of the offer : Magnetism intervenes in the data storage components, with information coded by the magnetization direction of submicronic magnetic domains. The calculations are instead ...