原文传递
Analyzing Mode Confusion via Model Checking.
| 题名： | Analyzing Mode Confusion via Model Checking. |
| 作者： | Carreno, Victor;Luettgen, Gerald; |
| 关键词： | PILOTS, AVIATION SAFETY, FLIGHT DECKS, DIGITAL SYSTEMS, AUTOMATION, DIAGNOSIS(GENERAL), GUIDANCE, MAN COMPUTER INTERFACE, AWARENESS. |
| 摘要： | Mode confusion is one of the most serious problems in aviation safety. Today's complex digital flight decks make it difficult for pilots to maintain awareness of the actual states, or modes, of the flight deck automation. NASA Langley leads an initiative to explore how formal techniques can be used to discover possible sources of mode confusion. As part of this initiative, a flight guidance system was previously specified as a finite Mealy automaton, and the theorem prover PVS was used to reason about it. The objective of the present paper is to investigate whether state-exploration techniques, especially model checking, are better able to achieve this task than theorem proving and also to compare several verification tools for the specific application. The flight guidance system is modeled and analyzed in Murphi, SMV, and Spin. The tools are compared regarding their system description language, their practicality for analyzing mode confusion, and their capabilities for error tracing and for animating diagnostic information. It turns out that their strengths are complementary. |
| 总页数： | 67 |
| 报告类型： | 科技报告 |
相关文献
- Designing the Control of a UAV Fleet with Model Checking.
- NEW SAFETY-BASED CHECKING PROCEDURE FOR OVERLOADS ON HIGHWAY BRIDGES.
- Progress through precedent: Going where no helicopter simulator has gone before
- A Formal Methods Approach to the Analysis of Mode Confusion
- Aviation Safety: Modeling and Analyzing Complex Interactions between Humans and Automated Systems
- Aviation Safety: Modeling and Analyzing Complex Interactions between Humans and Automated Systems.
检索历史
应用推荐
