Formal evaluation of landing gear system
Pages 75 - 84
Abstract
The failure of hardware or software in a critical system can lead to loss of lives. Design errors are a major source of the defects that can be introduced during the system development. A complementary approach like formal methods is considered as an alternative approach to identify the possible defects in the software development process using rigorous mathematical reasoning. The increasing system complexity and failure rate invoke the area of verification and validation of avionic systems. This paper describes a stepwise formal development of an aircraft landing system using Event-B. The formal models include the complex behaviour, temporal behaviour and sequence of operations of a landing gear system. The refinement based incremental development allows to verify and to validate the required safety properties. This case study is considered as a benchmark for techniques and tools dedicated to the verification of behavioural properties of systems.
References
[1]
J.-R. Abrial. Modeling in Event-B: System and Software Engineering. 2010.
[2]
Rajeev Alur and David L. Dill. A Theory of Timed Automata. Theor. Comput. Sci., 126(2): 183--235, 1994.
[3]
Dines Bjørner and Martin C. Henson, editors. Logics of Specification Languages. EATCS Textbook in Computer Science. Springer, 2007.
[4]
Frédéric Boniol and Virginie Wiels. The Landing Gear System Case Study. In Frédéric Boniol, Virginie Wiels, Yamine Ait Ameur, and Klaus-Dieter Schewe, editors, ABZ 2014: The Landing Gear Case Study, volume 433 of CCIS, pages 1--18. Springer, 2014.
[5]
Dominique Cansell, Dominique Méry, and Joris Rehm. Time Constraint Patterns for Event B Development. In Jacques Julliand and Olga Kouchnarenko, editors, B 2007: Formal Specification and Development in B, volume 4355 of Lecture Notes in Computer Science, pages 140--154. Springer Berlin Heidelberg, 2006.
[6]
Federal Aviation Administration (FAA). Aircraft Landing Gear System, Chapter 13 in Aviation Maintenance Technician Handbook - Airframe Vol-1. U.S. Dept. of Transportation, Washington, D.C., 2012.
[7]
Federal Aviation Administration (FAA). System Design and Analysis, Advisory Circular AC 25.1309-1A. http://www.faa.gov, June 1988.
[8]
Sally C. Johnson and Ricky W. Butler. Formal Methods, Chapter 21 in The Avionics Handbook. CRC Press, 2001. edited by Cary R. Spitzer.
[9]
Dominique Méry and Neeraj Kumar Singh. Modelling an Aircraft Landing System in Event-B (Full Report). Technical report. http://hal.inria.fr/hal-00971787.
[10]
Dominique Méry and Neeraj Kumar Singh. Automatic Code Generation from Event-B Models. In Proceedings of the Second Symposium on Information and Communication Technology, SoICT '11, pages 179--188, New York, NY, USA, 2011. ACM.
[11]
Dominique Méry and NeerajKumar Singh. Modeling an Aircraft Landing System in Event-B. In Frédéric Boniol, Virginie Wiels, Yamine Ait Ameur, and Klaus-Dieter Schewe, editors, ABZ 2014: The Landing Gear Case Study, volume 433 of CCIS, pages 154--159. Springer International Publishing, 2014.
[12]
RODIN. Rigorous Open Development Environment for Complex Systems. http://rodin-b-sharp.sourceforge.net. 2004--2013.
[13]
Neeraj Kumar Singh. Using Event-B for Critical Device Software Systems. Springer-Verlag GmbH, 2013.
Index Terms
- Formal evaluation of landing gear system
Recommendations
Modeling a landing gear system in Event-B
This article describes the Event-B modeling of a landing gear system of an aircraft whose complete description can be found in Boniol and Wiels (The Landing Gear System Case Study, ABZ Case Study, Communications in Computer Information Science, vol 433, ...
Analysis of DSR protocol in event-B
SSS'11: Proceedings of the 13th international conference on Stabilization, safety, and security of distributed systemsThis paper presents an incremental formal development of the Dynamic Source Routing (DSR) protocol in Event-B. DSR is a reactive routing protocol, which finds a route for a destination on demand, whenever communication is needed. Route discovery is an ...
Towards the Composition of Specifications in Event-B
The development of a system can start with the creation of a specification. Following this viewpoint, we claim that often a specification can be constructed from the combination of specifications which can be seen as composition. Event-B is a formal ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
December 2014
304 pages
ISBN:9781450329309
DOI:10.1145/2676585
- Conference Chair:
- Nguyen Trong Giang,
- General Chairs:
- Huynh Quyet Thang,
- Ismal Khalil,
- Program Chairs:
- Ngo Hong Son,
- Yves Deville,
- Marc Bui
Copyright © 2014 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 04 December 2014
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Conference
SoICT '14
SoICT '14: Fifth symposium on Information and Communication Technology
December 4 - 5, 2014
Hanoi, Viet Nam
Acceptance Rates
Overall Acceptance Rate 147 of 318 submissions, 46%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 100Total Downloads
- Downloads (Last 12 months)5
- Downloads (Last 6 weeks)0
Reflects downloads up to 17 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in