| Descripción: |
From the earliest hardware and software days to the internet era, complexity of computer systems has been something computer scientists, engineers, and programmers have had to deal with. Important fields of research and technology have originated, developed, or matured as a side-effect of this. In this dissertation, we investigate on some of the most challenging, current research directions that are related to the formal specification and verification of complex computer systems.
In this thesis, we focus on distributed systems such as Web systems and biological systems. In order to provide analysis and verification models and tools for these complex computing systems, we use Domain Specific Languages (DSLs). The first part of the thesis is devoted to security aspects and related techniques such as software certification. First, we study access control systems and propose a language for specifying access control policies that are tightly coupled with knowledge bases that provide semantic-aware descriptions of the accessed resources or elements. Also, we develop a novel framework for Code-Carrying Theory, which is a methodology for software certification to secure delivery of code in a distributed environment. Our framework is based on a Fold/Unfold transformation system for rewrite theories. The second part of the thesis focuses on the analysis and verification of Web systems and biological systems. As for web information retrieval, we propose a language for filtering information from big data repositories which uses semantic information retrieved from remote ontologies to refine the filtering process. Also, we study validation methods to check the consistency of web contents with respect to syntax and semantics properties. As our last Web research contribution, we propose a language which allows one to define and automatically check semantic as well as syntactic constraints on the static content of a Web system. Finally, regarding biological systems, we develop a logical formalism for modeling and analysis of quantitative aspects of biological processes, which is based on rewriting logic.
To evaluate the effectiveness of all the proposed methodologies, particular attention has been devoted to the development of prototype systems that have been implemented by using rule-based languages. |
