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.
- As the specification does not cover the reaction of modification of
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
- Although the graphs in Figure 7 and 8 were just sketched, we "reverse engineered" the formulas:
- Figure 7
f(x) = x^2.2 * 0.0025 + 95 if x <= 171
f(x) = 300 if x > 171
- Figure 8
f(x) = (7*x+60)/9
- Figure 7
The document ValidationSequencesv1.5.xlsx contains sample procedures that can be used to validate the model. It will be extended over the next few weeks. (previous version: ValidationSequencesv1.0.xlsx)
We are 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 email@example.com.
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:
- Introduce the methods and tools you used.
- Outline any distinctive features of your approach.
- Explain how your model is structured and how the structure relates to the requirements.
- What are the most important properties addressed by your solution.
- Explain any features of the requirements that are not addressed by your solution.
- Provide insights into how you approached the formalisation of the requirements.
- Describe any modelling styles / idioms that you used in your solution.
- Present key snippets of your models following the structure you outlined above (avoid presenting all the details of your models).
- Explain the role of time constraints and how you modelled it.
- Provide a link to the source models public available.
Validation & verification
- Describe strategies/tools used for validation of the model.
- Describe the verification approach used and the role it played, tools used, results of verification, degree of automation, etc.
- Describe changes to the model that resulted from the validation or verification.
- Describe ways in which the verification capabilities of your chosen technology influenced the modelling itself.
- Explain any ambiguities, limitations, flaws you identified in the specification document.
- Suggest any improvements to the requirements based on your analysis.
- Suggest any improvements to the method and tools that would help the application to the case study (future or already done).
- In what way could your solution support the derivation or verification of a software implementation?.
Submissions to Previous Case Studies
We explicitly encourage you to also submit interesting contributions for previous case studies:
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:
- Outline the main differences between your solution and the other case study solutions
- Compare your solution with other related work that you regard as relevant (not necessarily connected with the case study)
Important Dates AoE
|Abstract submission:||November 29, 2019|
|Paper submission:||December 06, 2019|
|Notification:||January 13, 2020|
|Final version:||March 02, 2020|
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 2020.