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.

Comparación de un nuevo método de aceleración de análisis dinámicos con métodos de reducción de modelos

La dinámica estructural estudia la respuesta de una estructura ante cargas o fenómenos variables en el tiempo. En muchos casos, estos fenómenos requieren realizar análisis paramétricos de la estructura considerando una gran cantidad de configuraciones de diseño o modificaciones de la estructura. Estos cambios, ya sean en fases iniciales de diseño o en fases posteriores de rediseño, alteran las propiedades físicas de la estructura y por tanto del modelo empleado para su análisis, cuyo comportamiento dinámico se modifica en consecuencia. Un caso de estudio de este tipo de modificaciones es la supervisión de la integridad estructural, que trata de identificar la presencia de daño estructural y prever el comportamiento de la estructura tras ese daño, como puede ser la variación del comportamiento dinámico de la estructura debida a una delaminación, la aparición o crecimiento de grieta, la debida a la pérdida de pala sufrida por el motor de un avión en vuelo, o la respuesta dinámica de construcciones civiles como puentes o edificios frente a cargas sísmicas. Si a la complejidad de los análisis dinámicos requeridos en el caso de grandes estructuras se añade la variación de determinados parámetros en busca de una respuesta dinámica determinada o para simular la presencia de daños, resulta necesario la búsqueda de medios de simplificación o aceleración del conjunto de análisis que de otra forma parecen inabordables tanto desde el punto de vista del tiempo de computación, como de la capacidad requerida de almacenamiento y manejo de grandes volúmenes de archivos de datos. En la presente tesis doctoral se han revisado los métodos de reducción de elementos .nitos más habituales para análisis dinámicos de grandes estructuras. Se han comparado los resultados de casos de estudio de los métodos más aptos, para el tipo de estructuras y modificaciones descritas, con los resultados de aplicación de un método de reducción reciente. Entre los primeros están el método de condensación estática de Guyan extendido al caso con amortiguamiento no proporcional y posteriores implementaciones de condensaciones dinámicas en diferentes espacios vectoriales. El método de reducción recientemente presentado se denomina en esta tesis DACMAM (Dynamic Analysis in Complex Modal space Acceleration Method), y consiste en el análisis simplificado que proporciona una solución para la respuesta dinámica de una estructura, calculada en el espacio modal complejo y que admite modificaciones estructurales. El método DACMAM permite seleccionar un número reducido de grados de libertad significativos para la dinámica del fenómeno que se quiere estudiar como son los puntos de aplicación de la carga, localizaciones de los cambios estructurales o puntos donde se quiera conocer la respuesta, de forma que al implementar las modificaciones estructurales, se ejecutan los análisis necesarios sólo de dichos grados de libertad sin pérdida de precisión. El método permite considerar alteraciones de masa, rigidez, amortiguamiento y la adición de nuevos grados de libertad. Teniendo en cuenta la dimensión del conjunto de ecuaciones a resolver, la parametrización de los análisis no sólo resulta posible, sino que es también manejable y controlable gracias a la sencilla implementación del procedimiento para los códigos habituales de cálculo mediante elementos .nitos. En el presente trabajo se muestra la bondad y eficiencia del método en comparación con algunos de los métodos de reducción de grandes modelos estructurales, verificando las diferencias entre sí de los resultados obtenidos y respecto a la respuesta real de la estructura, y comprobando los medios empleados en ellos tanto en tiempo de ejecución como en tamaño de ficheros electrónicos. La influencia de los diversos factores que se tienen en cuenta permite identificar los límites y capacidades de aplicación del método y su exhaustiva comparación con los otros procedimientos. ABSTRACT Structural dynamics studies the response of a structure under loads or phenomena which vary over time. In many cases, these phenomena require the use of parametric analyses taking into consideration several design configurations or modifications of the structure. This is a typical need in an engineering o¢ ce, no matter the structural design is in early or final stages. These changes modify the physical properties of the structure, and therefore, the finite element model to analyse it. A case study, that exempli.es this circumstance, is the structural health monitoring to predict the variation of the dynamical behaviour after damage, such as a delaminated structure, a crack onset or growth, an aircraft that suffers a blade loss event or civil structures (buildings or bridges) under seismic loads. Not only large structures require complex analyses to appropriately acquire an accurate solution, but also the variation of certain parameters. There is a need to simplify the analytical process, in order to bring CPU time, data .les, management of solutions to a reasonable size. In the current doctoral thesis, the most common finite element reduction methods for large structures are reviewed. Results of case studies are compared between a recently proposed method, herein named DACMAM (Dynamic Analysis in Complex Modal space Acceleration Method), and different condensation methods, namely static or Guyan condensation and dynamic condensation in different vectorial spaces. All these methods are suitable for considering non-classical damping. The reduction method DACMAM consist of a structural modification in the complex modal domain which provides a dynamic response solution for the reduced models. This process allows the selection of a few degrees of freedom that are relevant for the dynamic response of the system. These d.o.f. are the load application points, relevant structural points or points in which it is important to know the response. Consequently, an analysis with structural modifications implies only the calculation of the dynamic response of the selected degrees of freedom added, but with no loss of information. Therefore, mass, stiffness or damping modifications are easily considered as well as new degrees of freedom. Taking into account the size of the equations to be solved, the parameterization of the dynamic solutions is not only possible, but also manageable and controllable due to the easy implementation of the procedure in the standard finite element solvers. In this thesis, the proposed reduction method for large structural models is compared with other published model order reduction methods. The comparison shows and underlines the efficiency of the new method, and veri.es the differences in the response when compared with the response of the full model. The CPU time, the data files and the scope of the parameterization are also addressed.

