{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/26231"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/26231","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Rewriting-based formal modeling, analysis and implementation of real-time distributed services","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Al-Turki, Musab A."],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Meseguer, José","Agha, Gul A.","Gunter, Carl A.","Misra, Jayadev","Roşu, Grigore"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-08-25T22:19:42Z","date_published":"2011-08-25T22:19:42Z","updated_at":"2026-07-22T22:25:26Z","subjects":["Rewriting Logic","Maude","Orc","Formal Semantics","Formal Analysis","Distributed Systems","Web Services","Formal Implementation","Real-Time Systems","Service Orchestration","Service Availability","Denial of Service Attacks","Statistical Model Checking","Adaptive Selective Verification","PVeStA","MOrc"],"languages":["en"],"rights":["Copyright 2011 Musab Ahmad Al-Turki"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/26231","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Meseguer, José","Agha, Gul A.","Gunter, Carl A.","Misra, Jayadev","Roşu, Grigore"]},{"key":"dc:creator","label":"Author","values":["Al-Turki, Musab A."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2011-08-25T22:19:42Z","2011-08"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Rewriting Logic","Maude","Orc","Formal Semantics","Formal Analysis","Distributed Systems","Web Services","Formal Implementation","Real-Time Systems","Service Orchestration","Service Availability","Denial of Service Attacks","Statistical Model Checking","Adaptive Selective Verification","PVeStA","MOrc"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2011 Musab Ahmad Al-Turki"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/26231"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2011-07-11T19:29:11Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 25 Al-Turki_Musab.zip: 4921871 bytes, checksum: 43618184ef71d396b40c6c1c45055996 (MD5) wrappers-no-sv.maude: 2136 bytes, checksum: 2b85c1d2b786eb41aa9cb7d0cb3bf66f (MD5) wrappers-naive-sv.maude: 2410 bytes, checksum: 3344c55f8af861d6dca600db947f8c6e (MD5) wrappers-common.maude: 11102 bytes, checksum: 8201aa8af272cde09239c09c85a495f7 (MD5) wrappers-asv.maude: 3201 bytes, checksum: 162c7cdb717b7e8df61fa107c7d75d72 (MD5) wrappers-aggr-sv.maude: 2992 bytes, checksum: f35ebde7f115dd343ceaa0a0854640af (MD5) orc-syntax.maude: 9507 bytes, checksum: 00229bd13e64e8fc62f7f97f22d9f414 (MD5) orc-semantics.maude: 16611 bytes, checksum: 75e2494dd2a3b956aee75e586f7bcfe2 (MD5) orc-analysis.maude: 48624 bytes, checksum: 257829294e23acfb678a1abe5480b98b (MD5) apmaude.maude: 3315 bytes, checksum: 747fdcd6d9586e53245c4e11dd94d7ec (MD5) sv-naive.maude: 2050 bytes, checksum: 825964ac0cfeab4a03d60b748be677fe (MD5) sv-aggressive.maude: 2324 bytes, checksum: 4a1876059563380516cf215291c6a5d5 (MD5) omniscient.maude: 2797 bytes, checksum: ee72cd5b5db19a50fd4242e936c153dc (MD5) common.maude: 8985 bytes, checksum: ed3495c17d2a35bdc1e8d775da24d024 (MD5) asv.maude: 2028 bytes, checksum: 37f843e9f814ed68f55b2c411aae316a (MD5) apmaude.maude: 2989 bytes, checksum: 8b1cb79644af0196fc74b1a6bbd469eb (MD5) dist-orc-model.maude: 43005 bytes, checksum: 97a05bd8a7ad41d72a9aa243a7e4fc13 (MD5) dist-orc.maude: 37621 bytes, checksum: be8d0690e7f924137ea39901f436424a (MD5) orc-objects-semantics.maude: 14846 bytes, checksum: 7d72a42efb8bcbe3069c31fd9ddd12b4 (MD5) orc-sites.maude: 2430 bytes, checksum: 95f28862757509d09a5a427e899ca777 (MD5) orc-red-semantics.maude: 6879 bytes, checksum: d5cc1933b012f84c638c3e23babbeaba (MD5) orc-sos-semantics.maude: 4941 bytes, checksum: 4d96fd76ee3854ae0c4c676e0874cec5 (MD5) orc-infrastructure.maude: 5415 bytes, checksum: dc2657e407dba859d44564431bb489f5 (MD5) orc-syntax.maude: 14902 bytes, checksum: 24e9839d74779bc16ad1070f1c02dc0f (MD5) Al-Turki_Musab.pdf: 2217336 bytes, checksum: bb65aa6780a64a4deac35ee55df5da04 (MD5)","Made available in DSpace on 2011-08-25T22:19:42Z (GMT). No. of bitstreams: 26 Al-Turki_Musab.pdf: 2217336 bytes, checksum: bb65aa6780a64a4deac35ee55df5da04 (MD5) orc-syntax.maude: 14902 bytes, checksum: 24e9839d74779bc16ad1070f1c02dc0f (MD5) orc-sos-semantics.maude: 4941 bytes, checksum: 4d96fd76ee3854ae0c4c676e0874cec5 (MD5) orc-red-semantics.maude: 6879 bytes, checksum: d5cc1933b012f84c638c3e23babbeaba (MD5) orc-sites.maude: 2430 bytes, checksum: 95f28862757509d09a5a427e899ca777 (MD5) orc-objects-semantics.maude: 14846 bytes, checksum: 7d72a42efb8bcbe3069c31fd9ddd12b4 (MD5) dist-orc.maude: 37621 bytes, checksum: be8d0690e7f924137ea39901f436424a (MD5) dist-orc-model.maude: 43005 bytes, checksum: 97a05bd8a7ad41d72a9aa243a7e4fc13 (MD5) apmaude.maude: 2989 bytes, checksum: 8b1cb79644af0196fc74b1a6bbd469eb (MD5) orc-infrastructure.maude: 5415 bytes, checksum: dc2657e407dba859d44564431bb489f5 (MD5) asv.maude: 2028 bytes, checksum: 37f843e9f814ed68f55b2c411aae316a (MD5) common.maude: 8985 bytes, checksum: ed3495c17d2a35bdc1e8d775da24d024 (MD5) omniscient.maude: 2797 bytes, checksum: ee72cd5b5db19a50fd4242e936c153dc (MD5) sv-aggressive.maude: 2324 bytes, checksum: 4a1876059563380516cf215291c6a5d5 (MD5) sv-naive.maude: 2050 bytes, checksum: 825964ac0cfeab4a03d60b748be677fe (MD5) 1_apmaude.maude: 3315 bytes, checksum: 747fdcd6d9586e53245c4e11dd94d7ec (MD5) orc-analysis.maude: 48624 bytes, checksum: 257829294e23acfb678a1abe5480b98b (MD5) orc-semantics.maude: 16611 bytes, checksum: 75e2494dd2a3b956aee75e586f7bcfe2 (MD5) 1_orc-syntax.maude: 9507 bytes, checksum: 00229bd13e64e8fc62f7f97f22d9f414 (MD5) wrappers-aggr-sv.maude: 2992 bytes, checksum: f35ebde7f115dd343ceaa0a0854640af (MD5) wrappers-asv.maude: 3201 bytes, checksum: 162c7cdb717b7e8df61fa107c7d75d72 (MD5) wrappers-common.maude: 11102 bytes, checksum: 8201aa8af272cde09239c09c85a495f7 (MD5) wrappers-naive-sv.maude: 2410 bytes, checksum: 3344c55f8af861d6dca600db947f8c6e (MD5) wrappers-no-sv.maude: 2136 bytes, checksum: 2b85c1d2b786eb41aa9cb7d0cb3bf66f (MD5) license.txt: 4057 bytes, checksum: a34d7e3812bfeb56d940c7f6e211b4a8 (MD5) Al-Turki_Musab.zip: 4921871 bytes, checksum: 43618184ef71d396b40c6c1c45055996 (MD5)"]},{"key":"dc:title","label":"Title","values":["Rewriting-based formal modeling, analysis and implementation of real-time distributed services"]}]}],"canonical_facts":{"dc:contributor":["Meseguer, José","Agha, Gul A.","Gunter, Carl A.","Misra, Jayadev","Roşu, Grigore"],"dc:creator":["Al-Turki, Musab A."],"dc:date":["2011-08-25T22:19:42Z","2011-08"],"dc:description":["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.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2011-07-11T19:29:11Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 25 Al-Turki_Musab.zip: 4921871 bytes, checksum: 43618184ef71d396b40c6c1c45055996 (MD5) wrappers-no-sv.maude: 2136 bytes, checksum: 2b85c1d2b786eb41aa9cb7d0cb3bf66f (MD5) wrappers-naive-sv.maude: 2410 bytes, checksum: 3344c55f8af861d6dca600db947f8c6e (MD5) wrappers-common.maude: 11102 bytes, checksum: 8201aa8af272cde09239c09c85a495f7 (MD5) wrappers-asv.maude: 3201 bytes, checksum: 162c7cdb717b7e8df61fa107c7d75d72 (MD5) wrappers-aggr-sv.maude: 2992 bytes, checksum: f35ebde7f115dd343ceaa0a0854640af (MD5) orc-syntax.maude: 9507 bytes, checksum: 00229bd13e64e8fc62f7f97f22d9f414 (MD5) orc-semantics.maude: 16611 bytes, checksum: 75e2494dd2a3b956aee75e586f7bcfe2 (MD5) orc-analysis.maude: 48624 bytes, checksum: 257829294e23acfb678a1abe5480b98b (MD5) apmaude.maude: 3315 bytes, checksum: 747fdcd6d9586e53245c4e11dd94d7ec (MD5) sv-naive.maude: 2050 bytes, checksum: 825964ac0cfeab4a03d60b748be677fe (MD5) sv-aggressive.maude: 2324 bytes, checksum: 4a1876059563380516cf215291c6a5d5 (MD5) omniscient.maude: 2797 bytes, checksum: ee72cd5b5db19a50fd4242e936c153dc (MD5) common.maude: 8985 bytes, checksum: ed3495c17d2a35bdc1e8d775da24d024 (MD5) asv.maude: 2028 bytes, checksum: 37f843e9f814ed68f55b2c411aae316a (MD5) apmaude.maude: 2989 bytes, checksum: 8b1cb79644af0196fc74b1a6bbd469eb (MD5) dist-orc-model.maude: 43005 bytes, checksum: 97a05bd8a7ad41d72a9aa243a7e4fc13 (MD5) dist-orc.maude: 37621 bytes, checksum: be8d0690e7f924137ea39901f436424a (MD5) orc-objects-semantics.maude: 14846 bytes, checksum: 7d72a42efb8bcbe3069c31fd9ddd12b4 (MD5) orc-sites.maude: 2430 bytes, checksum: 95f28862757509d09a5a427e899ca777 (MD5) orc-red-semantics.maude: 6879 bytes, checksum: d5cc1933b012f84c638c3e23babbeaba (MD5) orc-sos-semantics.maude: 4941 bytes, checksum: 4d96fd76ee3854ae0c4c676e0874cec5 (MD5) orc-infrastructure.maude: 5415 bytes, checksum: dc2657e407dba859d44564431bb489f5 (MD5) orc-syntax.maude: 14902 bytes, checksum: 24e9839d74779bc16ad1070f1c02dc0f (MD5) Al-Turki_Musab.pdf: 2217336 bytes, checksum: bb65aa6780a64a4deac35ee55df5da04 (MD5)","Made available in DSpace on 2011-08-25T22:19:42Z (GMT). No. of bitstreams: 26 Al-Turki_Musab.pdf: 2217336 bytes, checksum: bb65aa6780a64a4deac35ee55df5da04 (MD5) orc-syntax.maude: 14902 bytes, checksum: 24e9839d74779bc16ad1070f1c02dc0f (MD5) orc-sos-semantics.maude: 4941 bytes, checksum: 4d96fd76ee3854ae0c4c676e0874cec5 (MD5) orc-red-semantics.maude: 6879 bytes, checksum: d5cc1933b012f84c638c3e23babbeaba (MD5) orc-sites.maude: 2430 bytes, checksum: 95f28862757509d09a5a427e899ca777 (MD5) orc-objects-semantics.maude: 14846 bytes, checksum: 7d72a42efb8bcbe3069c31fd9ddd12b4 (MD5) dist-orc.maude: 37621 bytes, checksum: be8d0690e7f924137ea39901f436424a (MD5) dist-orc-model.maude: 43005 bytes, checksum: 97a05bd8a7ad41d72a9aa243a7e4fc13 (MD5) apmaude.maude: 2989 bytes, checksum: 8b1cb79644af0196fc74b1a6bbd469eb (MD5) orc-infrastructure.maude: 5415 bytes, checksum: dc2657e407dba859d44564431bb489f5 (MD5) asv.maude: 2028 bytes, checksum: 37f843e9f814ed68f55b2c411aae316a (MD5) common.maude: 8985 bytes, checksum: ed3495c17d2a35bdc1e8d775da24d024 (MD5) omniscient.maude: 2797 bytes, checksum: ee72cd5b5db19a50fd4242e936c153dc (MD5) sv-aggressive.maude: 2324 bytes, checksum: 4a1876059563380516cf215291c6a5d5 (MD5) sv-naive.maude: 2050 bytes, checksum: 825964ac0cfeab4a03d60b748be677fe (MD5) 1_apmaude.maude: 3315 bytes, checksum: 747fdcd6d9586e53245c4e11dd94d7ec (MD5) orc-analysis.maude: 48624 bytes, checksum: 257829294e23acfb678a1abe5480b98b (MD5) orc-semantics.maude: 16611 bytes, checksum: 75e2494dd2a3b956aee75e586f7bcfe2 (MD5) 1_orc-syntax.maude: 9507 bytes, checksum: 00229bd13e64e8fc62f7f97f22d9f414 (MD5) wrappers-aggr-sv.maude: 2992 bytes, checksum: f35ebde7f115dd343ceaa0a0854640af (MD5) wrappers-asv.maude: 3201 bytes, checksum: 162c7cdb717b7e8df61fa107c7d75d72 (MD5) wrappers-common.maude: 11102 bytes, checksum: 8201aa8af272cde09239c09c85a495f7 (MD5) wrappers-naive-sv.maude: 2410 bytes, checksum: 3344c55f8af861d6dca600db947f8c6e (MD5) wrappers-no-sv.maude: 2136 bytes, checksum: 2b85c1d2b786eb41aa9cb7d0cb3bf66f (MD5) license.txt: 4057 bytes, checksum: a34d7e3812bfeb56d940c7f6e211b4a8 (MD5) Al-Turki_Musab.zip: 4921871 bytes, checksum: 43618184ef71d396b40c6c1c45055996 (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/26231"],"dc:language":["en"],"dc:rights":["Copyright 2011 Musab Ahmad Al-Turki"],"dc:subject":["Rewriting Logic","Maude","Orc","Formal Semantics","Formal Analysis","Distributed Systems","Web Services","Formal Implementation","Real-Time Systems","Service Orchestration","Service Availability","Denial of Service Attacks","Statistical Model Checking","Adaptive Selective Verification","PVeStA","MOrc"],"dc:title":["Rewriting-based formal modeling, analysis and implementation of real-time distributed services"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:26Z"}