University of Illinois Urbana-Champaign

Dist-Orc: A Rewriting-based Distributed Implementation of Orc with Formal Analysis

AlTurki, Musab; Meseguer, José

Content Files
distorc-alturki-meseguer.pdf

Permalink

https://hdl.handle.net/2142/15414

Description

Title
Dist-Orc: A Rewriting-based Distributed Implementation of Orc with Formal Analysis
Author(s)
  • AlTurki, Musab
  • Meseguer, José
Issue Date
2010-04
Keyword(s)
  • Orc
  • rewriting logic semantics
  • maude
  • real-time maude
  • formal analysis
  • distributed implementation
Date of Ingest
2010-04-19T21:26:55Z
Abstract
Orc is a theory of orchestration of services that allows structured programming of distributed and timed computations. Several formal semantics have been proposed for Orc, including a rewriting logic semantics developed by the authors. Orc also has a fully fledged implementation in Java with functional programming features. However, as with descriptions of most distributed languages, there exists a fairly substantial gap between Orc's formal semantics and its implementation, in that: (i) programs in Orc are not easily deployable in a distributed implementation just by using Orc's formal semantics, and (ii) they are not readily formally analyzable at the level of a distributed Orc implementation. In this work, we overcome problems (i) and (ii) for Orc. Specifically, we describe an implementation technique based on rewriting logic and Maude that narrows this gap considerably. The enabling feature of this technique is Maude's support for external objects through TCP sockets. We describe how sockets are used to implement Orc site calls and returns, and to provide real-time timing information to Orc expressions and sites. We then show how Orc programs in the resulting distributed implementation can be formally analyzed at a reasonable level of abstraction, and discuss the assumptions under which the analysis can be deemed correct. Finally, the distributed implementation and the formal analysis methodology are illustrated with a case study.
Type of Resource
text
Genre of Resource
  • Technical Report
  • Article
Language
en
Permalink
http://hdl.handle.net/2142/15414
Copyright and License Information
You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the authors.

Owning Collections

Research and Tech Reports - Computer Science PRIMARY