Published: 12th May 2018|
|Preface Régine Laleau, Dominique Méry, Shin Nakajima and Elena Troubitsyna|
|Domain Analysis & Description - The Implicit and Explicit Semantics Problem Dines Bjørner||1|
|Formal Modelling of Ontologies : An Event-B based Approach Using the Rodin Platform Yamine Ait Ameur, Idir Ait Sadoune, Kahina Hacid and Linda Mohand Oussaid||24|
|Incremental Database Design using UML-B and Event-B Ahmed Al-Brashdi, Michael Butler and Abdolbaghi Rezazadeh||34|
|Parameterized Model Checking Modulo Explicit Weak Memory Models Sylvain Conchon, David Declerck and Fatiha Zaïdi||48|
|Explicit Modelling of Physical Measures: From Event-B to Java J Paul Gibson and Dominique Méry||64|
|Securing Open Source Clouds Using Models Irum Rauf and Elena Troubitsyna||80|
|A Formal Model to Facilitate Security Testing in Modern Automotive Systems Eduardo dos Santos, Andrew Simpson and Dominik Schoop||95|
|Towards Integrated Modelling of Dynamic Access Control with UML and Event-B Inna Vistbakka and Elena Troubitsyna||105|
IMPEX 2017 and FM&MDD 2017 are two workshops held in Xi'An, China, on November 16, 2017. The organisers have decided to have a joint proceedings for the two events.
Most of methods based on proof systems, such as theorem provers, model checkers or any reasoning systems, rely on the definition and use of basic theories (logic, algebraic, types, etc.) in order to support the expression of proofs in formal developments. They also propose mechanisms and operators to define new theories (inside contexts or theories or species, like in Event-B, COQ, Isabelle/HOL, FOCALIZE, Nuprl, ASM, PVS, etc.) or to enrich their basic theories. In general, the definition of a theory is based on mathematical and logical abstract concepts that support the formalisation of the studied hardware and/or software systems. In other words, the semantics of such formalised systems is expressed in this theory; i.e. the used theory gives the semantics of all the systems formalised in this theory and the required properties of these systems are expressed and checked in the same theory. This kind of semantics represents the implicit semantics. Note that the same semantics is used for a wide variety of heterogeneous hardware and/or software systems.
Generally, hardware and/or software systems are associated to information issued from the application domain in which they evolve. For example, one integer variable (typed by an integer in the theory) may denote a temperature expressed in Celsius degrees, whilst another one may denote a pressure measured in bars at the extreme limit of the left wing of an aircraft in the landing phase. In general, this kind of knowledge is omitted by the produced formalisations or their formalisation is hardcoded in the designed formal model. If this knowledge carried by the concepts manipulated in these formal models is still in the mind of the model designer, it is not explicitly formalised and therefore, it is not shared in the same way as for implicit theories that can be reused in several formal developments. This kind of knowledge represents the explicit semantics.
The objective of the meeting was to discuss on 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.
We sollicited several kinds of contributions: research papers providing new concepts and results, position papers and research perspectives, experience reports, tool presentations. The current edition is a one-day workshop with four communications. Each submission was pre and post reviewed by three reviewers.
We had the honor to welcome Professor Dines Bjorner, Prof. Emeritus, from DTU Compute, Dept. of Mathematics and Computer Science, Techn.Univ.of Denmark, Denmark. He gave a keynote entitled The Manifest Domain Analysis and Description Approach to Implicit and Explicit Semantics and his slides are available at http://www.imm.dtu.dk/~dibj/2017/summer/impex.pdf.
Development of trustworthy software-intensive systems constitutes one of the major engineering challenges. Both functional correctness and extra-functional properties such as safety, reliability and security are equally important for ensuring system trustworthiness. To efficiently cope with complexity caused by inherently heterogeneous development environment, the designers often rely of model-driven techniques that provide them with a comprehensive integrated notation. Indeed, graphical models help to bridge the gap between informal requirements and formal models, while various architectural modelling frameworks enable the efficient multi-view analysis of diverse system properties.
Though the benefits of using both formal and model-driven techniques in the design of trustworthy systems are widely acknowledged, there is still a lack of common understanding of the integration mechanisms. In particular, there are ongoing debates about achieving a balance between flexibility and rigor in integrated modelling, analyzing the interplay between functional and extra-functional properties, using domain-specific frameworks as well as addressing trustworthiness at different architectural levels.
Moreover, the development of systems is becoming more and more incremental and practices like continuous integration and deployment are the ambition of many companies including those working with safety-critical systems. This implies that formal and model-driven techniques should support incremental verification thus enabling the continuous addition of new features while ensuring system trustworthiness.
The aims of this workshop were:
The current edition is a one-day workshop with four communications. Each submission was pre and post reviewed by three reviewers.
We would like to thank the PC members for doing such a great job in writing high-quality reviews and participating in the electronic PC discussion. The joint meeting was a time for strong scientific exchanges on topics of both workshop and has led to an interesting programme. We would like to thank all authors who submitted their work to IMPEX 2017 and FM&MDD 2017. We are grateful to the ICFEM Organisation Committee, which has accepted to host our workshop. The logistics of our job as Program Chairs were facilitated by the EasyChair system and we thank the editors of Electronic Proceedings in Theoretical Computer Science who accepted to publish the papers.