Abstract

Ever more software systems are present in our every day life, controlling processes and tasks that are critical. Therefore, we seek the assurance that these systems work cor- rectly and reliably. Conformance testing plays a role in this, as it can be used to verify, to a certain extent, that the system we use works according to its previously verified specification. TorX ([TB03]) is a tool for conformance testing, based on the IOCO theory. For this testing it requires access to the statespace of the specification.

This thesis describes the construction of the tool SPEX which is able to generate the statespace of Promela specification, for testing with TorX. To enable this, it uses two extensions to the Promela language. The first is an IO extension to open the specified system for testing, by adding a mechanism to describe the communication/interaction between the system and its environment. The second is a Set extension to close it again for verification, by replacing input actions by symbolic variables. Access to these extensions is simplified by the use of a preprocessor which can transform simple function calls to the corresponding Promela statements.

We have used SPEX in two case studies of the conference protocol and the 5 packet handshake protocol. We found that SPEX is more memory-efficient (by around 25%) than Trojka, the current tool for statespace generation of Promela specifications. We also found that the Set extension (used in closing the specified system) is generally useful for applying abstraction to Promela models, reducing their statespace. We conclude with suggestions to still improve the preprocessor and the Set extension by introducing more functions in the preprocessor for Sets, and renewing the Set extension with constraint programming techniques.