Study On The Automatic Testing Method For The Completeness Of Formal Specifications Based On SOFL

With the continuous development of SOFL method, as it can achieve much more complete and systematic formal specifications and different from Z and VDM formal language which are too complex to use, SOFL can be simply mastered by software developers to utilize and reveal its strengths, and this let it be perceived as an effective formal method. In the SOFL method, writing a formal specification is regarded as a method to help developers understand requirement and build a solid foundation for implementation. However, in practice, checking completeness still remains an open problem. In order to ensure that the specification covers all the user's requirements, the completeness as an important property of the specification, needs to be checked. This paper presents a tool supported testing approach to automatic checking of the completeness of formal specifications.In this paper, we first introduce the concept of specification completeness in SOFL and then explain how its automatic checking is done. Checking completeness of a specification means to check whether the specification reflects all the aspects of the user's requirements, and each functional scenario is exclusive to any other one at the same time. That is equal to say, only when both of the completeness and exclusiveness are guaranteed, we can ensure the completeness of specification. Concisely speaking, our method utilizes automatic testing techniques to automatically check the completeness. The method focuses on checking the completeness of processes by using sufficient test cases generated from appropriate predicate expressions to check the completeness condition. Finally, a case study is presented in this paper to show how our method works in practice.Only the formal specifications with completeness being guaranteed can provide solid foundation for implementation.