Checking internal consistency of sofl specification: A hybrid approach

Abstract

A SOFL specification can be written with errors inside, leading to an untrustable situation for implementation. Some techniques, such as specification review and testing, have been proposed to detect and remove the errors from the specification as early as possible. Meanwhile these techniques face strong challenges when applied to practice in that they strongly rely on human intelligence to either cautiously design a review task tree for directing the whole review process, or design some test inputs to "run" the specification. The completeness of the review or testing tasks also remains a problem. In this paper we propose a hybrid approach to checking the internal consistency of a SOFL specification. The internal consistency is an important property indicating that the entire specification can work properly. The essential idea of the hybrid approach is to adopt the different strategies to check the different aspects of the specification: concrete or abstract values are used to check the satisfiability of a process, and the symbolic execution and the deduction techniques can be used to check the internal consistency of the specification at the integration level. We also use a Sort-Search example to illustrate the use of the hybrid approach. © 2014 Springer International Publishing Switzerland.