Name
Abstract | ||
|---|---|---|
This paper describes our work on demonstrating verification technologies on a flight-critical system of realistic functionality, size, and complexity. Our work targeted a commercial aircraft control system named Transport Class Model (TCM), and involved several stages: formalizing and disambiguating requirements in collaboration with domain experts; processing models for their use by formal verification tools; applying compositional techniques at the architectural and component level to scale verification. Performed in the context of a major NASA milestone, this study of formal verification in practice is one of the most challenging that our group has performed. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-19249-9_20 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Rate of climb,Software engineering,Systems engineering,Computer science,Critical system,Real-time computing,Requirements elicitation,Verification,Control system,Formal verification,Safety property | Journal | 9109 |
ISSN | Citations | PageRank |
0302-9743 | 12 | 0.70 |
References | Authors | |
21 | 6 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Guillaume Brat | 1 | 12 | 0.70 |
| David H. Bushnell | 2 | 12 | 0.70 |
| Misty Davies | 3 | 12 | 0.70 |
| Dimitra Giannakopoulou | 4 | 1327 | 72.46 |
| Falk Howar | 5 | 399 | 30.95 |
| Temesghen Kahsai | 6 | 221 | 14.80 |