<p> It has been argued for some time that tabular representations of formal specifications can help in writing them, in understanding them, and in checking them. Recently it has been suggested that tabular representations also help in breaking down large verification and refinement conditions into a number of smaller ones.</p> <p> The article [32] developed the theory, but the real proof in terms of an implementation is not provided. This project is about formalizing tables in a theorem prover, Simplify, defining theorems of [32] in terms of functions written in the OCaml programming language, and conducting some case studies in verifying and refining realistic problems.</p> <p> A parser is designed to ease our job of inputting expressions. Pretty-print is also provided: all predicates and tables of the examples in our thesis are automatically generated.</p> <p> Our first example is a control system, a luxury sedan car seat. This example gives us an overall impression on how to prove correctness from tabular specification. The second example specifies a visitor information system. The design features of this example involve modeling properties and operations on sets, relations and functions by building self-defined axioms. The third example illustrates another control system, an elevator. Theorems of algorithmic refinements, stepwise data refinements, and the combination of algorithmic abstraction and data abstraction are applied correspondingly to different operations.</p> / Thesis / Master of Science (MSc)

Research on personalization, including recommender systems, focuses on applications such as in online shopping malls and simple information systems. These systems consider user profile and item information obtained from data explicitly entered by users. There it is possible to classify items involved and to personalize based on a direct mapping from user or user group to item or item group. However, in complex, dynamic, and professional information systems, such as digital libraries, additional capabilities are needed to achieve personalization to support their distinctive features: large numbers of digital objects, dynamic updates, sparse rating data, biased rating data on specific items, and challenges in getting explicit rating data from users. For this reason, more research on implicit rating data is recommended, because it is easy to obtain, suffers less from terminology issues, is more informative, and contains more user-centered information. In previous reports on my doctoral work, I discussed collecting, storing, processing, and utilizing implicit rating data of digital libraries for analysis and decision support. This dissertation presents a visualization tool, VUDM (Visual User-model Data Mining tool), utilizing implicit rating data, to demonstrate the effectiveness of implicit rating data in characterizing users, user communities, and usage trends of digital libraries. The results of user studies, performed both with typical end-users and with library experts, to test the usefulness of VUDM, support that implicit rating data is useful and can be utilized for digital library analysis software, so that both end users and experts can benefit. / Ph. D.

Building facades, serving mainly to protect occupants and structural components from natural forces, require periodic inspections for the detection and assessment of building façade anomalies. Over the past years, a growing trend of utilizing camera-equipped drones for periodical building facade inspection has emerged. Building façade anomalies, such as cracks and erosion, can be detected through analyzing drone-captured video, photographs, and infrared images. Such anomalies are known to have an impact on various building performance aspects, e.g., thermal, energy, moisture control issues. Current research efforts mainly focus on the design of drone flight schema for building inspection, 3D building model reconstruction through drone-captured images, and the detection of specific façade anomalies with these images. However, there are several research gaps impeding the improvement of automation level during the processes of building façade inspection with UAV (Unmanned Aerial Vehicle). These gaps are (1) lack effective ways to store multi-type data captured by drones with the connection to the spatial information of building facades, (2) lack high-performance tools for UAV-image analysis for the automated detection of building façade anomalies, and (3) lack a comprehensive management (i.e., storage, retrieval, analysis, and display) of large amounts and multi-media information for cyclic façade inspection. When seeking inspirations from nature, the process of drone-based facade inspection can be compared with caching birds' foraging food through spatial memory, visual sensing, and remarkable memories. This dissertation aims at investigating ways to improve the management of UAV-captured data and the automation level of drone-based façade anomaly inspection with inspirations from caching birds' foraging behavior. Firstly, a 2D spatial model of building façades was created in the geographic information system (GIS) for the registration and storage of UAV-images to assign façade spatial information to each image. Secondly, computational methods like computer vision and deep learning neural networks were applied to develop algorithms for automated extraction of visual features of façade anomalies within UAV-captured images. Thirdly, a GIS-based database was designed for the comprehensive management of heterogeneous inspection data, such as the spatial, multi-spectral, and temporal data. This research will improve the automation level of storage, retrieval, analysis, and documentation of drone-captured images to support façade inspection during a building's service lifecycle. It has promising potential for supporting the decision-making of early-intervention or maintenance strategies to prevent façade failures and improve building performance. / Doctor of Philosophy / Building facades require periodic inspections and maintenance to protect occupants and structures from natural forces like the sun, wind, rain, and snow. Over the past years, a growing trend of utilizing drones for periodical building facade inspection has emerged. Building façade anomalies, such as cracks and corrosion, can be detected from the drone-captured photographs or video. Such anomalies are known to have an impact on various building performance aspects, such as moisture issues, abnormal heat loss, and additional energy consumptions. Existing practices for detecting façade anomalies from drone-captured photographs mainly rely on manual checking by going through numerous façade images and repetitively zooming in and out these high-resolution images, which is time-consuming and labor-intensive with potential risks of human errors. Besides, this manual checking process impedes the management of drone-captured data and the documentation of façade inspection activities. At the same time, the emerging technologies of computer vision (CV) and artificial intelligence (AI) have provided many opportunities to improve the automation level of façade anomaly detection and documentation. Previous research efforts have explored the image-based generation of 3D building models using computer vision techniques, as well as image-based detection of specific anomalies using deep learning techniques. However, few studies have looked into the comprehensive management, including the storage, retrieval, analysis, and display, of drone-captured images with the spatial coordinate information of building facades; there is also a lack of high-performance image analytics tools for the automated detection of building façade anomalies. This dissertation aims at investigating ways to improve the automation level of analyzing and managing drone-captured images as well as documenting building façade inspection information. To achieve this goal, a building façade model was created in the geographic information system (GIS) for the semi-automated registration and storage of drone-captured images with spatial coordinates by using computer vision techniques. Secondly, deep learning was applied for automated detection of façade anomalies in drone-captured images. Thirdly, a GIS-based database was designed as the platform for the automated analysis and management of heterogeneous data for drone-captured images, façade model information, and detected façade anomalies. This research will improve the automation level of drone-based façade inspection throughout a building's service lifecycle. It has promising potential for supporting the decision-making of maintenance strategies to prevent façade failures and improve building performance.

