Utilizing specification testing in review task trees for rigorous review of formal specifications

Review task tree (RTT) is a comprehensible notation for expressing review tasks in rigorous review of formal specifications. It has a mechanism for evaluating the final review result based on the review results of all the members (atomic tasks) of its minimal cutset. However, the notation does not provide any method for actually reviewing the atomic tasks. We present a way to utilize a specification testing method for rigorous review of the atomic tasks. Strategies for generating test cases for each kind of RTT are described and explained with examples. A small case study is conducted using the proposed technique, and the result is analyzed to show the benefit and the potential limitation of the technique.