Specification-based verification and testing of open distributed systems

Abstract

The motivation for this dissertation is to increase the usefulness of Creol as a modeling language for open distributed systems and through this contribute to the overall goal of verification and testing of open distributed systems. We develop methods for tool-based testing and verification of Creol models, by introducing two different formal languages for specification of Creol components using behavioral interfaces. The formalisms lead to two different ways to use these specifications to build frameworks and tools for automatic testing of Creol models. Creol is a modeling language that is specifically designed for modeling open distributed systems with asynchronous communication. The basic programming paradigm of Creol is object orientation. The syntax of Creol is quite similar to a programming language, but Creol abstracts certain properties; thus some aspects of the system may remain undetermined in the model. In this way we get models that are more abstract than the full system, but that may be structurally quite similar to the systems and also quite complex. This again makes it necessary to ensure that also the model conform to the intended behavior of the system. By exploiting capabilities of the rewriting logic execution platform Maude—such as metalevel rewriting, efficient state exploration, and rewriting modulo equational attributes (associativity and commutativity)—we achieve efficient methods for assume-guarantee style specification-based testing and model checking of Creol components. The methods we have developed address the additional challenges for verification and testing that arise from the non-determinism of the model. We have implemented the methods as testing frameworks in rewriting logic together with examples. We have experimented with the frameworks to evaluate the testing methods. The experiments show that both methods are useful for building frameworks for automatic testing of Creol model components. Thus the main result of the dissertation is tool-supported methods for verification of Creol models of open distributed systems, and consequently methods for specification-based verification and testing of open distributed systems.