In Virginia Tech's Digital Library Research Laboratory, we support subject-matter-experts (SMEs) in their pursuit of research goals. Their goals include everything from data collection to analysis to reporting. Their research commonly involves an analysis of an extensive collection of data such as tweets or web pages. Without support -- such as by our lab, developers, or data analysts/scientists -- they would undertake the data analysis themselves, using available analytical tools, frameworks, and languages. Then, to extract and produce the information needed to achieve their goals, the researchers/users would need to know what sequences of functions or algorithms to run using such tools, after considering all of their extensive functionality. Our research addresses these problems directly by designing a system that lowers the information barriers. Our approach is broken down into three parts. In the first two parts, we introduce a system that supports discovery of both information and supporting services. In the first part, we describe the methodology that incorporates User eXperience (UX) research into the process of workflow design. Through the methodology, we capture (a) what are the different user roles and goals, (b) how we break down the user goals into tasks and sub-tasks, and (c) what functions and services are required to solve each (sub-)task. In the second part, we identify and describe key components of the infrastructure implementation. This implementation captures the various goals/tasks/services associations in a manner that supports information inquiry of two types: (1) Given an information goal as query, what is the workflow to derive this information? and (2) Given a data resource, what information can we derive using this data resource as input? We demonstrate both parts of the approach, describing how we teach and apply the methodology, with three case studies. In the third part of this research, we rely on formalisms used in describing digital libraries to explain the components that make up the information system. The formal description serves as a guide to support the development of information systems that generate workflows to support SME information needs. We also specifically describe an information system meant to support information goals that relate to Twitter data. / Doctor of Philosophy / In Virginia Tech's Digital Library Research Laboratory, we support subject-matter-experts (SMEs) in their pursuit of research goals. This includes everything from data collection to analysis to reporting. Their research commonly involves an analysis of an extensive collection of data such as tweets or web pages. Without support -- such as by our lab, developers, or data analysts/scientists -- they would undertake the data analysis themselves, using available analytical tools, frameworks, and languages. Then, to extract and produce the information needed to achieve their goals, the researchers/users would need to know what sequences of functions or algorithms to run using such tools, after considering all of their extensive functionality. Further, as more algorithms are being discovered and datasets are getting larger, the information processing effort is getting more and more complicated. Our research aims to address these problems directly by attempting to lower the barriers, through a methodology that integrates the full life cycle, including the activities carried out by User eXperience (UX), analysis, development, and implementation experts. We devise a three part approach to this research. The first two parts concern building a system that supports discovery of both information and supporting services. First, we describe the methodology that introduces UX research into the process of workflow design. Second, we identify and describe key components of the infrastructure implementation. We demonstrate both parts of the approach, describing how we teach and apply the methodology, with three case studies. In the third part of this research, we extend formalisms used in describing digital libraries to encompass the components that make up our new type of extensible information system.

A comprehensive, distributed parameter, annual, watershed nonpoint source management system (WATNPS) was developed for land management planning. WATNPS simulates annual sediment, nitrogen (chemical and livestock organic), and phosphorus (chemical and livestock organic) yields from nonpoint sources. The system is linked to a GIS platform to reduce the input required by personnel during analysis. WATNPS predicts potential impacts of land management practices on surface water quality. Data were compiled for the Middle Fork Holston River (MFHR) drainage basin, Owl Run and Nomini Creek watersheds in Virginia. WATNPS utilizes annual screening models for the prediction of pollutant yields. Overland delivery ratio, phosphorus yield, and animal waste models were modified for use in the system. In-stream delivery ratio, and pollutant routing procedures were developed as a part of the overall system functionality. Development and calibration of individual in-stream delivery ratio parameters was performed based on single year data from Nomini Creek and Owl Run. A procedure was developed to rank individual watersheds and sites based on predicted pollutant yields during screening. Simulation results and individual watershed characteristics were used during the development of a drainage quality index (DQI). The DQI was developed using statistical analysis to link a water quality indicator to predicted yields and watershed characteristics. The DQI was developed to assess the impact of management within individual watersheds and among watersheds within a drainage basin. WATNPS was validated using observed data. During simulations WATNPS predicted sediment yields within 50% of observed values. Nutrient yields were predicted within a order of magnitude. Simulation of alternative livestock management practices in Owl Run reflected the same trends identified in the observed data. The Hutton Creek simulation was also consistent with water quality observations. A watershed ranking based on the DQI assessment was compared to one provided by local personnel to compare predicted trends to observed watershed conditions. A demonstration of WATNPS selected a single watershed based on watershed rankings. Critical sites were identified during WATNPS site assessment and BMPs were developed. Following BMP implementation the watershed was simulated to determine the impact on sediment, nitrogen, and phosphorus yields. / Ph. D.

Presently, the United States has yet to achieve the 1991 Intermodal Surface Transportation Efficiency Act's (ISTEA) goal of creating a seamless intermodal transportation system. In addition to the dearth of connections, the nation's poor transportation information systems limit intercity intermodal transportation. Travelers lack awareness of available transportation options and face too many separate portals for trip planning that both consume time and present inadequate information. This paper posits that the creation of an efficient and extensive web-based door-to-door intermodal trip planner can solve these problems. The proposed system will present travelers with a single portal to meet all their trip planning needs. Upon selecting specific trips, travelers can then decide to be directed to operators to make a purchase. The system will include operators from the major modal groups including intercity buses, intercity rail, commuter rail, transit, and airlines. It will also include taxis due to the disjointed nature of the US public transportation system and the need to connect users who are far from stations. The requirements to create this trip planner are explored, including the support systems, potential legal issues, and suitable entities for administration and management. A survey of 39 transportation system users revealed the existence of redundant and inadequate trip planners and that the lack of sufficient information on public transportation options is driving travelers to private vehicles for shorter distances even for those who prefer public means of transportation. Analysis of the costs and benefits of implementing the proposed system is drawn from interviews with key personnel within the transportation industry, and a review of nationwide trip planners in European countries. Finally, a roadmap is presented on how best to implement the system with inputs from both the public and private sector. Recommendations include the establishment of an industry-wide data standard, a national interagency database, and a cooperative structure that entices major players within each mode to participate in the system. Also suggested are incentives from the DOT and interested private sector members to encourage more operators to participate in the system. / Master of Science

