Systematic approach for constructing an understandable state machine from a contract-based specification: controlled experiments

摘要

Contract-based specifications using OCL or JML are employed widely to describe the behaviors of systems. However, complex behaviors might not be understood using these specifications because they focus on each individual method instead of the relationships between them. State machines (SMs) can be used to model the dynamic behavior including acceptable event sequences. However, the manual construction of SMs is a time-consuming and error-prone task. Many studies have aimed to construct SMs from contract-based specifications. However, existing SM construction approaches are not concerned with certain qualities of the SMs, such as understandability. In this study, we aimed to develop a combined atomic condition-based approach for constructing highly understandable SMs from formal specifications. We conducted two controlled experiments to evaluate the understandability of the SMs constructed: technology-oriented and human-oriented evaluations. Two existing SM construction approaches, i.e., condition-partitioning-based approach and experience-based approach, were used as the controls in the two experiments, for comparison with the proposed approach. In the technology-oriented experiment, 36 SMs were constructed from 12 specifications using the three approaches. A paired-samples Wilcoxon's signed-rank test was used to test the differences in the values of a SM understandability metric based on cohesion and coupling metrics. In the human-oriented experiment, we used 15 of the 36 SMs and the differences between the understandability correctness (the number of correct answers/the number of answered questions) measured by 23 participants were tested using an independent t test. The results of the two experiments showed that the understandability of SMs constructed using the proposed approach was significantly better than that of SMs constructed using the two control approaches (). The proposed approach does not support advanced features such as the containers of contract-based specifications and the hierarchy/concurrency of SMs.