This paper discusses design for verification that uses a model checker--namely, the action language verifier (ALV)--to detect and prevent synchronization faults in the domain of avionic systems. More specifically, the paper describes experimental results obtained by applying ALV to an automated air traffic control (ATC) software element known as the tactical separation assisted flight environment (TSAFE). TSAFE is responsible for maintaining proper separation between airplanes flying in commercial airspace.

There are four main contributions in this paper: the reconstruction of TSAFE in the concurrency controller pattern, the justification for using this pattern, and identification and replacement of all synchronization statements with appropriate concurrency control protocols, such as RW and MUTX; the implementation of TSAFE using distributed client/server in Java; the creation of 140 faulty versions of TSAFE using manual seeded faults, as well as randomly and automatically seeded faults; and a two-step verification of a TSAFE behavior, interface, and behavioral verification, using the ALV model checker.

The paper is well written and well organized. It definitely represents many technical efforts in the design of very complex and critical systems. The main benefit of its approach is the efficient and effective use of the model checker to detect the synchronization problems that may cause inconsistency in the state of a safety-critical system. This possible inconsistency may result in the system being in a hazardous state that may ultimately lead to an accident.

The main concern of this approach is that it does not elaborate on how the automatic translation of the concurrency controller pattern into ALV is achieved. More specifically, the discussion regarding transformation rules is unclear and incomplete. Discussion of the transformation rules is necessary in order to better understand, and therefore better appreciate, the work and the automatic translation of the concurrency control pattern into an input that can be used by the ALV model checker.