| Unfortunately, the relevant link in the TFA is dead, but IA has it: <https://web.archive.org/web/20111019054900/http://ti.arc.nas...>. Here's some interesting quotes: > during a task’s release of a lock, but before its actual release, the task may get interrupted by the daemon if the property gets broken. This means that the task terminates without releasing the lock. The error is particularly nasty in the sense that all code, except the lock releasing itself, had been protected against this situation: in case of an interrupt the lock releasing would be executed. > The modeling effort, i.e. obtaining a PROMELA model from the LISP program, took about 12 man weeks during 6 calendar weeks, while the verification effort took about one week. ... The translation phase was non-trivial and time consuming due to the relative expressive power of LISP when compared with PROMELA. > Java PathFinder (JPF) is a translator from a non-trivial subset of Java to PROMELA. > The translator is written in 6000 lines of LISP, and was developed over a period of 8 months. JPF has been applied to a number of case studies, amongst them a 1500 line game server, a NASA file transfer protocol for satellites, and a NASA data transmission protocol for the space shuttle ground control. |