Use of tabular expressions in the inspection of concurrent programs

This thesis presents a systematic, rigorous inspection approach for concurrent programs. The approach has been successfully applied to a classic concurrent program of the Readers/Writers problem. In the inspection process, we rewrite the concurrent program by assigning each primitive statement a label; the transfer of control from statement to statement is made explicit. Auxiliary variables are used to record extra information for inspection without affecting the original intent of the program. The resulting program is a non-deterministic sequential program with the same behavioral effect as the original concurrent program. The rewritten program is then examined through checking the truth-value of the system invariant that fully captures program structure. A decreasing quantity of the program states is also used to show the clean completion of the program. We use tabular expressions, program-function tables, to describe the function of the program. Each column in the table is inspected individually; the program is ‘divided’ into small components to be ‘conquered’ with ease. The correctness of the whole program is implied (evaluated) by the correctness of the columns examined through the inspection.