Case Study

Table of Contents

As successfully practiced at ABZ 2014, ABZ 2016, and ABZ 2018, the 7th edition of ABZ included 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.

Specification Document

Case study system overview

The specification document of the "Adaptive Exterior Light and Speed Control System" can be found here (latest version 1.17 from 19/12/19).
You can also download previous versions: 1.2, 1.3, 1.9, 1.11, 1.14.

Additional Information

  • As the specification does not cover the reaction of modification of daytimeLights and ambientLighting, it may be assumed that these values are determined before starting the model and remain unchanged throughout simulation.
  • For the sake of simplicity it may be assumed that KeyInIgnitionOnPosition means engineOn=True whereas NoKeyInserted or KeyInserted means engineOn=False
  • Although the graphs in Figure 7 and 8 were just sketched, we "reverse engineered" the formulas:
    • Figure 7


    • Figure 8

Validation Sequences

The document ValidationSequences_v1.8.xlsx contains sample procedures that can be used to validate the model. It will be extended over the next weeks.
(previous versions: 1.0, 1.5, 1.6, 1.7)

Q&A

We offered two telephone conferences at 27.9.19 and 25.10.19, where questions regarding the case study were answered. Any questions or comments raised have been added either to the document itself or on this website (see above). If you still have any questions, please do not hesitate to contact us!

If you would like to be kept up to date on further information and updates regarding the case study, please send us a short e-mail to abz2021@uni-ulm.de.

Submissions

Note that we welcome ABZ case study submissions that use any formalism (not just ASM, Alloy, B, TLA, VDM and Z).

To make the submissions more comparable, we recommend the following paper structure/content:

Introduction

Modelling strategy

Model details

Validation & verification

Other points

Submissions to Previous Case Studies

We explicitly encourage you to also submit interesting contributions for previous case studies:

Landing gear

Hemodialysis machine

Hybrid ERTMS/ETCS Level 3

If you submit a new contribution to a previous case study, we recommend an additional section in your paper structure:

Submission Process

Submit your contribution (not more than 14 pages in LNCS format) reporting on the experiments conducted with any of the state based techniques in the scope of ABZ 2021.

Authors should consult Springer's authors' guidelines and use their proceedings templates, either for LaTeX or for Word, for the preparation of their papers. Springer encourages authors to include their ORCIDs in their papers. In addition, the corresponding author of each paper, acting on behalf of all of the authors of that paper, must complete and sign a Consent-to-Publish form. The corresponding author signing the copyright form should match the corresponding author marked on the paper. Once the files have been sent to Springer, changes relating to the authorship of the papers cannot be made.

Authors interested in contributing to ABZ 2021 in Open Access or Open Choice should refer to the corresponding Springer webpage.

Important Dates AoE

Coming soon...