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

23.09.2015 | ABZ 2014

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

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

This paper describes the modeling, done using the Event-B notation, of the aircraft landing gear case study that was proposed in a special track of the ABZ’2014 Conference. In the course of our development, we discovered some problems in our initial modeling approach. This has led us to propose a second approach and then a third one. Each approach is more efficient than the previous one in terms of proof obligations (roughly speaking: 2000, 1000, 500). All this will be described in this paper. The methodology of proving reachability and deadlock freeness are discussed. Animation and simulation are used as complementary analysis to formal proofs. We also try to go beyond this specific case study and give some thoughts about large industrial modeling.
Vorheriger Artikel The landing gear case study: challenges and experiments
Nächster Artikel Modeling a landing gear system in 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
Literatur
1.
2.
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)CrossRefMATH
3.
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)CrossRefMATH
4.
Abrial, J.-R., Butler, M.J., Hallerstede, S., Hoang, T.S., Mehta, Farhad, Voisin, Laurent: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447–466 (2010)CrossRef
5.
Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Proceedings of B’98: Recent Advances in the Development and Use of the B Method, 2nd International B Conference, Montpellier, 22–24 April 1998, pp. 83–128 (1998)
6.
Abrial, J.-R., Su, W., Zhu, H.: Formalizing hybrid systems with Event-B. In: ABZ, pp. 178–193 (2012)
7.
8.
9.
Barrett, C.W., de Moura, L., Stump, A.: Smt-comp: satisfiability modulo theories competition. In: Proceedings of 17th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol. 357, Edinburgh, Scotland, 6–10 July 2005
10.
Boniol, F., Wiels, V.: The Landing Gear System Case Study. In: ABZ Case Study. Communications in Computer Information Science, vol. 433. Springer (2014)
11.
Boström, P.: Creating sequential programs from Event-B models. In: Proceedings of, 8th International Conference on Integrated Formal Methods, pp. 74–88. Nancy, 11–14 Oct 2010
12.
Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient satisfiability modulo theories via delayed theory combination. In: Proceedings of the 17th International Conference on Computer Aided Verification, pp. 335–349 (2005)
13.
Cansell, D., Méry, D., Rehm, J.: Time constraint patterns for Event-B development. In: Proceedings of B 2007: Formal Specification and Development in B, 7th International Conference of B Users, pp. 140–154. Besançon, 17–19 January 2007
14.
Peter, F., Vadim, E.: Modelica—a unified object-oriented language for system modelling and simulation. In Proceedings of ECOOP’98—Object-Oriented Programming, 12th European Conference, pp. 67–90. Brussels, 20-24 July 1998
15.
Fürst A., Hoang, T.S., Basin, D.A., Desai, K., Sato, N., Miyazaki, K.: Code generation for Event-B. In: Proceedings of 11th International Conference on Integrated Formal Methods, pp. 323–338. Bertinoro, 9–11 Sept 2014
16.
Hallerstede, S., Jastram, M., Ladenberger, L.: A method and tool for tracing requirements into specifications. Science of Computer Programming, p. 36 (2013)
17.
Hallerstede, S., Jastram, M., Ladenberger, L.: A method and tool for tracing requirements into specifications. Sci. Comput. Program. 82, 2–21 (2014)CrossRef
18.
Hallerstede, S., Leuschel, M.: Constraint-based deadlock checking of high-level specifications. TPLP 11(4–5), 767–782 (2011)MathSciNet
19.
Hoang, T.S., Abrial, J.-R.: Reasoning about liveness properties in Event-B. In: Proceedings of 13th International Conference on Formal Engineering Methods on Formal Methods and Software Engineering, pp. 456–471. Durham, 26–28 Oct 2011
20.
Hoang, T.S., Fürst, A., Abrial, J.-R.: Event-B patterns and their tool support. Softw. Syst. Model. 12(2), 229–244 (2013)CrossRef
21.
Kuruma, H., Basin, D.A., Abrial, J.-R.: Developing topology discovery in Event-B. Sci. Comput. Program. 74(11–12), 879–899 (2009)MathSciNetMATH
22.
Hudon, S., Hoang, T.S.: Development of control systems guided by models of their environment. Electron. Notes Theor. Comput. Sci. 280, 57–68 (2011)CrossRef
23.
Larman, C.: Applying UML and Patterns: An Introduction to Object-Oriented Analysis and Design and Iterative Development. Prentice Hall, Upper Saddle River (2004)
24.
Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)CrossRef
25.
Manna, Z., Pnueli, A.: Adequate proof principles for invariance and liveness properties of concurrent programs. Sci. Comput. Program. 4(3), 257–289 (1984)MathSciNetCrossRefMATH
26.
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems Specification. Springer, New York (1992)CrossRefMATH
27.
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems Safety. Springer, New York (1995)CrossRefMATH
28.
29.
Méry, D., Singh, N.K.: Automatic code generation from Event-B models. In: Proceedings of the 2011 Symposium on Information and Communication Technology, Hanoi, pp. 179–188. 13–14 Oct 2011
30.
Otter, M., Malmheden, M., Elmqvist, H., Mattsson, S.E., Johnsson, C.: A new formalism for modeling of reactive and hybrid systems. In: 7th international Modelica Conference, pp. 364–377 (2009)
31.
32.
Said, M.Y., Butler, M.J., Snook, C.F.: Language and tool support for class and state machine refinement in UML-B. In: Proceedings of Formal Methods, Second World Congress, Eindhoven, pp. 579–595. 2–6 Nov 2009
33.
Sarshogh, M.R., Butler, M.J.: Specification and refinement of discrete timing properties in Event-B. ECEASST, vol. 46 (2011)
34.
Savicks, V., Butler, M., Colley, J.: Co-simulation environment for Rodin: landing gear case study. In: ABZ 2014: The Landing Gear Case Study, pp. 148–153 (2014)
35.
Wen, S., Abrial J.-R., Runlei, H., Huibiao, Z.: From requirements to development: Methodology and example. In: ICFEM, pp. 437–455 (2011)
36.
Su W., Abrial J.-R., Zhu H.: Complementary methodologies for developing hybrid systems with Event-B. In: ICFEM, pp. 230–248 (2012)
37.
Voisin, L., Abrial, J.-R.: The rodin platform has turned ten. In: Proceedings of Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, pp. 1–8. Toulouse, 2–6 June 2014
38.
Yeganefard, S., Butler, M.J., Rezazadeh, A.: Evaluation of a guideline by formal modelling of cruise control system in Event-B. In: Proceedings of Second NASA Formal Methods Symposium—NFM 2010, pp. 182–191. Washington D.C., 13–15 April 2010
Metadaten
Titel
Aircraft landing gear system: approaches with Event-B to the modeling of an industrial system
Publikationsdatum
23.09.2015
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-0400-3

Weitere Artikel der Ausgabe 2/2017

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

ABZ 2014

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

ABZ 2014

Validation of the ABZ landing gear system using ProB

Introduction

The landing gear case study: challenges and experiments

ABZ 2014

Modeling a landing gear system in Event-B

ABZ 2014

Environment-driven reachability for timed systems

ABZ 2014

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

Premium Partner

    Bildnachweise