Formal Verification of Temporal Properties for Parametrized Concurrent Programs and Concurrent Data Structures

Los tipos de datos concurrentes son implementaciones concurrentes de las abstracciones de datos clásicas, con la diferencia de que han sido específicamente diseñados para aprovechar el gran paralelismo disponible en las modernas arquitecturas multiprocesador y multinúcleo. La correcta manipulación de los tipos de datos concurrentes resulta esencial para demostrar la completa corrección de los sistemas de software que los utilizan. Una de las mayores dificultades a la hora de diseñar y verificar tipos de datos concurrentes surge de la necesidad de tener que razonar acerca de un número arbitrario de procesos que invocan estos tipos de datos de manera concurrente. Esto requiere considerar sistemas parametrizados. En este trabajo estudiamos la verificación formal de propiedades temporales de sistemas concurrentes parametrizados, poniendo especial énfasis en programas que manipulan estructuras de datos concurrentes. La principal dificultad a la hora de razonar acerca de sistemas concurrentes parametrizados proviene de la interacción entre el gran nivel de concurrencia que éstos poseen y la necesidad de razonar al mismo tiempo acerca de la memoria dinámica. La verificación de sistemas parametrizados resulta en sí un problema desafiante debido a que requiere razonar acerca de estructuras de datos complejas que son accedidas y modificadas por un numero ilimitado de procesos que manipulan de manera simultánea el contenido de la memoria dinámica empleando métodos de sincronización poco estructurados. En este trabajo, presentamos un marco formal basado en métodos deductivos capaz de ocuparse de la verificación de propiedades de safety y liveness de sistemas concurrentes parametrizados que manejan estructuras de datos complejas. Nuestro marco formal incluye reglas de prueba y técnicas especialmente adaptadas para sistemas parametrizados, las cuales trabajan en colaboración con procedimientos de decisión especialmente diseñados para analizar complejas estructuras de datos concurrentes. Un aspecto novedoso de nuestro marco formal es que efectúa una clara diferenciación entre el análisis del flujo de control del programa y el análisis de los datos que se manejan. El flujo de control del programa se analiza utilizando reglas de prueba y técnicas de verificación deductivas especialmente diseñadas para lidiar con sistemas parametrizados. Comenzando a partir de un programa concurrente y la especificación de una propiedad temporal, nuestras técnicas deductivas son capaces de generar un conjunto finito de condiciones de verificación cuya validez implican la satisfacción de dicha especificación temporal por parte de cualquier sistema, sin importar el número de procesos que formen parte del sistema. Las condiciones de verificación generadas se corresponden con los datos manipulados. Estudiamos el diseño de procedimientos de decisión especializados capaces de lidiar con estas condiciones de verificación de manera completamente automática. Investigamos teorías decidibles capaces de describir propiedades de tipos de datos complejos que manipulan punteros, tales como implementaciones imperativas de pilas, colas, listas y skiplists. Para cada una de estas teorías presentamos un procedimiento de decisión y una implementación práctica construida sobre SMT solvers. Estos procedimientos de decisión son finalmente utilizados para verificar de manera automática las condiciones de verificación generadas por nuestras técnicas de verificación parametrizada. Para concluir, demostramos como utilizando nuestro marco formal es posible probar no solo propiedades de safety sino además de liveness en algunas versiones de protocolos de exclusión mutua y programas que manipulan estructuras de datos concurrentes. El enfoque que presentamos en este trabajo resulta ser muy general y puede ser aplicado para verificar un amplio rango de tipos de datos concurrentes similares. Abstract Concurrent data types are concurrent implementations of classical data abstractions, specifically designed to exploit the great deal of parallelism available in modern multiprocessor and multi-core architectures. The correct manipulation of concurrent data types is essential for the overall correctness of the software system built using them. A major difficulty in designing and verifying concurrent data types arises by the need to reason about any number of threads invoking the data type simultaneously, which requires considering parametrized systems. In this work we study the formal verification of temporal properties of parametrized concurrent systems, with a special focus on programs that manipulate concurrent data structures. The main difficulty to reason about concurrent parametrized systems comes from the combination of their inherently high concurrency and the manipulation of dynamic memory. This parametrized verification problem is very challenging, because it requires to reason about complex concurrent data structures being accessed and modified by threads which simultaneously manipulate the heap using unstructured synchronization methods. In this work, we present a formal framework based on deductive methods which is capable of dealing with the verification of safety and liveness properties of concurrent parametrized systems that manipulate complex data structures. Our framework includes special proof rules and techniques adapted for parametrized systems which work in collaboration with specialized decision procedures for complex data structures. A novel aspect of our framework is that it cleanly differentiates the analysis of the program control flow from the analysis of the data being manipulated. The program control flow is analyzed using deductive proof rules and verification techniques specifically designed for coping with parametrized systems. Starting from a concurrent program and a temporal specification, our techniques generate a finite collection of verification conditions whose validity entails the satisfaction of the temporal specification by any client system, in spite of the number of threads. The verification conditions correspond to the data manipulation. We study the design of specialized decision procedures to deal with these verification conditions fully automatically. We investigate decidable theories capable of describing rich properties of complex pointer based data types such as stacks, queues, lists and skiplists. For each of these theories we present a decision procedure, and its practical implementation on top of existing SMT solvers. These decision procedures are ultimately used for automatically verifying the verification conditions generated by our specialized parametrized verification techniques. Finally, we show how using our framework it is possible to prove not only safety but also liveness properties of concurrent versions of some mutual exclusion protocols and programs that manipulate concurrent data structures. The approach we present in this work is very general, and can be applied to verify a wide range of similar concurrent data types.

