IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

Rewriting-based formal modeling, analysis and implementation of real-time distributed services

Show full item record

Bookmark or cite this item: http://hdl.handle.net/2142/26231

Files in this item

File Description Format
PDF Al-Turki_Musab.pdf (2MB) (no description provided) PDF
Unknown orc-syntax.maude (15KB) (no description provided) Unknown
Unknown orc-sos-semantics.maude (5KB) (no description provided) Unknown
Unknown orc-red-semantics.maude (7KB) (no description provided) Unknown
Unknown orc-sites.maude (2KB) (no description provided) Unknown
Unknown orc-objects-semantics.maude (15KB) (no description provided) Unknown
Unknown dist-orc.maude (38KB) (no description provided) Unknown
Unknown dist-orc-model.maude (43KB) (no description provided) Unknown
Unknown apmaude.maude (3KB) (no description provided) Unknown
Unknown orc-infrastructure.maude (5KB) (no description provided) Unknown
Unknown asv.maude (2KB) (no description provided) Unknown
Unknown common.maude (9KB) (no description provided) Unknown
Unknown omniscient.maude (3KB) (no description provided) Unknown
Unknown sv-aggressive.maude (2KB) (no description provided) Unknown
Unknown sv-naive.maude (2KB) (no description provided) Unknown
Unknown 1_apmaude.maude (3KB) (no description provided) Unknown
Unknown orc-analysis.maude (49KB) (no description provided) Unknown
Unknown orc-semantics.maude (17KB) (no description provided) Unknown
Unknown 1_orc-syntax.maude (10KB) (no description provided) Unknown
Unknown wrappers-aggr-sv.maude (3KB) (no description provided) Unknown
Unknown wrappers-asv.maude (3KB) (no description provided) Unknown
Unknown wrappers-common.maude (11KB) (no description provided) Unknown
Unknown wrappers-naive-sv.maude (2KB) (no description provided) Unknown
Unknown wrappers-no-sv.maude (2KB) (no description provided) Unknown
Title: Rewriting-based formal modeling, analysis and implementation of real-time distributed services
Author(s): Al-Turki, Musab A.
Director of Research: Meseguer, José
Doctoral Committee Chair(s): Meseguer, José
Doctoral Committee Member(s): Agha, Gul A.; Gunter, Carl A.; Misra, Jayadev; Roşu, Grigore
Department / Program: Computer Science
Discipline: Computer Science
Degree Granting Institution: University of Illinois at Urbana-Champaign
Degree: Ph.D.
Genre: Dissertation
Subject(s): Rewriting Logic Maude Orc Formal Semantics Formal Analysis Distributed Systems Web Services Formal Implementation Real-Time Systems Orc Service Orchestration Service Availability Denial of Service Attacks Statistical Model Checking Adaptive Selective Verification PVeStA MOrc
Abstract: The last decade has seen an explosive growth of both: (1) enterprise service-oriented software systems, for managing enterprise resources and automating business processes, and (2) user-centric, cloud-based web applications, which provide richer experiences and more intelligent services to end-users than traditional, monolithic applications. The adoption of systems that are based on Internet-accessible software components, a class of distributed software systems to which we simply refer as \emph{Internet software}, is expected to grow tremendously in the future. Nevertheless, designing and developing dependable Internet software poses a unique set of challenges, making the already difficult issue of whether a deployed system meets its specification requirements even harder to address than for traditional software systems. In this dissertation, we develop formal specification, simulation, prototyping, and formal analysis techniques and tools for distributed software services, based on rewriting logic, the Maude system, and the theory of Orc, with the overall goal of improving the reliability of Internet software. The dissertation focuses on the formal specification and analysis of two fundamentally important aspects of Internet software systems: (1) the correctness of service compositions, and (2) the availability of services. For service composition specification and analysis, we systematically use and extend methods from the rewriting logic semantics project and apply them to service orchestrations in Orc, providing a simple, elegant and efficient formal model for timed orchestration design and analysis. The rewriting specifications of the semantics of Orc is presented in three main semantics-preserving refinements in order to achieve maximum efficiency and expressiveness: (1) an SOS-based rewriting semantics, (2) a reduction rewriting semantics, and (3) an object-based rewriting semantics. A specification of the the latter in Real-Time Maude is used as a back-end for a high-level, web-based tool, {\sc MOrc}, enabling exhaustive formal verification, including model checking, of service orchestrations in Orc. Moreover, the dissertation develops a natural transformation path from formal models of Orc programs to actual, provably-correct, distributed implementations with physical timing, which enable observing actual possible behaviors of service orchestrations in realistic environments. For the service availability problem, the dissertation extends current methods based on rewriting logic for the specification and analysis of availability properties to improve their efficiency and scalability. In particular, the dissertation first presents parallel versions of the statistical model checking algorithm of Sen, Viswanathan and Agha~\cite{SenSVA:2005} and the statistical quantitative analysis algorithm of Agha, Meseguer and Sen~\cite{AghaAMS:2006}. The parallel algorithms we propose, which are implemented in a parallel, client/server extension of \textsc{VeStA}, called \textsc{PVeStA}, exploit an inherent parallelization opportunity within these statistical analysis algorithms, where multiple, independent Monte-Carlo simulations are performed. Performance gains as a result of parallelization can in practice be remarkable, as demonstrated using several experiments. Furthermore, using Maude and {\sc PVeStA}, we apply the rewriting logic approach to availability analysis to the Adaptive Selective Verification (ASV) protocol and verify, in the presence of denial-of-service (DoS) attacks, several of its availability properties, which were previously shown either analytically or statistically by low-level network simulations. In addition, the dissertation proposes an expressive and modular method for the formal specification and analysis of service availability against DoS in service compositions using generic ASV object wrappers. This is achieved essentially by combining techniques developed for Orc service orchestrations and service availability analysis. The method is illustrated by specifying and analyzing an ASV-endowed service orchestration pattern in Orc.
Issue Date: 2011-08-25
URI: http://hdl.handle.net/2142/26231
Rights Information: Copyright 2011 Musab Ahmad Al-Turki
Date Available in IDEALS: 2011-08-25
Date Deposited: 2011-08
 

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 1179
  • Downloads this Month: 19
  • Downloads Today: 1

Browse

My Account

Information

Access Key