Co-located with ICFEM 2017 (19th International Conference on Formal Engineering Methods) in Xi’an, China, 13-17th November 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, FOCAL, 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 is 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.
Topic Areas
Discussions, presentations and more generally, contributions 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 modelled 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 domain properties?
- Define composition mechanisms to handle domain knowledge in formal modelling techniques.
Beyond the technical results targeted by the proposed meeting, social, economic and resilience impacts are expected. These impacts are built on the foundations of heterogeneity reduction and formal model alignment.
