ABZ2020 – 7th International Conference on Rigorous State Based Methods

The ABZ conference is dedicated to the cross-fertilization of state-based and machine-based formal methods, like Abstract State Machines (ASM), Alloy, B, TLA, VDM and Z, that share a common conceptual foundation and are widely used in both academia and industry for the design and analysis of hardware and software systems. The conference aims for a vital exchange of knowledge and experience among the research communities around different formal methods.

Important Dates

  • Workshop proposal : 01.11.19
  • Tutorial proposal : 16.02.20
  • Case study abstract : 29.11.19
  • Paper abstract : 13.01.20
  • Conference : 25. – 29.05.20

Case Study

As successfully practiced at ABZ 2014, ABZ 2016, and ABZ 2018, the 7th edition of ABZ will include again special sessions dedicated to a shared real-life case study. The objective of this session is to enrich the set of case studies developed with ABZ methods with a practical and real-life case study. After the success of the “Landing Gear” case study at ABZ 2014 in the aeronautical context, the « Hemodialysis Machine » case study at ABZ 2016 in the medical domain, and the « Hybrid ERTMS/ETCS » at ABZ 2018 in the railway domain, this time we defined a real-life case study issued from the automotive domain.

 

 

The 13th International Symposium on Theoretical Aspects of Software Engineering July 29-31, 2019, Guilin, China

The 13th Theoretical Aspects of Software Engineering Symposium (TASE 2019) will be held in Guilin, China in July 29-31, 2019. TASE is an international symposium that aims to bring together researchers and developers from academia and industry with interest in the theoretical aspects of software engineering. Modern society is increasingly dependent on software systems that are becoming larger and more complex. This poses new challenges to current software engineering methodologies that need to be enhanced using modern results from theoretical computer science. We invite submission of research papers on topics covering all theoretical aspects of software engineering, including those describing applications of theoretical computer science in industrial applications and software engineering methodologies.

 

FM’2019 October 7-11, 2019  Porto, Portugal

FM’19 is the 23rd symposium in a series organized by the Formal Methods Europe association (FME). Every 10 years the symposium is organized as a World Congress. Twenty years after FM’99 in Toulouse, and ten years after FM’09in Eindhoven, formal methods communities from all over the world will again have the opportunity to meet. Therefore, FM’19 will be both an occasion to celebrate, and a platform for enthusiastic researchers and practitioners from a diversity of backgrounds and schools to exchange their ideas and share their experience.

Abstract Submission: 28 March 2019

Full Paper Submission: 11 April 2019, 23:59 AoE

Dominique Méry is involved in the organisation of two workshops F-IDE and FMIS.

 

IMPEX2017 First International Workshop on Handling IMPlicit and EXplicit knowledge in formal system development

see http://impex2017.loria.fr

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. Lire la suite