Automatic Detection and Correction of Flaws in Service Specifications

Abstract

While rigorous, mathematical techniques are helpful for improving the quality of software engineering, the threshold of learning and adapting formal methods keep many practitioners from embracing these kinds of approaches. We present the emph{Arctis Analyzer}, a tool for supporting a developer by formal methods, without the developer having to understand any formal language. To realize this tool, we developed an extensible analysis framework that is used by the analyzer to assist the user when problems are encountered. We combine model checking with syntactic analysis so as to provide a developer with not only symptoms, but also diagnoses and fixes for the underlying flaws in the specifications. Our work is based in SPACE, an approach for specifying reactive and distributed systems. In this approach, systems are composed of service specifications as opposed to traditional component specifications. Services are expressed by UML collaborations and activities representing their structure and behavior, respectively. This work focuses on analyzing the behavior of the services, hence on the UML activities. The analyzer transforms the UML models into tlaplus{}, the language of the Temporal Logic of Actions, TLA. It also generates TLA theorems for a number of properties that should hold. In order to detect property violations, the tool uses the model checker TLC to check the entire state space of the formal specifications. The analyzer can visualize any error traces from TLC in terms of the graphical model that the user is working on. This thesis presents the analyzer and how it is implemented. It also presents the analysis framework detailing twelve theorems, eleven symptoms, seven diagnoses and nine fixes. Out of these, ten theorems, six symptoms, three diagnoses and two fixes, have been implemented in the analyzer as proof of concept. The thesis also contains a number of examples showing the use of the analyzer within Arctis.