Dominique Méry

J Paul Gibson, Dominique Méry

The increasing development of cyber-physical systems (CPSs) requires modellers to represent and reason about physical values. This paper addresses two major, inter-related, aspects that arise when modelling physical measures. Firstly, there is often a heterogeneity of representation; for example: speed can be represented in many different units (mph, kph, mps, etc. . . ). Secondly, there is incoherence in composition; for example: adding a speed to a temperature would provide a meaningless result in the physical world, even though such a purely mathematical operation is meaningful in the abstract. These aspects are problematic when implicit semantics - concerned with measurements - in CPSs are not explicit (enough) in the requirements, design and implementation models. We present an engineering approach for explicitly modelling measurements during all phases of formal system development. We illustrate this by moving from Event-B models to Java implementations, via object oriented design.

Régine Laleau, Dominique Méry, Shin Nakajima et al.

This volume contains the joint proceedings of IMPEX 2017, the first workshop on Handling IMPlicit and EXplicit knowledge in formal system development and FM&MDD, the second workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD) held together on November 16, 2017 in Xi'an, China, as part of ICFEM 2017, 19th International Conference on Formal Engineering Methods. IMPEX emphasises mechanisms for reducing heterogeneity of models induced by the absence of explicit semantics expression in the formal techniques used to specify these models. More precisely, the meeting targets to highlight the advances in handling both implicit and explicit semantics in formal system developments. The aims of FM&MDD are to advance the understanding in the area of developing and applying formal and model-driven techniques for designing trustworthy systems, to discuss the emerging issues in the area, to improve the dialog between different research communities and between academia and industry, to discuss a roadmap of the future research in the area and to create a forum for discussing and disseminating the new ideas and the research results in the area

Catherine Dubois, Paolo Masci, Dominique Méry

This volume contains the proceedings of F-IDE 2016, the third international workshop on Formal Integrated Development Environment, which was held as an FM 2016 satellite event, on November 8, 2016, in Limassol (Cyprus). High levels of safety, security and also privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application in order to ease the justification of design choices and the review of code and proofs. Thus tools are needed for handling specifications, program constructs and verification artifacts. The aim of the F-IDE workshop is to provide a forum for presenting and discussing research efforts as well as experience returns on design, development and usage of formal IDE aiming at making formal methods "easier" for both specialists and non-specialists.

Dominique Méry, Neeraj Kumar Singh

The failure of hardware or software in a critical system can lead to loss of lives. The design errors can be main source of the failures that can be introduced during system development process. Formal techniques are an alternative approach to verify the correctness of critical systems, overcoming limitations of the traditional validation techniques such as simulation and testing. The increasing complexity and failure rate brings new challenges in the area of verification and validation of avionic systems. Since the reliability of the software cannot be quantified, the \textit{correct by construction} approach can implement a reliable system. Refinement plays a major role to build a large system incrementally from an abstract specification to a concrete system. This paper contributes as a stepwise formal development of the landing system of an aircraft. The formal models include the complex behaviour, temporal behaviour and sequence of operations of the landing gear system. The models are formalized in Event-B modelling language, which supports stepwise refinement. This case study is considered as a benchmark for techniques and tools dedicated to the verification of behavioural properties of systems. The report is the full version of a paper published for the ABZ 2014 Case Study. is

Catherine Dubois, Dimitra Giannakopoulou, Dominique Méry

This volume contains the proceedings of F-IDE 2014, the first international workshop on Formal Integrated Development Environment, which was held as an ETAPS 2014 satellite event, on April 6, 2014, in Grenoble (France). High levels of safety, security and also privacy standards require the use of formal methods to specify and develop compliant software (sub)systems. Any standard comes with an assessment process, which requires a complete documentation of the application in order to ease the justification of design choices and the review of code and proofs. Thus tools are needed for handling specifications, program constructs and verification artifacts. The aim of the F-IDE workshop is to provide a forum for presenting and discussing research efforts as well as experience returns on design, development and usage of formal IDE aiming at making formal methods "easier" for both specialists and non-specialists.