Spatio-temporal distribution of pyrethroids in soil in Mediterranean paddy fields

Purpose The demand of rice by the increase in population in many countries has intensified the application of pesticides and the use of poor quality water to irrigate fields. The terrestrial environment is one compartment affected by these situations, where soil is working as a reservoir, retaining organic pollutants. Therefore, it is necessary to develop methods to determine insecticides in soil and monitor susceptible areas to be contaminated, applying adequate techniques to remediate them. Materials and methods This study investigates the occurrence of ten pyrethroid insecticides (PYs) and its spatio-temporal variance in soil at two different depths collected in two periods (before plow and during rice production), in a paddy field area located in the Mediterranean coast. Pyrethroids were quantified using gas chromatography?mass spectrometry (GC?MS) after ultrasound-assisted extraction with ethyl acetate. The results obtained were assessed statistically using non-parametric methods, and significant statistical differences (p < 0.05) in pyrethroids content with soil depth and proximity to wastewater treatment plants were evaluated. Moreover, a geographic information system (GIS) was used to monitor the occurrence of PYs in paddy fields and detect risk areas. Results and discussion Pyrethroids were detected at concentrations ?57.0 ng g?1 before plow and ?62.3 ng g?1 during rice production, being resmethrin and cyfluthrin the compounds found at higher concentrations in soil. Pyrethroids were detected mainly at the top soil, and a GIS program was used to depict the obtained results, showing that effluents from wastewater treatment plants (WWTPs) were the main sources of soil contamination. No toxic effects were expected to soil organisms, but it is of concern that PYs may affect aquatic organisms, which represents the worst case scenario. Conclusions A methodology to determine pyrethroids in soil was developed to monitor a paddy field area. The use of water fromWWTPs to irrigate rice fields is one of the main pollution sources of pyrethroids. It is a matter of concern that PYs may present toxic effects on aquatic organisms, as they can be desorbed from soil. Phytoremediation may play an important role in this area, reducing the possible risk associated to PYs levels in soil.

Avaliação de linguagem por ressonância magnética funcional em pacientes com epilepsia associada à esclerose mesial temporal unilateral: correlação com avaliação clínica de linguagem

Introdução: A esclerose mesial temporal (EMT) é a principal causa de epilepsia resistente ao tratamento medicamentoso. Pacientes com EMT apresentam dificuldades no processamento semântico e fonológico de linguagem e maior incidência de reorganização cerebral da linguagem (bilateral ou à direita) em relação à população geral. A ressonância magnética funcional (RMf) permite avaliar a reorganização cerebral das redes de linguagem, comparando padrões de ativação cerebral entre diversas regiões cerebrais. Objetivo: Investigar o desempenho linguístico de pacientes com EMT unilateral esquerda e direita e a ocorrência de reorganização das redes de linguagem com RMf para avaliar se a reorganização foi benéfica para a linguagem nestes pacientes. Métodos: Utilizamos provas clínicas de linguagem e paradigmas de nomeação visual e responsiva para RMf, desenvolvidos para este estudo. Foram avaliados 24 pacientes com EMTe, 22 pacientes com EMTd e 24 controles saudáveis, submetidos a provas de linguagem (fluência semântica e fonológica, nomeação de objetos, verbos, nomes próprios e responsiva, e compreensão de palavras) e a três paradigmas de linguagem por RMf [nomeação por confrontação visual (NCV), nomeação responsiva à leitura (NRL) e geração de palavras (GP)]. Seis regiões cerebrais de interesse (ROI) foram selecionadas (giro frontal inferior, giro frontal médio, giro frontal superior, giro temporal inferior, giro temporal médio e giro temporal superior). Índices de Lateralidade (ILs) foram calculados com dois métodos: bootstrap, do programa LI-Toolbox, independe de limiar, e PSC, que indica a intensidade da ativação cerebral de cada voxel. Cada grupo de pacientes (EMTe e EMTd) foi dividido em dois subgrupos, de acordo com o desempenho em relação aos controles na avaliação clinica de linguagem. O <= -1,5 foi utilizado como nota de corte para dividir os grupos em pacientes com bom e com mau desempenho de linguagem. Em seguida, comparou-se o desempenho linguístico dos subgrupos ao índices IL-boot. Resultados: Pacientes com EMT esquerda e direita mostraram pior desempenho que controles nas provas clínicas de nomeação de verbos, nomeação de nomes próprios, nomeação responsiva e fluência verbal. Os mapas de ativação cerebral por RMf mostraram efeito BOLD em regiões frontais e temporoparietais de linguagem. Os mapas de comparação de ativação cerebral entre os grupos revelaram que pacientes com EMT esquerda e direita apresentam maior ativação em regiões homólogas do hemisfério direito em relação aos controles. Os ILs corroboraram estes resultados, mostrando valores médios menores para os pacientes em relação aos controles e, portanto, maior simetria na representação da linguagem. A comparação entre o IL-boot e o desempenho nas provas clínicas de linguagem indicou que, no paradigma de nomeação responsiva à leitura, a reorganização funcional no giro temporal médio, e possivelmente, nos giros temporal inferior e superior associou-se a desempenho preservado em provas de nomeação. Conclusão: Pacientes com EMT direita e esquerda apresentam comprometimento de nomeação e fluência verbal e reorganização da rede cerebral de linguagem. A reorganização funcional de linguagem em regiões temporais, especialmente o giro temporal médio associou-se a desempenho preservado em provas de nomeação em pacientes com EMT esquerda no paradigma de RMf de nomeação responsiva à leitura

Desarrollo y caracterización de dos materiales biocerámicos basados en β-CaSiO₃ (Wollastonita) para el tratamiento pulpar del diente temporal y permanente joven

El empleo de la wollastonita ha sido ampliamente documentado en la literatura como sustituto óseo, siendo un material accesible, económico, biocompatible, bioactivo y osteoinductivo. Los cementos en base a wollastonita se presentan mezclando una fase solida (polvo) con una fase líquida para formar una pasta manejable, la cual se transforma en una masa dura en pocos minutos (mediante fraguado o desecación). El objetivo de nuestro trabajo está enfocado a mejorar y desarrollar nuevos cementos donde se emplea la wollastonita como fuente de iones calcio y sílice, para una aplicación endodóntica. Primero, el nuevo cemento fraguable fue formulado. El cemento fraguable consiste en una mezcla de aluminatos cálcicos (mayenita, Ca12Al14O33 y aluminato tricálcico, Ca3Al2O6) como componente hidráulico. El aluminato de calcio, al igual que los silicatos de calcio que componen el agregado trióxido mineral (MTA), experimenta una reacción de hidratación al mezclarlo con agua que conduce al fraguado y endurecimiento, pero a diferencia de los silicatos de calcio lo hace mucho más rápidamente. Esta mezcla de aluminatos cálcicos fue obtenida en laboratorio mediante combustión. El rápido endurecimiento del aluminato de calcio fue regulado mediante la adición de ácido cítrico, el cual actúa como inhibidor retardando la reacción de fraguado mediante el secuestro de iones calcio. Su elección está justificada por ser un compuesto económico y disponible comercialmente, estando aprobado su uso por la Agencia de Alimentos y medicamentos (FDA por Federal Drug Administration) como excipiente. Para mejorar su manejo y plasticidad se estudian distintos agentes plastificantes (polivinilpirrolidona, polietilenglicol y carboximetilcelulosa). Estos agentes también actúan como retardantes (en nuestro caso un efecto desventajoso) al disminuir la velocidad de reacción de fraguado mediante el incremento de la viscosidad del medio (efecto deseado). Todos ellos son disponibles comercialmente, estando aprobado su uso como excipientes por la FDA...

