An Automatic Approach to Constructing an Understandable State Machine from a Contract-based Formal Specification
Jung-Ho Bae, Heung Seok Chae · Jeongbo gwahaghoe nonmunji. so'peuteuweeo mich eung'yong · 2012
A state machine is a dynamic behavioral model to describe behavior of a system, a component or an object. State machines are widely used for formal verification, testing and automatic code generation. Manual constructions of state machines are time-consuming and error-prone tasks because state machines capture all possible method sequences of systems. Understandability of state machines indicates how correct and quick the system behavior can be understood with the state machine. State machines can be various forms even if they represent the same behavior. Understandabilities of the difference state machines are different. Therefore understandabilities should be considered when constructing state machines. There are many approaches to automatically constructing state machines. However, they commonly have two drawbacks; incomplete automation and lack of concerns for quality such as understandability. In this paper, we propose an approach to constructing a highly understandable state machine from a contract-based formal specification. To evaluate understandabilities of constructed state machines, empirical studies have been performed. For the empirical studies, three state machines are prepared with three different techniques including our approach. The understandabilities of the state machines have been measured with eight participants per one state machine. The results shows that the state machine with our approach is the highest understandable.