Manager Training and Development Strategy: A Methodology to Link Strategic Initiatives at Washington and Lee University

Washington and Lee University has developed and implemented a strategic plan and performance development initiative for 2007-2017. In concert with the strategic plan and performance development initiative, supportive manager core competencies have been identified. The deliverable for this capstone project is a documented methodology that supports the strategy for the design and implementation of a manager training and development program that ensures needed competencies are available. The author uses survey data to determine training needs and priorities and, through a review of literature, investigates effective strategies to arrive at a successful implementation methodology. The author presents findings and conclusions regarding design implementation methodology for manager training and development.

Contribution to Real-Time Estimation of Crop Phenological States in a Dynamical Framework Based on NDVI Time Series: Data Fusion With SAR and Temperature

In this study, a methodology based in a dynamical framework is proposed to incorporate additional sources of information to normalized difference vegetation index (NDVI) time series of agricultural observations for a phenological state estimation application. The proposed implementation is based on the particle filter (PF) scheme that is able to integrate multiple sources of data. Moreover, the dynamics-led design is able to conduct real-time (online) estimations, i.e., without requiring to wait until the end of the campaign. The evaluation of the algorithm is performed by estimating the phenological states over a set of rice fields in Seville (SW, Spain). A Landsat-5/7 NDVI series of images is complemented with two distinct sources of information: SAR images from the TerraSAR-X satellite and air temperature information from a ground-based station. An improvement in the overall estimation accuracy is obtained, especially when the time series of NDVI data is incomplete. Evaluations on the sensitivity to different development intervals and on the mitigation of discontinuities of the time series are also addressed in this work, demonstrating the benefits of this data fusion approach based on the dynamic systems.

Management information systems : user's guide for indentifying automatic data processing equipment (ADPE) requirements.

Issued Feb. 23, 1976.

System and circuit design of the transformatrix coefficient processor and output data channel,

Vita.

Food stamp program : implementation of electronic benefit transfer systems : report to the ranking minority member, Committee on Agriculture, Nutrition, and Forestry, U.S. Senate /

"GAO-02-332."

Resources for the implementation of total quality management (TQM) : in education, in nonprofits, and in the service sector /

Includes index.

Understanding policy implementation processes as self-organizing systems

Implementation studies and related research in organizational theory can be enhanced by drawing on the field of complex systems to understand better and, as a consequence, more successfully manage change. This article reinterprets data previously published in the British Journal of Management to reveal a new contribution, that policy implementation processes should be understood as a self-organizing system in which adaptive abilities are extremely important for stakeholders. In other words, national policy is reinterpreted at the local level, with each local organization uniquely mixing elements of national policy with their own requirements making policy implementation unpredictable and more sketchy. The original article explained different paces and directions of change in terms of traditional management processes: leadership, politics, implementation and vision. By reinterpreting the data, it is possible to reveal that deeper level processes, which are more emergent, are also at work influencing change, which the authors label possibility space. Implications for theory, policy and practice are identified.

Personal privacy as a positive experience of shopping:an illustration through the case of online grocery shopping

Purpose - This paper aims to demonstrate the need for an improved understanding of the opportunities offered by privacy online. This is contextualized in the case of supermarket purchases of food in particular, often described as an intimate and personal choice. In the case of grocery shopping, the "intimacy" may be at the household level between members or/and between e-grocers' food offerings, and their other "non-food" related services Design/methodology/approach - This paper draws upon social practice theory research, retailing and consumer behaviour in order to develop a conceptual framework for understanding the value of positive privacy. The research uses 39 in-depth interviews of e-grocery shoppers in the area of Portsmouth (UK). Findings - This paper suggests a framework for embedded elements of positive privacy into retailing strategy as a driver for growth in the e-grocery sector. Three meta-themes requiring different approaches to privacy are uncovered. Positive privacy is dynamic and contextual at the consumer/household levels as well as for product/e-grocery brands. Research limitations/implications - This paper advocates the building of long-term sustainable relationship through sharing, offering, and exchange of information rather than pure technological chasing of data. Originality/value - A consumer centred bottom-up approach is employed demonstrating the value of two-way dialogues with consumers on sensitive issues. E-grocery is used as an illustration that involves regular re-purchase of a basket of staple goods over a long period of time where privacy becomes a latent long-term concern. © Emerald Group Publishing Limited.

Selection and application of risk management tools and techniques for build-operate-transfer projects

Construction projects are risky. However, the characteristics of the risk highly depend on the type of procurement being adopted for managing the project. A build-operate-transfer (BOT) project is recognized as one of the most risky project schemes. There are instances of project failure where a BOT scheme was employed. Ineffective rts are increasingly being managed using various risk management tools and techniques. However, application of those tools depends on the nature of the project, organization's policy, project management strategy, risk attitude of the project team members, and availability of the resources. Understanding of the contents and contexts of BOT projects, together with a thorough understanding of risk management tools and techniques, helps select processes of risk management for effective project implementation in a BOT scheme. This paper studies application of risk management tools and techniques in BOT projects through reviews of relevant literatures and develops a model for selecting risk management process for BOT projects. The application to BOT projects is considered from the viewpoints of the major project participants. Discussion is also made with regard to political risks. This study would contribute to the establishment of a framework for systematic risk management in BOT projects.

Retail multinational learning:a case study of Tesco

Purpose - This article examines the internationalisation of Tesco and extracts the salient lessons learned from this process. Design/methodology/ approach - This research draws on a dataset of 62 in-depth interviews with key executives, sell- and buy-side analysts and corporate advisers at the leading investment banks in the City of London to detail the experiences of Tesco's European expansion. Findings - The case study of Tesco illuminates a number of different dimensions of the company's international experience. It offers some new insights into learning in international distribution environments such as the idea that learning is facilitated by uncertainty or "shocks" in the international retail marketplace; the size of the domestic market may inhibit change and so disable international learning; and learning is not necessarily facilitated by step-by-step incremental approaches to expansion. Research limitations/implications - The paper explores learning from a rather broad perspective, although it is hoped that these parameters can be used to raise a new set of more detailed priorities for future research on international retail learning. It is also recognised that the data gathered for this case study focus on Tesco's European operations. Practical implications - This paper raises a number of interesting issues such as whether the extremities of the business may be a more appropriate place for management to experiment and test new retail innovations, and the extent to which retailers take self-reflection seriously. Originality/value - The paper applies a new theoretical learning perspective to capture the variety of experiences during the internationalisation process, thus addressing a major gap in our understanding of the whole internationalisation process. © Emerald Group Publishing Limited.

