Loading...
Please wait, while we are loading the content...
Similar Documents
Formal verification of the runway safety monitor
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Siminiceanu, Radu Ciardo, Gianfranco |
| Copyright Year | 2006 |
| Description | The Runway Safety Monitor (RSM) designed by Lockheed Martin is part of NASA's effort to reduce runway accidents. We developed a Petri net model of the RSM protocol and used the model checking functions of our tool SMART to investigate a number of safety properties in RSM. To mitigate the impact of state-space explosion, we built a highly discretized model of the system, obtained by partitioning the monitored runway zone into a grid of smaller volumes and by considering scenarios involving only two aircraft. The model also assumes that there are no communication failures, such as bad input from radar or lack of incoming data, thus it relies on a consistent view of reality by all participants. In spite of these simplifications, we were able to expose potential problems in the RSM conceptual design. Our findings were forwarded to the design engineers, who undertook corrective action. Additionally, the results stress the efficiency attained by the new model checking algorithms implemented in SMART, and demonstrate their applicability to real-world systems. |
| File Size | 724652 |
| Page Count | 28 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20060010998 |
| Archival Resource Key | ark:/13960/t1pg6nf6z |
| Language | English |
| Publisher Date | 2006-04-01 |
| Access Restriction | Open |
| Subject Keyword | Air Transportation And Safety Protocol Computers Algorithms Runways Petri Nets Engineers Safety Avionics Program Verification Computers Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Technical Report |
