Modeling a Landing Gear System in Event-B

Amel Mammar; Régine Laleau

doi:10.1007/978-3-319-07512-9_6

Modeling a Landing Gear System in Event-B

Amel Mammar, Régine Laleau

Université Paris-Est

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

This paper describes the Event-B modeling of the landing gear system of an aircraft whose the complete description can be found in [3]. This real-life case study has been proposed by the ABZ'2014 track that takes place in Toulouse, the European capital of the aeronautic industry. Our modeling is based on the Parnas and Madey's 4-Variable Model that permits to consider the different parts of a system. These parts are incremently introduced using the Event-B refinement technique. The entire development has been carried out under the Rodin toolset. To validate and prove the different components, we use the Atelier B, SMT and ML provers which are plugged to Rodin.

Original language	English
Title of host publication	ABZ 2014
Subtitle of host publication	The Landing Gear Case Study - Case Study Track, Held at the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, Proceedings
Publisher	Springer Verlag
Pages	80-94
Number of pages	15
ISBN (Print)	9783319075112
DOIs	https://doi.org/10.1007/978-3-319-07512-9_6
Publication status	Published - 1 Jan 2014

Publication series

Name	Communications in Computer and Information Science
Volume	433
ISSN (Print)	1865-0929

Access to Document

10.1007/978-3-319-07512-9_6

Cite this

Mammar, A., & Laleau, R. (2014). Modeling a Landing Gear System in Event-B. In ABZ 2014: The Landing Gear Case Study - Case Study Track, Held at the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, Proceedings (pp. 80-94). (Communications in Computer and Information Science; Vol. 433). Springer Verlag. https://doi.org/10.1007/978-3-319-07512-9_6

@inproceedings{00f5dc0d2fd24946b5338ad24bd5c1df,

title = "Modeling a Landing Gear System in Event-B",

abstract = "This paper describes the Event-B modeling of the landing gear system of an aircraft whose the complete description can be found in [3]. This real-life case study has been proposed by the ABZ'2014 track that takes place in Toulouse, the European capital of the aeronautic industry. Our modeling is based on the Parnas and Madey's 4-Variable Model that permits to consider the different parts of a system. These parts are incremently introduced using the Event-B refinement technique. The entire development has been carried out under the Rodin toolset. To validate and prove the different components, we use the Atelier B, SMT and ML provers which are plugged to Rodin.",

author = "Amel Mammar and R{\'e}gine Laleau",

year = "2014",

month = jan,

day = "1",

doi = "10.1007/978-3-319-07512-9\_6",

language = "English",

isbn = "9783319075112",

series = "Communications in Computer and Information Science",

publisher = "Springer Verlag",

pages = "80--94",

booktitle = "ABZ 2014",

}

Mammar, A & Laleau, R 2014, Modeling a Landing Gear System in Event-B. in ABZ 2014: The Landing Gear Case Study - Case Study Track, Held at the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, Proceedings. Communications in Computer and Information Science, vol. 433, Springer Verlag, pp. 80-94. https://doi.org/10.1007/978-3-319-07512-9_6

Modeling a Landing Gear System in Event-B. / Mammar, Amel; Laleau, Régine.
ABZ 2014: The Landing Gear Case Study - Case Study Track, Held at the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, Proceedings. Springer Verlag, 2014. p. 80-94 (Communications in Computer and Information Science; Vol. 433).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Modeling a Landing Gear System in Event-B

AU - Mammar, Amel

AU - Laleau, Régine

PY - 2014/1/1

Y1 - 2014/1/1

N2 - This paper describes the Event-B modeling of the landing gear system of an aircraft whose the complete description can be found in [3]. This real-life case study has been proposed by the ABZ'2014 track that takes place in Toulouse, the European capital of the aeronautic industry. Our modeling is based on the Parnas and Madey's 4-Variable Model that permits to consider the different parts of a system. These parts are incremently introduced using the Event-B refinement technique. The entire development has been carried out under the Rodin toolset. To validate and prove the different components, we use the Atelier B, SMT and ML provers which are plugged to Rodin.

AB - This paper describes the Event-B modeling of the landing gear system of an aircraft whose the complete description can be found in [3]. This real-life case study has been proposed by the ABZ'2014 track that takes place in Toulouse, the European capital of the aeronautic industry. Our modeling is based on the Parnas and Madey's 4-Variable Model that permits to consider the different parts of a system. These parts are incremently introduced using the Event-B refinement technique. The entire development has been carried out under the Rodin toolset. To validate and prove the different components, we use the Atelier B, SMT and ML provers which are plugged to Rodin.

U2 - 10.1007/978-3-319-07512-9_6

DO - 10.1007/978-3-319-07512-9_6

M3 - Conference contribution

AN - SCOPUS:84903542487

SN - 9783319075112

T3 - Communications in Computer and Information Science

SP - 80

EP - 94

BT - ABZ 2014

PB - Springer Verlag

ER -

Modeling a Landing Gear System in Event-B

Abstract

Publication series

Access to Document

Fingerprint

Cite this