Published: 12th May 2018
DOI: 10.4204/EPTCS.271
ISSN: 2075-2180

EPTCS 271

Proceedings Joint Workshop on
Handling IMPlicit and EXplicit knowledge in formal system development (IMPEX)
and
Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD)
Xi'An, China, 16th November 2017

Edited by: Régine Laleau, Dominique Méry, Shin Nakajima and Elena Troubitsyna

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

Preface

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.

First International Workshop on Handling IMPlicit and EXplicit knowledge in formal system development (IMPEX 2017)

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.

Second Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems (FM&MDD 2017)

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.

General comments

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.