Rewriting-based formal modeling, analysis and implementation of real-time distributed services
Musab A. Alturki · 2011
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) usercentric, 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 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