Conformance verification of finite state machines based on machine inference and model checking

Abstract

The conformance problem has attracted much interest in the research field of software verification, since the implementation that doesn’t conform to the specification may cause some errors such as the communicating interruption in the composited application. However, the earlier works in conformance verification assume that the internal structures of the implementation are explicit. It may not always be the case such as the applications that implemented in .NET or Java. In this dissertation, we propose an alternative approach for verifying a conformance between the specification and the implementation whose only external behaviors can be observed. We use an adapted version of Angluin’s algorithm to infer a deterministic Finite State Machine (FSM) from the implementations. By transforming the obtained model to the modeling formalism LTS, the model checker LTSA can be used for checking the conformance criterion in our framework. From the experiment based on Web services composition, we can detect the execution trace of the implemented Web service that does not conform to the choreography specification. Moreover, since the assumption that the implementations have to be deterministic may be too restricted in some applications (such as, a communication system or a component-based system), we also present a novel learning algorithm, namely , which can be applied to infer both deterministic and non-deterministic FSMs.