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

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
titre	ABZ 2014
Sous-titre	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
Editeur	Springer Verlag
Pages	80-94
Nombre de pages	15
ISBN (imprimé)	9783319075112
Les DOIs	https://doi.org/10.1007/978-3-319-07512-9_6
état	Publié - 1 janv. 2014

Série de publications

Nom	Communications in Computer and Information Science
Volume	433
ISSN (imprimé)	1865-0929

Accès au document

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

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

Mammar, A., & Laleau, R. (2014). Modeling a Landing Gear System in Event-B. Dans 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 (p. 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. Dans 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, p. 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).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

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.

UR - https://www.scopus.com/pages/publications/84903542487

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

Résumé

Série de publications

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation