Program verification is vital as more and more users are creating, downloading and executing foreign computer programs. Software verification tools provide a means for determining if a program adheres to a user’s security requirements, or security policy. There are many verification tools that exist for checking different types of policies on different types of programs. Currently however, there is no verification tool capable of determining if all types of programs satisfy all types of policies. This thesis describes a framework for supporting multiple verification tools to determine program satisfaction. A user’s security requirements are represented at multiple levels of abstraction as Intermediate Execution Environments. Using a sequence of configurations, a user’s security requirements are transformed from the abstract level to the tool level, possibly for multiple verification tools. Using a number of case studies, the validity of the framework is shown.

Software testing, one of the most important methods for quality assurance, has become too expensive and error prone for complex modern software systems. Test automation aims to reduce the costs of software testing and to improve its reliability. Despite advances in test automation, there are some domains for which automation seems to be difficult, for example, testing software to reveal the presence of security vulnerabilities, testing for conformance to security properties that traverse several functionalities of an application such as privacy policies, and testing asynchronous concurrent systems. Although there are research works that aim to solve the problems of test automation for these domains, there is still a gap between the practice and the state of the art. These works describe specific approaches that deal with particular problems, generally under restricted conditions. Nevertheless, individually, they have not made noticeable impact on the practice in test automation for these domains. Therefore, there is a need for an integrated framework that binds specific approaches together in order to provide more complete solutions. It is also important for this framework to show how current test automation efforts, tools and frameworks, can be reused. This thesis addresses this need by describing a general model-based testing framework and its specialisation for the testing domains of security vulnerabilities, privacy policies and asynchronous systems

Program verification is vital as more and more users are creating, downloading and executing foreign computer programs. Software verification tools provide a means for determining if a program adheres to a user’s security requirements, or security policy. There are many verification tools that exist for checking different types of policies on different types of programs. Currently however, there is no verification tool capable of determining if all types of programs satisfy all types of policies. This thesis describes a framework for supporting multiple verification tools to determine program satisfaction. A user’s security requirements are represented at multiple levels of abstraction as Intermediate Execution Environments. Using a sequence of configurations, a user’s security requirements are transformed from the abstract level to the tool level, possibly for multiple verification tools. Using a number of case studies, the validity of the framework is shown.

Master of Science / Department of Computing and Information Sciences / Daniel Andresen / Android balloon game application is an android application which helps in improving the children’s vocabulary power. This application provides a graphical user interface with words as questions and balloons as the options. The end user will have to select a balloon in order to select an answer. There are three modules in this application which are game mode, new game and high scores. In the basic module questions like Alpha_bet are included. Also as an enhancement, the game is made interesting by giving the user three lives to clear the levels of the game. Three small balloons are included in the application which resemble the three lives and once an incorrect answer is selected, the green balloon will be replaced by a red balloon depicting an incorrect answer. Also the scores will be computed for every correct option that is selected by the user. The score is incremented by ten points for every correct answer. And for the high score section, the game would maintain the list of top players. High score section will consist of the user’s name, score, time and date for the gameplay. Apart from that a next button is included which helps the user to skip a word which the user finds it difficult to answer. A hint option is also provided in the game which pronounces the word helping the user to guess the word correctly.

Master of Science / Department of Computing and Information Sciences / William Hsu / Bayesian networks are graphical models whose nodes represent random variables and whose edges represent conditional dependence between variables. Each node in a Bayesian network is equipped with a conditional probability function that expresses the likelihood that the node will take on different values given the values of its parents. A common task for a Bayesian network is to perform inference by computing the marginal probabilities of each possible value for each node. In this thesis, I introduce three new algorithms for approximate inference of Bayesian networks that use edge deletion techniques. The first reduces a network to its maximal weight spanning tree using the Kullback-Leibler information divergence as edge weights, and then runs Pearl’s algorithm on the resulting tree. Because Pearl’s algorithm can perform inference on a tree in linear time, as opposed to the exponential running time of all general exact inference algorithms, this reduction results in a tremendous speedup in inference. The second algorithm applies triangulation pre-processing rules that are guaranteed to be optimal if the original graph has a treewidth of four or less, and then deletes edges from the network and continues applying rules so that the resulting triangulated graph will have a maximum clique size of no more than five. The junction tree exact inference algorithm can then be run on the reduced triangulated graph. While the junction tree algorithm has an exponential worst-case running time in the size of the maximum clique in the triangulated graph, placing a bound on the clique size effectively places a polynomial time bound on the inference procedure. The third algorithm deletes edges from a triangulation of the original network until the maximum clique size in the triangulated graph is below a desired bound. Again, the junction tree algorithm can then be run on the resulting triangulated graph, and the bound on the maximum clique size will also polynomially bound the inference time. When tested for efficiency and accuracy on common Bayesian networks, these three algorithms perform up to 10,000 times faster than current exact and approximate techniques while achieving error values close to those of sampling techniques.