The adoption of Geographic Information System (GIS) technology in social studies classroom practices has helped accelerate the achievement of educational goals. However, despite the value that GIS possesses for supporting student learning skills, few schools have adopted it so far. A reason for this deficiency lies in the absence of specific instructional models that demonstrate possible methods for incorporating GIS into class curriculum. This study sought to address this problem, tailored specifically for Kuwaiti social studies classrooms, with the design, development, and validation of a GIS Instructional Model to facilitate AIW. The study employed a design and development research methodology, comprised of five major phases, (i) selection of model components and theoretical foundation, (ii) analysis and development, (iii) formative feedback, (iv) revision, and (v) usability evaluation. In phase one, the Inquiry Design Model (IDM) format and components with AIW framework were selected to provide basic guidelines for the GIS Instructional Model. In phase two, following a comprehensive review of relevant academic literature, and in combination with personal experience, the researcher developed a preliminary GIS Instructional Model. In phase three, two expert reviewers evaluated the model, delivering their opinions by completing an online survey and taking part in follow-up interviews. The expert reviewers were primarily tasked with determining the model's ability to facilitate AIW in a social studies classroom, and providing suggestions for improving its performance. In phase four, the details gleaned from this formative feedback phase were then used to revise the model and enhance its effectiveness. In the last phase, six Kuwaiti expert reviewers assessed this updated version of the GIS Instructional Model to determine what barriers it might face regarding its implementation in the Kuwaiti educational system. They completed an online survey as part of this process and provided possible solutions to address perceived barriers. The data gained from expert reviewer feedback in these formative and usability evaluation phases were analyzed using qualitative methodologies. This step-by-step procedure helped to validate the model. As a result, a ready-to-implement teaching model, with all necessary teaching materials and instructions, was developed for Kuwaiti social studies classrooms. This model is proposed to enable social studies teachers to better understand how to integrate GIS into their classrooms to support AIW. Recommendations are provided for Kuwaiti educational policymakers and stakeholders to help overcome perceived obstacles that may hinder model implementation; suggestions for future research are also included. / Doctor of Philosophy / Geographical Information Systems (GIS) are software-based technologies which simplify the gathering, storing and manipulation of spatially-related data in ways which allow users to visually represent complex geographic phenomena more easily, bringing greater understanding for the world around us. As a result, the integration of GIS technology into social studies classroom practices has assisted student learning and achievement. However, despite the value which GIS possesses, few schools have integrated this technology so far. A significant reason for this limitation is the lack of clear guidelines or models which demonstrate how to employ this technology in the classroom. To help address the problem, this study developed a GIS Instructional Model for Kuwaiti social studies teachers to facilitate student authentic intellectual work, i.e. the student's demonstration of their deeper understanding for the knowledge and skills they are learning. The study employed a design and developmental research methodology, comprised of five major phases, (i) selection of model components and theoretical foundation, (ii) analysis and development, (iii) formative feedback, (iv) revision, and (v) usability evaluation. Phase one involved the selection of the study's theoretical foundation. In phase two, following a comprehensive review of relevant academic literature and, in combination with personal experience, the researcher developed a preliminary GIS Instructional Model. Two expert reviewers evaluated the model in phase three, delivering their opinions by completing an online survey and taking part in follow-up interviews. This feedback was analyzed in phase four, leading to revisions in the GIS Instructional Model to improve its quality for supporting student learning. In the final phase, six Kuwaiti expert reviewers assessed the newly-updated model to determine what barriers it might face regarding its implementation in the Kuwaiti educational system. They completed an online survey as part of this process and provided possible solutions to address these perceived obstacles. This step-by-step procedure helped to validate the model. The overall result was the development of a ready-to-implement teaching model, with all necessary educational materials and instructions, for employing GIS technology in Kuwaiti social studies classrooms to support student authentic intellectual work. In addition, recommendations were provided for Kuwaiti educational policymakers and stakeholders to help overcome perceived obstacles that may hinder model implementation; suggestions for future research are also included.

No / Human resource information systems (HRIS) usage allows the human resource (HR) professional to become a strategic player. With both increasing functionality and affordability, HRIS are being used extensively in organisations of all sizes. Despite this, surprisingly little is know about the current usage, whether disparities exist between companies of different sizes, or about the impact HRIS has on the general professional standing of the HR professional. We developed and administered a survey and gave structured interviews to assess and compare the specific areas of use and to introduce a taxonomy that provides a framework for academic discussion and comparison. We further determined whether HRIS usage was strategic, a perceived value-add for the organisation, and its impact on professional standing for HR professionals. These findings were compared to those for other professions that also use MIS. Our results showed that, on average, few differences exist between SME and large company usage. Moreover, we found that the professional standing of HR professionals has been enhanced by the specific use of HRIS for strategic partnering but that this is not as pronounced as that experienced by those from other professions.

Online Knowledge Communities, also known as online forum, are popular web-based tools that allow members to seek and share knowledge. Documents to answer varieties of questions are associated with the process of knowledge exchange. The social network of members in an Online Knowledge Community is an important factor to improve search precision. However, prior ranking functions don't handle this kind of document with using this information. In this study, we try to resolve the problem of finding authoritative documents for a user query within an Online Knowledge Community. Unlike prior ranking functions which consider either content based feature, hyperlink based feature, or document structure based feature, we explored the Online Knowledge Community social network structure and members social interaction activities to design features that can gauge the two major factors affecting user knowledge adoption decision: argument quality and source credibility. We then design a customized Genetic Algorithm to adjust the weights for new features we proposed. We compared the performance of our ranking strategy with several others baselines on a real world data www.vbcity.com/forums/. The evaluation results demonstrated that our method could improve the user search satisfaction with an obviously percentage. At the end, we concluded that our approach based on knowledge adoption model and Genetic Algorithm is a better ranking strategy in the Online Knowledge Community. / Master of Science

No / Technology application to agricultural productivity is thought to be the solution to meet food demand of the growing population. In a rapidly changing world, with the prospect of decreasing arable land due to urbanization and industrialization, agricultural output requires a 70 % increase in production levels and efficient growth in the harvesting, distribution and consumption of the resources, to meet demand. There are innovations in Information and Communications Technology that can be applied to the agricultural sector in areas of precision farming, use of farm management software, wireless sensors, and use of agricultural machinery. Remote sensing technology is playing a key role through precision agriculture. This paper highlights ways in which precision agriculture is impacting on agriculture with the use of unmanned aerial vehicles for image capturing, processing and analysis.