Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 2/2017

15.08.2015 | ABZ 2014

Validation of the ABZ landing gear system using ProB

verfasst von: Lukas Ladenberger, Dominik Hansen, Harald Wiegard, Jens Bendisposto, Michael Leuschel

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 2/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

In this article, we present our formalization of the ABZ landing gear case study in Event-B. The development was carried out using the Rodin platform and mainly used superposition refinement to structure the specification. To validate the model, we complemented proof with animation and model checking. For the latter, we used the ProB animator and model checker. Graphical representation of the model turned out to be crucial in the development and validation of the model; this was achieved using the visualization features provided by ProB and BMotion Studio. In addition, we discuss the positive and negative aspects of the Event-B language and tools which we encountered while working on the ABZ case study.
Vorheriger Artikel Modeling a landing gear system in Event-B
Nächster Artikel The landing gear system in multi-machine Hybrid Event-B

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
The general valve is introduced in a later refinement step.
 
2
It is, however, slightly more efficient than checking each of these properties in isolation.
 
3
The projection is on the abstract variables gear and door; as now the gears and doors can move asynchronously.
 
8
Where ProB was useful to detect deadlocks during, and in some cases also after development of the model.
 
Literatur
1.
Abrial, J.-R.: The B-book: Assigning programs to meanings. Cambridge University Press, New York (1996)
2.
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)
3.
Abrial, J.-R., Butler, M., Hallerstede, S.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) Proceedings ICFEM’06, LNCS 4260, pp. 588–605. Springer-Verlag (2006)
4.
Bendisposto, J.: Directed and Distributed Model Checking of B-Specifications. Dissertation, University of Düsseldorf (2015)
5.
Bert, D., Potet, M.-L., Stouls, N.: Genesyst: A tool to reason about behavioral aspects of B event specifications. application to security properties. In ZB 2005, pages 299–318 (2005)
6.
Boniol, F., Wiels, V.: The Landing Gear System Case Study. In: ABZ Case Study. Communications in Computer Information Science, vol. 433. Springer (2014)
7.
Börger, E.: Abstract State Machines. Springer, Berlin, Heidelberg (2003)
8.
Bouton, T., de Oliveira, D.C.B., Déharbe, D., Fontaine, P.: Verit: an open, trustable and efficient smt-solver. In: Schmidt, R.A. (eds.) Proc. Conference on Automated Deduction (CADE), Lecture Notes in Computer Science, pp. 151–156. Springer (2009)
9.
Cansell, D., Méry, D., Rehm, J.: Time constraint patterns for event B development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007: Formal Specification and Development in B, 7th International Conference of B Users, Besançon, France, January 17–19, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4355 pp. 140–154. Springer (2007)
10.
Dahlström, E., Dengler, P., Grasso, A., Liley, C., McCormack, C., Schepers, D., Watt, J.: Scalable vector graphics (svg) 1.1. World Wide Web Consortium Recommendation, vol. 16 (2011)
11.
de Moura, L.M., Bjørner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS, LNCS 4963, pp. 337–340. Springer (2008)
12.
Deharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Smt solvers for rodin. In: Proceedings ABZ’2012, LNCS. Springer (to appear)
13.
Gmehlich, R., Grau, K., Hallerstede, S., Leuschel, M., Lösch, F., Plagge, D.: On fitting a formal method into practice. In: Qin, S., Qiu, Z. (eds.) Proceedings ICFEM’2011, Lecture Notes in Computer Science, vol. 6991, pp. 195–210. Springer (2011)
14.
Hallerstede, S., Jastram, M., Ladenberger, L.: A method and tool for tracing requirements into specifications. Sci. Comput. Program. 82, 2–21 (2014)CrossRef
15.
Hallerstede, S., Leuschel, M.: Constraint-based deadlock checking of high-level specifications. TPLP 11(4–5), 767–782 (2011)MathSciNet
16.
Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ Landing Gear System using ProB. In: ABZ 2014: The Landing Gear Case Study, pp. 66–79. Springer (2014)
17.
Hoang, T.S., Abrial, J.: Event-b decomposition for parallel programs. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) Abstract State Machines, Alloy, B and Z, Second International Conference, ABZ 2010, Orford, QC, Canada, February 22–25, 2010. Proceedings, Lecture Notes in Computer Science, vol. 5977, pp. 319–333. Springer (2010)
18.
Koenig, D., Glover, A., King, P., Laforge, G., Skeet, J.: Groovy in action, vol. 91. Manning (2007)
19.
Krings, S., Bendisposto, J., Leuschel, M.: Turning failure into proof: evaluating the prob disprover. In: Proceedings of the 1st International Workshop about Sets and Tools (2014)
20.
21.
Ladenberger, L., Bendisposto, J., Leuschel, M.: Visualising Event-B models with B-Motion Studio. In: Proceedings FMICS’2009, LNCS 5825, pp. 202–204. Verlag (2009)
22.
Ladenberger, L., Dobrikov, I., Leuschel, M.: An approach for creating domain specific visualisations of csp models. In: Giannakopoulou, D., Salan, G. (eds.) HOFM 2014, LNCS (2014)
23.
Lamport, L.: Real-time model checking is really simple. In: Borrione, D., Paul, W.J. (eds.) Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3–6, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3725, pp. 162–175. Springer (2005)
24.
Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)CrossRef
25.
Ligot, O., Bendisposto, J., Leuschel, M.: Debugging event-b models using the prob disprover plug-in. Proceedings AFADL 7 (2007)
26.
Plagge, D., Leuschel, M.: Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. STTT 11, 9–21 (2010)CrossRef
27.
Roscoe, A.W., Hoare, C.A.R., Bird R.: The Theory and Practice of Concurrency. Prentice-Hall PTR, Upper Saddle River (1997)
28.
Rubel, D., Wren, J., Clayberg, E.: The Eclipse Graphical Editing Framework (GEF). Addison-Wesley Professional (2011)
29.
Butler, M., Savicks, Vitaly, Colley, J.: Co-simulation environment for rodin: landing gear case study. Communications in Computer Information Science, vol. 433. Springer (2014)
30.
Silva, R., Butler, M.: Shared event composition/decomposition in event-b. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO, Lecture Notes in Computer Science, vol. 6957, pp. 122–141. Springer (2010)
31.
Silva, R., Pascal, C., Hoang, T .S., Butler, M .J.: Decomposition tool for event-b. Softw., Pract. Exp. 41(5), 199–208 (2011)CrossRef
32.
Su, W., Abrial, J.-R.: Aircraft landing gear system: Approaches with event-b to the modeling of an industrial system. In: ABZ 2014: The Landing Gear Case Study, pp. 19–35. Springer (2014)
33.
Metadaten
Titel
Validation of the ABZ landing gear system using ProB
verfasst von
Lukas Ladenberger
Dominik Hansen
Harald Wiegard
Jens Bendisposto
Michael Leuschel
Publikationsdatum
15.08.2015
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 2/2017
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-015-0395-9

Weitere Artikel der Ausgabe 2/2017

International Journal on Software Tools for Technology Transfer 2/2017 Zur Ausgabe

ABZ 2014

Aircraft landing gear system: approaches with Event-B to the modeling of an industrial system

ABZ 2014

The landing gear system in multi-machine Hybrid Event-B

ABZ 2014

Modeling a landing gear system in Event-B

ABZ 2014

Rigorous development process of a safety-critical system: from ASM models to Java code

Introduction

The landing gear case study: challenges and experiments

ABZ 2014

Environment-driven reachability for timed systems