Loading...
Please wait, while we are loading the content...
Similar Documents
Assume-guarantee verification of source code with design-level assumptions
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Pasareanu, Corina S. Giannakopoulou, Dimitra Cobleigh, Jamieson M. |
| Copyright Year | 2004 |
| Description | Model checking is an automated technique that can be used to determine whether a system satisfies certain required properties. To address the 'state explosion' problem associated with this technique, we propose to integrate assume-guarantee verification at different phases of system development. During design, developers build abstract behavioral models of the system components and use them to establish key properties of the system. To increase the scalability of model checking at this level, we have developed techniques that automatically decompose the verification task by generating component assumptions for the properties to hold. The design-level artifacts are subsequently used to guide the implementation of the system, but also to enable more efficient reasoning at the source code-level. In particular we propose to use design-level assumptions to similarly decompose the verification of the actual system implementation. We demonstrate our approach on a significant NASA application, where design-level models were used to identify; and correct a safety property violation, and design-level assumptions allowed us to check successfully that the property was presented by the implementation. |
| File Size | 1078189 |
| Page Count | 10 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20040068289 |
| Archival Resource Key | ark:/13960/t43r5tj4b |
| Language | English |
| Publisher Date | 2004-01-01 |
| Access Restriction | Open |
| Subject Keyword | Computer Programming And Software Source Programs Program Verification Computers Computer Systems Design Java Programming Language Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Article |
