Loading...
Please wait, while we are loading the content...
Similar Documents
Practical application of model checking in software verification
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Skakkebaek, Jens Ulrik Havelund Sr., Klaus |
| Copyright Year | 1999 |
| Description | This paper presents our experiences in applying the JAVA PATHFINDER (J(sub PF)), a recently developed JAVA to SPIN translator, in the finding of synchronization bugs in a Chinese Chess game server application written in JAVA. We give an overview of J(sub PF) and the subset of JAVA that it supports and describe the abstraction and verification of the game server. Finally, we analyze the results of the effort. We argue that abstraction by under-approximation is necessary for abstracting sufficiently smaller models for verification purposes; that user guidance is crucial for effective abstraction; and that current model checkers do not conveniently support the computational models of software in general and JAVA in particular. |
| File Size | 1067617 |
| Page Count | 22 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20000069002 |
| Archival Resource Key | ark:/13960/t3b043d4s |
| Language | English |
| Publisher Date | 1999-04-01 |
| Access Restriction | Open |
| Subject Keyword | Computer Programming And Software Computer Viruses China Synchronism Computer Systems Simulation Mathematical Models Game Theory 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 | Article |
