The idea of the meeting arose from two observations, concerned with the nature of proof-based systems and the way in which they are used by formal methods applied to the development of software.

Firstly, most proof based systems [9] are based on the definition and use of theories (logic, algebraic, types, etc.) in order to support the expression of proofs in formal developments that can become highly complex. In general, these proof systems are based on theories composed of axioms and an inference system. The formal developments conducted in such systems contribute to the definition of new theories or to the enrichment (extension) of existing ones through new deduced theorems using automatic and/or semi-automatic proof procedures.

In practice, these approaches are used in two situations: 1) for defining new theories that can be themselves extended or enriched, 2) for the formal development of hardware and/or software systems. In this second case, a developed system is abstracted by a model formalised in the used theory and the required properties of this model are expressed and checked in the same theory using its inference rules. The meeting addresses this second situation.

The approaches supporting such formal development offer a basic theory and propose mechanisms and operators making it possible to define new theories (inside contexts, or theories or species, like in Event-B [1], COQ[2], Isabelle/HOL[10], FOCAL[5], Nuprl[4], ASM [3], etc.) and to enrich these theories. The formal modelling of hardware and/or software systems is realised in these approaches.

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. The semantics of such formalised systems is expressed in this theory; i.e. the used theory gives the semantics of the formalized systems and the semantics of all the systems formalised in this theory. In the context of this approach, this kind of semantics represents the implicit semantics. The same semantics is used for a wide variety of heterogeneous systems. However, in several situations, the developed hardware and/or software systems are associated to other information issued from the application domain in which these systems 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. 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 same semantics is, again, used for a wide variety of heterogeneous systems.

In the last decade, knowledge models, named ontologies [7][8], have been set up to facilitate the software designer to make explicit this kind of knowledge. According to Gruber, an ontology is a specification of a conceptualisation. Ontologies are formal models describing the meaning (semantics) of concepts of a domain independently of the considered conceptual models which prescribe the design of these models. The possibility to associate this kind of knowledge to the concepts manipulated by the formal models defining or prescribing the hardware and/or software systems facilitates the formal specification of new properties and concepts — such as adaptability, re-configurability, identification of degraded modes, interoperability, etc. —for heterogeneous systems [6].

Another observation is related to the way in which a hardware and/or software system is developed using formal methods and how the proofs associated with these developments are conducted. 6/13 Such systems are usually designed by decomposing into/composing subsystems in a top/down, bottom/ up and mixed process. The refinement/abstraction and instantiation development operations are applied during these processes.

The objective of the meeting is to discuss on mechanisms for reducing model heterogeneity 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 the state in handling both implicit and explicit semantics in formal system developments. Discussions, presentations and more generally, contribution shall address one or more topics described below

• Show that when making explicit the domain knowledge in formal models, several relevant hidden (because they are not explicitly modeled in classical formal modelling languages) properties can be handled
• How knowledge models, like ontologies, can be handled in formal system developments ?
• What are the candidate formal modelling languages and techniques to model such domain knowledge ? What are the reasoning capabilities entailed by these modelling languages ?
• Define relevant case studies that illustrate the need to make explicit the domain properties ?
• Define composition mechanisms to handle domain knowledge in formal modelling techniques.

Beyond the technical results targeted by the proposed Shonan meeting, social, economic and resilience impacts are expected. These impacts are built on the foundations of heterogeneity reduction and formal model alignment. Finally, we mention that once this meeting is completed, it is planned to publish a book gathering the main contributions and results.

[1] Jean-Raymond Abrial. Modeling in Event-B – System and Software Engineering. Cambridge University Press, 2010.
[2] Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. springer, 2004.
[3] Egon Börger and Robert F. Stärk. Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, 2003.
[4] R L Constable. Implementing mathematics with the Nuprl proof development system. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1986.
[5] Catherine Dubois, Thérese Hardin, and V Donzeau-Gouge. Building certified components within focal. Trends in Functional Programming, 5:33–48, 2006.
[6] Alexander Egyed and Nenad Medvidovic. A formal approach to heterogeneous software modeling. Fundamental Approaches to Software Engineering, pages 178–192, 2000.
[7] Thomas R.Gruber. A translation approach to portable ontology specifications. Knowl. Acquis., 5(2):199–220, June 1993.
[8] Stéphane Jean, Guy Pierra, and Yamine Aït-Ameur. Domain ontologies: A database-oriented analysis. In José A. Moinhos Cordeiro, Vitor Pedrosa, Bruno Encarnação, and Joaquim Filipe, editors, WEBIST (1), pages 341–351. INSTICC Press, 2006.
[9] Gérard Le Lann. Proof-based system engineering and embedded systems. Lectures on Embedded Systems, pages 208–248, 1998.
[10] Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. Isabelle/HOL: a proof assistant for higher-order logic, volume 2283. Springer, 2002.