Formalization of XVSM

Context

XVSM (extensible virtual shared memory), formal specification

Task Description

Beyond the Java and .NET based implementations, there exists also a formal model for XVSM. This model defines the behavior of the XVSM middleware and serves as the basis for any implementation in a programming language. It uses nested meta data structures with algebraic access. A reference implementation in Haskell has already been developed.

In the here offered work, the major part of the specification shall be defined with formal methods like temporal logics or specification languages in a more precise way. With help of these, certain properties of the middleware shall be formally verified. Cooperation with other national and international researchers is planned.

Requirements

• Lecture "Verteiltes Programmieren mit Space Based Computing Middleware"
• experiences with formal methods

Student

partly assigned (please apply under ID = "XVSM-Formalization")

Supervisor

A.o. Univ.-Prof. Dr. Dipl.-Ing. eva Kühn

Related Projects in the Network

• Java implementation of XVSM [MozartSpaces]
• Stefan Craß, A formal model of the Extensible Virtual Shared Memory (XVSM) and its implementation in Haskell, diploma thesis, TU Wien, 2010 [link]
• Stefan Craß, eva Kühn, Gernot Salzer, Algebraic Foundation of a Data Model for an Extensible Space-Based Collaboration Protocol, Thirteenth International Database Engineering & Applications Symposium (IDEAS), Calabria, Italy, September 16-18, 2009 [link]
• eva Kühn, Richard Mordinyi, Christian Schreiber, An Extensible Space-based Coordination Approach for Modeling Complex Patterns in Large Systems. In Proceedings 3rd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation - Special Track on Formal Methods for Analysing and Verifying Very Large Systems (ISoLA), October 13-15, 2008, Porto Sani, Greece, 2008 [link]