Modelling and benchmarking business processes: The supply-line example

Benchmarking techniques have evolved over the years since Xerox’s pioneering visits to Japan in the late 1970s. The focus of benchmarking has also shifted during this period. By tracing in detail the evolution of benchmarking in one specific area of business activity, supply and distribution management, as seen by the participants in that evolution, creates a picture of a movement from single function, cost-focused, competitive benchmarking, through cross-functional, cross-sectoral, value-oriented benchmarking to process benchmarking. As process efficiency and effectiveness become the primary foci of benchmarking activities, the measurement parameters used to benchmark performance converge with the factors used in business process modelling. The possibility is therefore emerging of modelling business processes and then feeding the models with actual data from benchmarking exercises. This would overcome the most common criticism of benchmarking, namely that it intrinsically lacks the ability to move beyond current best practice. In fact the combined power of modelling and benchmarking may prove to be the basic building block of informed business process re-engineering.

Brilliant mistake! Essays on incidents of management mistakes and mea culpa

Purpose – The purpose of this paper is to examine students’ perceptions of managerial mistakes and why (and why not) managers admit mistakes. Design/methodology/approach – This paper provides a reflective account of how students’ perceive management mistakes and deal with admitting “mea culpa” – “I am to blame”. Findings – The findings show a range of attitudes: they highlight the intermingling pressures associated with the cultural environment and mistakes; they identify media characteristics and its influences on mistakes and mea culpa; they highlight ceremonial processes and tasks that shape and influence the declaration of mea culpa; and they identify how the psychology and sociology of mistakes confronts and affects students. Taken together, the study highlights the varying degrees of wariness that is carried forward by the students from vicariously learning about management mistakes. Originality/value – This paper links up with recent discussions on retail failure and retail pedagogy. It is hoped that this paper will encourage more academics to address, and engage with, management mistakes creatively in their teaching.

Exploratory data analysis with non-linear and missing data in geochemistry

Exploratory analysis of data seeks to find common patterns to gain insights into the structure and distribution of the data. In geochemistry it is a valuable means to gain insights into the complicated processes making up a petroleum system. Typically linear visualisation methods like principal components analysis, linked plots, or brushing are used. These methods can not directly be employed when dealing with missing data and they struggle to capture global non-linear structures in the data, however they can do so locally. This thesis discusses a complementary approach based on a non-linear probabilistic model. The generative topographic mapping (GTM) enables the visualisation of the effects of very many variables on a single plot, which is able to incorporate more structure than a two dimensional principal components plot. The model can deal with uncertainty, missing data and allows for the exploration of the non-linear structure in the data. In this thesis a novel approach to initialise the GTM with arbitrary projections is developed. This makes it possible to combine GTM with algorithms like Isomap and fit complex non-linear structure like the Swiss-roll. Another novel extension is the incorporation of prior knowledge about the structure of the covariance matrix. This extension greatly enhances the modelling capabilities of the algorithm resulting in better fit to the data and better imputation capabilities for missing data. Additionally an extensive benchmark study of the missing data imputation capabilities of GTM is performed. Further a novel approach, based on missing data, will be introduced to benchmark the fit of probabilistic visualisation algorithms on unlabelled data. Finally the work is complemented by evaluating the algorithms on real-life datasets from geochemical projects.