Loading...
Please wait, while we are loading the content...
Similar Documents
Formal verification of large software systems
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Yin, Xiang Knight, John |
| Copyright Year | 2010 |
| Description | We introduce a scalable proof structure to facilitate formal verification of large software systems. In our approach, we mechanically synthesize an abstract specification from the software implementation, match its static operational structure to that of the original specification, and organize the proof as the conjunction of a series of lemmas about the specification structure. By setting up a different lemma for each distinct element and proving each lemma independently, we obtain the important benefit that the proof scales easily for large systems. We present details of the approach and an illustration of its application on a challenge problem from the security domain |
| File Size | 660461 |
| Page Count | 10 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20100018552 |
| Archival Resource Key | ark:/13960/t3227wk0z |
| Language | English |
| Publisher Date | 2010-04-01 |
| Access Restriction | Open |
| Subject Keyword | Mathematical And Computer Sciences (general) Computer Systems Design Computer Systems Performance Reliability Analysis Software Reliability Program Verification Computers Computer Programs Software Engineering Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Article |
