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.
List of papers. Paper #2 (Chapter 9) is removed from the thesis due to copyright restrictions.
Chapter 8/Paper #1 Einar Broch Johnsen, Olaf Owe, and Arild B. Torjusen: Validating behavioral component interfaces in rewriting logic. The definitive version published in: Proceedings IPM International Workshop on Foundations of Software Engineering (FSEN 2005). Electronic Notes in Theoretical Computer Science, May 2006, volume 159, pages 187-204.[JOT06]. doi:10.1016/j.entcs.2005.12.069
Chapter 9/Paper #2 Einar Broch Johnsen, Olaf Owe and Arild B. Torjusen: Validating behavioral component interfaces in rewriting logic. Published in Fundamenta Informaticae, 82 (2008) 341–359 [JOT08]. http://fi.mimuw.edu.pl/index.php/FI
Chapter 10/Paper #3 Arild Torjusen, Olaf Owe and Gerardo Schneider: Towards integration of XML in the Creol object-oriented language. Published as Research Report 365, Dept. of Informatics, Univ. of Oslo, Oct. 2007 (revised Feb. 2008) [TOS07a]. urn.nb.no/URN:NBN:no-18693
Chapter 11/Paper #4 Immo Grabe, Martin Steffen, and Arild B. Torjusen: Executable interface specifications for testing asynchronous Creol components. Published as Research Report 375, Dept. of Informatics, Univ. of Oslo, July 2008 (revised May 2010) [GST08]. urn.nb.no/URN:NBN:no-25758
Chapter 12/Paper #5 Olaf Owe, Martin Steffen, and Arild B. Torjusen: Model testing asynchronously communicating objects using modulo AC rewriting. The definitive version published in: Proceedings of Model-Based Testing MBT’10 (ETAPS Satellite Workshop), March 2010. Electronic Notes in Theoretical Computer Science, December 2010, volume 264, pages 69-84. doi:10.1016/j.entcs.2010.12.015