The development of complex systems usually requires multi-view modelling when the systems involve different scientific disciplines and skills [1]. For instance, in the case of autonomous systems, modelling behaviours and interactions of different systems may require control theory concepts, communication protocols, resource allocation, access control rules, time constraints, etc.

However, handling critical complex models related to different engineering domain areas involves modelling concepts that are not explicitly available nor supported by a single formal method. Examples of such domain-specific concepts are reals and continuous functions, classes, and more generally new types with associated operators and properties. Their formal definitions require to start from the core concepts of formal methods i.e. from discrete maths, set theory, category theory, logic and basic arithmetic. This modelling chain could be possible with most of the existing formal methods but it is cumbersome and makes the proof difficult to carry, because of all the details of the encoding of domain-specific concepts in their underlying theory. Moreover, the explicit semantics of these domain-specific concepts are lost by this modelling [2], which makes their reuse not directly possible.

A solution for specifying domain theories consists in using extension mechanisms available in most of existing formal methods. We can cite for instance contexts or theories or species like in Event- B [3], COQ[4], Isabel/HOL[5], Dedukti[6], Nuprl[7], ASM[8], etc. Thus defining a domain theory may consist in specifying data types and their properties, operators to manipulate them with welldefinedness conditions that ensure their correct use, axioms and proved theorems. Consequently, in a system to be developed, the domain theory is used to type specific concepts that can be manipulated only by its operators, provided that the well-definedness conditions are satisfied. Theorems defined in the domain theory can be reused in proofs related to the system to be developed. Domain theories offer a more faithful and encapsulated representation of domain concepts, streamlining the reuse of these concepts when building system models, and facilitating their specification, validation and understanding.

The objective of the meeting is to discuss the state of the art advances in the definition of domain theories in formal methods. It builds on the results obtained since the 2016 Shonan Meeting 90 on “Implicit and explicit semantics integration in proof based developments of discrete systems” 1. We want to evaluate the main achievements and identify outstanding challenges. Indeed, although the approaches discussed in Meeting 90 made notable impacts, some limitations are identified. The previous approaches supported modeling by the means of ontology or annotations, thus focusing on understanding and description. They did not support domain-specific verification such as proof reuse and recurring proof patterns. This is critical since there is an increasing demand for dependability of cyber-physical systems, which requires complex verification over continuous systems. We now need a better understanding of how to formalise domain knowledge in order to efficiently exploit it in comprehensive verification mechanisms.

Contributions to the meeting shall address one or more topics described below.

• Experiments on using extension mechanisms of formal methods to define domain theories.
• Experiments on using domain theories, defined using extension mechanisms, in the formal development of complex models. Note that formal development not only includes system specification but also verification of system properties. Among others, case studies showing the reuse of domain theories in the development of various complex systems, the feasibility of multi-view modelling in a single formal framework, etc.
• How to handle the semantic heterogeneity that can occur if different domain theories have to be integrated to develop a complex system? In particular, domain knowledge can be twofold: domain knowledge related to scientific data types, like differential equations and time representation, and domain knowledge related to application domains of systems under design, for example imperial or metric units, railway protocols or International Civil Aviation Organization regulations. It may happen that theories related to scientific domain knowledge are formalized in a logic different from the one used in theories related to application domain knowledge. How can these different semantics be aligned?
• How to ensure that the extension mechanism used to import specific domain theories is sound?
• How to handle domain theory validation?
• How to address proof certification issues as heterogeneous proofs may appear due to the use of different proof systems adapted to specific theories?

 

The meeting will have two types of sessions. The first type of sessions will have short presentations where each participant will introduce their research work, and list some ideas/challenges/research directions that they would like to discuss during the meeting. Such presentations will be scheduled during the first two days of the meeting. The second type of sessions will consist in intensive discussions among sub-groups of participants. The topics of the discussions will be decided at the meeting among those proposed by participants, but candidates include opportunities for domain theories to emerging applications such as digital twins or AI-based systems, gaps between the present research

and industry applications, etc. The current plan is to use a variation of the world cafe method 2: this will allow participants to move across the different sub-groups and so get to know the different initial topics. Finally, we will sort out a research agenda for formal method extensions to support domain theories, including a planning of book.

[1] D. Bjørner. Manifest domains: analysis and description. Formal Asp. Comput., 29(2):175–225, 2017.

[2] Y. Ait-Ameur and D. Méry. Making explicit domain knowledge in formal system development. Sci. Comput. Program., 121:100–127, 2016.

[3] M. J. Butler and I. Maamria. Practical theory extension in Event-B. In Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, pp. 67–81, 2013.

[4] Y. Bertot and P. Castéran. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer Science & Business Media, 2013.

[5] T. Nipkow et al. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. http://isabelle.in.tum.de/.

[6] A. Assaf et al. Expressing theories in the ΛΠ-calculus modulo theory and in the Dedukti system. In TYPES: Types for Proofs and Programs, Novi SAd, Serbia, May 2016.

[7] R. L. Constable et al. Implementing mathematics with the Nuprl proof development system. Prentice Hall, 1986.

[8] E. Börger and R. F. Stärk. Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, 2003.