Master of Science / Department of Computing and Information Sciences / Daniel A. Andresen / The objective of this project is to build an e-commerce website using ASP.NET as well as J2EE technologies. Visual Studio 2005 provides a great IDE to build seamless front end layer for the websites with minimum effort. Hence, it is used to build the presentation layer. The business logic layer is developed in ASP.NET 2.0 and J2EE, exposing the functions as web services. Two similar clients have been developed in ASP.NET. These two clients invoke the .NET and J2EE web services. The two similar websites are subjected to testing for correctness and performance. Stress and load testing is performed thoroughly on the website. A detailed analysis of the results is done using the response times and throughputs from various tests. This report proves that we can build a website using a presentation tier developed in ASP.NET consuming any of the two technologies’ (ASP.NET & J2EE) web services. This proves to be very useful in scenarios where we need the best overall user experience regardless of the technology, to replace or extend an existing business tier by using a different technology.

Master of Science / Department of Computing and Information Sciences / David A. Gustafson / Current research involving vocal emotion detection has taken a variety of different approaches, and has found certain acoustic attributes to characterize different emotional states. While there have been improvements in classification over the past few years, computer classification is not nearly as accurate as human classification. This paper proposes the existence of an attribute that has not been examined, which can be used as a measure for detecting emotion in human vocal samples. It is shown that the new infrasonic attribute is significant when examining agitated emotions. Therefore, it can be used to help improve vocal emotion detection.

Master of Science / Department of Computing and Information Sciences / Gurdip Singh / Developing an optimal working environment and managing the of work load in an efficient manner are the major challenges for most businesses today. So, the importance of the workflow and workflow management in an organization is unquestionable. Many organizations use sophisticated systems to organize the workflows. One such workflow system based on a concise and powerful modeling language called “Yet Another Workflow Language” is YAWL. YAWL handles complex data, transformations, integration with organizational resources and Web Service integration. Workflow comprises of three main perspectives: control-flow, data and the resources. In Yawl, the control-flow and the data-flow are tightly coupled within the workflow enactment engine. But the resource perspective is provided by a discrete custom service called Resource Service. Administrative tools are provided using which the administrator has to manually select the resource (referred as participant) which needs to perform a particular task of the workflow. This project aims at developing a service which can automate the assignment of the tasks to the participants by using the Resource service which provides number of interfaces that expose the full functionality of the service. The application of this project with respect to Healthcare domain is presented. Healthcare domain is the one of the most demanding and yet critical business process. Hospitals face increasing pressure to both improve the quality of the services delivered to patients and to reduce costs .Hence there is significant demand on hospitals in regard to how the organization, execution, and monitoring of work processes is performed. Workflow Management Systems like YAWL offers a potential solution as they support processes by managing the flow of work.

Master of Science / Department of Computing and Information Sciences / Gurdip Singh / Ad hoc based routing protocol is a reactive protocol to route messages between mobile nodes. It allows nodes to pass messages through their neighbors to nodes which they cannot directly communicate. It uses Route Request (RREQ) and Route Reply (RREP) messages for communication. Wireless sensor networks consist of tiny sensor motes with capabilities of sensing, computation and wireless communication. This project aims to implement data collector application to collect the temperature data from the set of wireless sensor devices located within a building, which will help in gathering the information by finding the route with minimum number of hops to reach destination and generates low message traffic by not encouraging the duplicate message within the network. Using this application, wireless devices can communicate effectively to provide the network information to the user. This system consists of a mobile wireless sensor device called base station which is connected to a PC to communicate and is the root of the network. It also consists of set of client sensor devices which are present in different parts of the building. This project has been evaluated by determining how well the ad hoc protocol performs by measuring the number of messages and time consumed in learning about the complete topology. This application will eventually find the path with minimum number of hops. Simple Network Management Protocol (SNMP) is also used to monitor the sensor nodes remotely. This project was developed using nesC and C programming languages with TinyOS and UNIX based operating systems. It has been tested with a sufficient number of motes and evaluated based on the number of messages generated and number of hops traveled for each route request.

Master of Science / Department of Computing and Information Sciences / John M. Hatcliff / There are a number of network situations where different networks have different security policies and still need to share information. While it is important to allow some data to flow between the two networks, it is just as important that they don't share any data that violates the respective security policies of the networks. Constraints on data sharing are often phrased in terms of classification levels of data (e.g. top secret, secret, public). They might also be stated in terms of the contents of the data (e.g. are there military base names, is the location correct). The software and hardware that works to solve these problems is called Cross Domain Solutions (CDS). There are a variety of hardware platforms capable of implementing CDS. These platforms are all configured in different ways and they are often proprietary. Not only are there a number of platforms on the market, many are difficult to understand, verify, or even specify. The Guardol project provides an open, non-proprietary, and domain-specific language for specifying CDS security policies and implementing CDS. Guardol is designed to be easy to understand and verify. This thesis describes the design and implementation of primary Guardol components. It includes a description of the Eclipse GUI plug-ins that have been developed for the project as well as a description of new formal analyses and translations that have been developed for the language. The translation is used to plug into external tools for model checking and the analyses help to make the translation clean and efficient. The analyses are also useful tools to help make the use of Guardol easier for developers.