Recognizing and tagging temporal expressions in Spanish

This paper shows a system about the recognition of temporal expressions in Spanish and the resolution of their temporal reference. For the identification and recognition of temporal expressions we have based on a temporal expression grammar and for the resolution on an inference engine, where we have the information necessary to do the date operation based on the recognized expressions. For further information treatment, the output is proposed by means of XML tags in order to add standard information of the resolution obtained. Different kinds of annotation of temporal expressions are explained in another articles [WILSON2001][KATZ2001]. In the evaluation of our proposal we have obtained successful results.

Enhancing QA systems with complex temporal question processing capabilities

This paper presents a multilayered architecture that enhances the capabilities of current QA systems and allows different types of complex questions or queries to be processed. The answers to these questions need to be gathered from factual information scattered throughout different documents. Specifically, we designed a specialized layer to process the different types of temporal questions. Complex temporal questions are first decomposed into simple questions, according to the temporal relations expressed in the original question. In the same way, the answers to the resulting simple questions are recomposed, fulfilling the temporal restrictions of the original complex question. A novel aspect of this approach resides in the decomposition which uses a minimal quantity of resources, with the final aim of obtaining a portable platform that is easily extensible to other languages. In this paper we also present a methodology for evaluation of the decomposition of the questions as well as the ability of the implemented temporal layer to perform at a multilingual level. The temporal layer was first performed for English, then evaluated and compared with: a) a general purpose QA system (F-measure 65.47% for QA plus English temporal layer vs. 38.01% for the general QA system), and b) a well-known QA system. Much better results were obtained for temporal questions with the multilayered system. This system was therefore extended to Spanish and very good results were again obtained in the evaluation (F-measure 40.36% for QA plus Spanish temporal layer vs. 22.94% for the general QA system).

Evaluating knowledge-based approaches to the multilingual extension of a temporal expression normalizer

The extension to new languages is a well known bottleneck for rule-based systems. Considerable human effort, which typically consists in re-writing from scratch huge amounts of rules, is in fact required to transfer the knowledge available to the system from one language to a new one. Provided sufficient annotated data, machine learning algorithms allow to minimize the costs of such knowledge transfer but, up to date, proved to be ineffective for some specific tasks. Among these, the recognition and normalization of temporal expressions still remains out of their reach. Focusing on this task, and still adhering to the rule-based framework, this paper presents a bunch of experiments on the automatic porting to Italian of a system originally developed for Spanish. Different automatic rule translation strategies are evaluated and discussed, providing a comprehensive overview of the challenge.

Multilingual extension of a temporal expression normalizer using annotated corpora

This paper presents the automatic extension to other languages of TERSEO, a knowledge-based system for the recognition and normalization of temporal expressions originally developed for Spanish. TERSEO was first extended to English through the automatic translation of the temporal expressions. Then, an improved porting process was applied to Italian, where the automatic translation of the temporal expressions from English and from Spanish was combined with the extraction of new expressions from an Italian annotated corpus. Experimental results demonstrate how, while still adhering to the rule-based paradigm, the development of automatic rule translation procedures allowed us to minimize the effort required for porting to new languages. Relying on such procedures, and without any manual effort or previous knowledge of the target language, TERSEO recognizes and normalizes temporal expressions in Italian with good results (72% precision and 83% recall for recognition).

Evaluation of complex temporal questions in CLEF-QA

