Abstract State Machines, Alloy, B, TLA, VDM and Z (Proceedings ABZ 2014)

. Abstract State Machines, Alloy, B, TLA, VDM and Z (Proceedings ABZ 2014). volume 8477, 6, 2014.

  • Yamine Ait-Ameur
  • Klaus-Dieter Schewe
SerieLecture Notes of Computer Science

The 4th edition of the international conference ABZ took place in Toulouse from June 2nd to June 6th. This conference records the latest development in refinement and proof state based formal methods. It follows the success of the London (2008), Orford (2010) and Pisa (2012) editions.

This edition of ABZ was marked by two major events. In addition to ASM, B, Z, Alloy and VDM, this edition of ABZ has seen the introduction of TLA (Temporal Logic of Actions) as the sixth formal method covered by the scope of the conference. In order to emphasise the integration of TLA, Leslie LAMPORT has been invited to be one of the keynote speakers of this edition of ABZ. He accepted to give an invited talk entitled “TLA+ for Non-Dummies” the year he was distinguished by the Turing Award. Congratulations !

After the “steam Boiler” case study raised 20 years ago, the second event highlighting the 4th ABZ conference is the introduction of a case study track. The aeronautic context offered by the Toulouse area pushed us to look for a case study issued from this domain. Frédéric BONIOL and Virginie WIELS kindly and immediately accepted to propose a “landing gear system” to be modelled within proof and refinement state based methods in the scope of ABZ. A separate proceedings   volume, also  published by Springer Verlag, is dedicated to this case study.