1,721,019 research outputs found
PHIL: A Lazy Implementation of a Language for Approximate Filtering of XML Documents
No full textIn this paper, we introduce a system, written in Haskell, for filtering information from XML data. Essentially,
the system implements a simple declarative language which allows one to extract relevant data as well as to exclude useless and misleading contents from an XML document by matching patterns against XML documents.
The matching mechanism employes a cost-based pattern transformation algorithm which searches for patterns in an approximate way (i.e. modulo renaming, insertion, and deletion of XML items) and ranks the results w.r.t. their cost. In order to improve efficiency, the implementation uses sophisticated indexing techniques and exploits laziness to automatically avoid the construction of unnecessary data structures. We analyzed both the expressiveness of our filtering language and the performance of the system using the well known XMark benchmark suite
A Rewriting-based, Parameterized Exploration Scheme for the Dynamic Analysis of Complex Software Systems
Full text linkLos sistemas software actuales son artefactos complejos cuyo comportamiento es a menudo extremadamente difícil de entender. Este hecho ha llevado al desarrollo de metodologías formales muy sofisticadas para el análisis, comprensión y depuración de programas.
El análisis de trazas de ejecución consiste en la búsqueda dinámica de contenidos específicos dentro de las trazas de ejecución de un cierto programa. La búsqueda puede llevarse a cabo hacia adelante o hacia atrás. Si bien el análisis hacia adelante se traduce en una forma de análisis de impacto que identifica el alcance y las posibles consecuencias de los cambios en la entrada del programa, el análisis hacia atrás permite llevar a cabo un rastreo de la procedencia; es decir, muestra como (partes de) la salida del programa depende de (partes de) su entrada y ayuda a estimar qué dato de la entrada es necesario modificar para llevar a cabo un cambio en el resultado.
En esta tesis se investiga una serie de metodologías de análisis de trazas que son especialmente adecuadas para el análisis de trazas de ejecución largas y complejas en la lógica de reescritura, que es un marco lógico y semántico especialmente adecuado para la formalización de sistemas altamente concurrentes.
La primera parte de la tesis se centra en desarrollar una técnica de análisis de trazas hacia atrás que alcanza enormes reducciones en el tamaño de la traza. Esta metodología se basa en la fragmentación incremental y favorece un mejor análisis y depuración ya que la mayoría de las inspecciones, tediosas e irrelevantes, que se realizan rutinariamente en el diagnostico y la localización de errores se pueden eliminar de forma automática. Esta técnica se ilustra por medio de varios ejemplos que ejecutamos mediante el sistema iJulienne, una herramienta interactiva de fragmentación que hemos desarrollado y que implementa la técnica de análisis de trazas hacia atrás. En la segunda parte de la tesis se formaliza un sistema paramétrico, flexible y dinámico, para la exploración de computaciones en la lógica de reescritura. El esquema implementa un algoritmo de animación gen érico que permite la ejecución indeterminista de una teoría de reescritura condicional dada y que puede ser objeto de seguimiento mediante el uso de diferentes modalidades, incluyendo una ejecución gradual paso a paso y una fragmentación automática hacia adelante y/o hacia atrás, lo que reduce drásticamente el tamaño y la complejidad de las trazas bajo inspección y permite a los usuarios evaluar de forma aislada los efectos de una declaración o instrucción dada, el seguimiento de los efectos del cambio de la entrada, y obtener información sobre el comportamiento del programa (o mala conducta del mismo). Por otra parte, la fragmentación de la traza de ejecución puede identificar nuevas oportunidades de optimización del programa. Con esta metodología, un analista puede navegar, fragmentar, filtrar o buscar en la traza durante la ejecución del programa. El marco de análisis de trazas gen érico se ha implementado en el sistema Anima y describimos una profunda evaluación experimental de este que demuestra la utilidad del enfoque propuesto.Frechina Navarro, F. (2014). A Rewriting-based, Parameterized Exploration Scheme for the Dynamic Analysis of Complex Software Systems [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/44234TESI
Rewriting-based Verification and Debugging of Web Systems
Full text linkThe increasing complexity of Web system has led to the development of sophisticated formal methodologies for verifying and correcting Web data and Web programs.
In general, establishing whether a Web system behaves correctly with respect to the original intention of the programmer or checking its internal consistency
are non-trivial tasks as witnessed by many studies in the literature.
In this dissertation, we face two challenging problems related to the verification of Web systems.
Firstly, we extend a previous Web verification framework based on partial rewriting by providing a semi-automatic technique for repairing Web systems.
We propose a basic repairing methodology that is endowed with several strategies for optimizing the number of repair actions that must be executed in order to fix a given Web site.
Also, we develop an improvement of the Web verification framework that is based on abstract interpretation and greatly enhances both efficiency and scalability of the original technique.
Secondly, we formalize a framework for the specification and model-checking of dynamic Web applications that is based on Rewriting Logic.
Our framework allows one to simulate
the user navigation and the evaluation of Web scripts within a Web application, and also check important related properties such us reachability and consistency.
When a property is refuted, a counter-example with the erroneous trace is delivered.
Such information can be analyzed in order to debug the Web application under examination by means of a novel backward trace slicing technique that we formulated for this purpose.
This technique consists in tracing back, along an execution trace, all the relevant symbols of the term (or state) that we are interested to observe.Romero ., DO. (2011). Rewriting-based Verification and Debugging of Web Systems [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/12496Palanci
Rule-Based Software Verification and Correction
Full text linkThe increasing complexity of software systems has led to the development of sophisticated formal Methodologies for verifying and correcting data and programs. In general, establishing whether a program behaves correctly w.r.t. the original programmer s intention or checking the consistency and the correctness of a large set of data are not trivial tasks as witnessed by many case studies which occur in the literature.
In this dissertation, we face two challenging problems of verification and correction. Specifically, verification and correction of declarative programs, and the verification and correction of Web sites (i.e. large collections of semistructured data).
Firstly, we propose a general correction scheme for automatically correcting declarative, rule-based programs which exploits a combination of bottom-up as well as topdown inductive learning techniques. Our hybrid hodology is able to infer program corrections that are hard, or even impossible, to obtain with a simpler,automatic top-down or bottom-up learner. Moreover, the scheme will be also particularized to some well-known declarative programming paradigm: that is, the functional logic and the functional programming paradigm.
Secondly, we formalize a framework for the automated verification of Web sites which can be used to specify integrity conditions for a given Web site, and then automatically check whether these conditions are fulfilled. We provide a rule-based, formal specification language which allows us to define syntactic as well as semantic
properties of the Web site. Then, we formalize a verification technique which detects both incorrect/forbidden patterns as well as lack of information, that is, incomplete/missing Web pages. Useful information is gathered during the verification process which can be used to repair the Web site. So, after a verification phase, one
can also infer semi-automatically some possible corrections in order to fix theWeb site.
The methodology is based on a novel rewritBallis, D. (2005). Rule-Based Software Verification and Correction [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/1948Palanci
Special issue of the Journal of Symbolic Computation on Automated Specification and Verification of Web Systems
No full text
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
