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

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