IMPEX 2017: First International Workshop on Handling IMPlicit and EXplicit knowledge in formal system development Xidian University Xi’an, China, November 13-17, 2017 |
Conference website | http://impex2017.loria.fr |
Submission link | https://easychair.org/conferences/?conf=impex2017 |
Abstract registration deadline | August 26, 2017 |
Submission deadline | September 2, 2017 |
Background and Objectives
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 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.
List of Topics
Discussions, presentations and more generally, contributions shalladdress one or more topics described below
- Show that when making explicit the domain knowledge in formal models, several relevant hidden (because they are not explicitlymodelled 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.
Submission Guidelines
Papers should be written in English and not exceed 15 pages for long papers and 8 pages for short papers in EPTCS format (http://www.eptcs.org/ for details). Submission should be made through the IMPEX 2017 submission page (https://easychair.org/conferences/?conf=impex2017), handled by the EasyChair conference management system.
Proceedings
- Preliminary proceedings, including all the papers selected for the workshop, will be available electronically at the workshop.
- Post proceedings will be published after the workshiop with Electronic Proceedings in Theoretical Computer Science (EPTCS).
Important Dates
- Abstract Submission: 26 August 2017
- Full Paper Submission: 2 September 2017
- Acceptance/Rejection Notification: 1 October 2017
- Camera-ready Paper for preliminary proceedings: October 28, 2017
- Camera-ready Paper for post-proceedings: 30 November 2017
Committees
Program Committee
-
Yamine Ait Ameur, IRIT/INPT-ENSEEIHT, France
-
Marco Casanova, Catholic University of Rio de Janeiro, Brazil
-
Calvanese Diego, Free University of Bozen-Bolzano, Italy
-
Eric Dubois, Luxembourg Institute for Science and Technology, Luxembourg
-
Josテゥ Fiadeiro, University of Leicester, UK
-
Marc Frappier, University of Sherbrooke, Canada
-
Stefania Gnesi, ISTI-CNR, Italy
-
Thai Son Hoang, University of Southampton, UK
-
Fuyuki Ishikawa, National Institute of Informatics, Japan
-
Régine Laleau, LACL, University of Paris-Est Crテゥteil, France (co-chair)
-
Dominique Méry, LORIA, University of Lorraine, France (co-chair)
-
Shin Nakajima, National Institute of Informatics, Japan (co-chair)
-
John Rushby, SRI International, California, USA
-
Klaus-Dieter Schewe, Software Competence Centre Hagenberg, Linz, Austria
-
Cong Tian, Xidian University, China
-
Elena Troubitsyna, |o Akademi University, Finland
-
Qing Wang, Australian National University, Canberra, Australia
-
Alan Wassyng, McMaster University, Canada
-
Hirokazu Yatsu, Kyushu University, Fukuoka, Japan
Organizing committee
-
Régine Laleau, LACL, University of Paris-Est Crテゥteil, France
-
Dominique Méry, LORIA, University of Lorraine, France
-
Shin Nakajima, National Institute of Informatics, Japan
Publication
Papers accepted for presentation will be published in EPTCS. Authors of selected papers from IMPEX 2017 will be invited to submit an extended version to a journal (ISSE Springer agreement). However, such an invitation does not imply acceptance of the paper. All the submissions will be evaluated following the guidelines set by the journal. Only those which satisfy all the criteria will be accepted for publication.
Contact
All questions about submissions should be emailed to Régine Laleau or Dominique Méry or Shin Nakajima
Sponsors
- ANR Project IMPEX (http://impex.loria.fr and http://www.agence-nationale-recherche.fr/?Projet=ANR-13-INSE-0001)
- ANR Project Formose (http://formose.lacl.fr and http://www.agence-nationale-recherche.fr/projet-anr/?tx_lwmsuivibilan_pi2%5BCODE%5D=ANR-14-CE28-0009)
- Université de Lorraine, France
- Université Paris Est Créteil, France