This paper presents the evaluation of a QA system for the treatment of complex temporal questions. The system was implemented in a multilayered architecture where complex temporal questions are first decomposed into simple questions, according to the temporal relations expressed in the original question. These simple questions are then processed independently by our standard Question Answering engine and their respective answers are filtered to satisfy the temporal restrictions of each simple question. The answers to the simple decomposed questions are then combined, according to the temporal relations extracted from the original complex question, to give the final answer. This evaluation was performed as a pilot task in the Spanish QA Track of the Cross Language Evaluation Forum 2004.

Splitting complex temporal questions for question answering systems

This paper presents a multi-layered Question Answering (Q.A.) architecture suitable for enhancing current Q.A. capabilities with the possibility of processing complex questions. That is, questions whose answer needs to be gathered from pieces of factual information scattered in different documents. Specifically, we have designed a layer oriented to process the different types of temporal questions. Complex temporal questions are first decomposed into simpler ones, according to the temporal relationships expressed in the original question. In the same way, the answers of each simple question are re-composed, fulfilling the temporal restrictions of the original complex question. Using this architecture, a Temporal Q.A. system has been developed. In this paper, we focus on explaining the first part of the process: the decomposition of the complex questions. Furthermore, it has been evaluated with the TERQAS question corpus of 112 temporal questions. For the task of question splitting our system has performed, in terms of precision and recall, 85% and 71%, respectively.

Grammar specification for the recognition of temporal expressions

This paper tells about the recognition of temporal expressions and the resolution of their temporal reference. A proposal of the units we have used to face up this tasks over a restricted domain is shown. We work with newspapers' articles in Spanish, that is why every reference we use is in Spanish. For the identification and recognition of temporal expressions we base on a temporal expression grammar and for the resolution on a dictionary, where we have the information necessary to do the date operation based on the recognized expressions. In the evaluation of our proposal we have obtained successful results for the examples studied.

Event ordering through temporal expression resolution

In this paper a multilingual method for event ordering based on temporal expression resolution is presented. This method has been implemented through the TERSEO system which consists of three main units: temporal expression recognizing, resolution of the coreference introduced by these expressions, and event ordering. By means of this system, chronological information related to events can be extracted from documental databases. This information is automatically added to the documental database in order to allow its use by question answering systems in those cases referring to temporality. The system has been evaluated obtaining results of 91 % precision and 71 % recall. For this, a blind evaluation process has been developed guaranteing a reliable annotation process that was measured through the kappa factor.

Elección temporal de los viajes turísticos: una aproximación con modelos de recuento

Comunicación presentada en el XIII Congreso Nacional de ACEDE, Salamanca, 21-23 septiembre 2003.

Question answering and multi-search engines in geo-temporal information retrieval

In this paper we present a complete system for the treatment of both geographical and temporal dimensions in text and its application to information retrieval. This system has been evaluated in both the GeoTime task of the 8th and 9th NTCIR workshop in the years 2010 and 2011 respectively, making it possible to compare the system to contemporary approaches to the topic. In order to participate in this task we have added the temporal dimension to our GIR system. The system proposed here has a modular architecture in order to add or modify features. In the development of this system, we have followed a QA-based approach as well as multi-search engines to improve the system performance.

Applying semantic knowledge to the automatic processing of temporal expressions and events in natural language

This paper addresses the problem of the automatic recognition and classification of temporal expressions and events in human language. Efficacy in these tasks is crucial if the broader task of temporal information processing is to be successfully performed. We analyze whether the application of semantic knowledge to these tasks improves the performance of current approaches. We therefore present and evaluate a data-driven approach as part of a system: TIPSem. Our approach uses lexical semantics and semantic roles as additional information to extend classical approaches which are principally based on morphosyntax. The results obtained for English show that semantic knowledge aids in temporal expression and event recognition, achieving an error reduction of 59% and 21%, while in classification the contribution is limited. From the analysis of the results it may be concluded that the application of semantic knowledge leads to more general models and aids in the recognition of temporal entities that are ambiguous at shallower language analysis levels. We also discovered that lexical semantics and semantic roles have complementary advantages, and that it is useful to combine them. Finally, we carried out the same analysis for Spanish. The results obtained show comparable advantages. This supports the hypothesis that applying the proposed semantic knowledge may be useful for different languages.