The growing use of computers in modern control systems has led to the develop- ment of complex dynamic systems known as hybrid systems, which integrates both discrete and continuous systems. Given that hybrid systems are systems that operates in real time allowing for changes in continuous state over time periods, and discrete state changes across zero time, their modelling, analysis and verification becomes very difficult. The formal verifications of such systems based on specifications that can guar- antee their behaviour is very important especially as it pertains to safety critical applications. Accordingly, addressing such verifications issues are important and is the focus of this thesis. In this thesis, in order to actualise the specification and verification of hybrid systems, Interval Temporal Logic(ITL) was adopted as the underlying formalism given its inherent characteristics of providing methods that are flexible for both propositional and first-order reasoning regarding periods found in hardware and software system’s descriptions. Given that an interval specifies the behaviour of a system, specifications of such systems are therefore represented as a set of intervals that can be used to gain an understanding of the possible behaviour of the system in terms of its composition whether in sequential or parallel form. ITL is a powerful tool that can handle both forms of composition given that it offers very strong and extensive proof and specification techniques to decipher essential system properties including safety, liveliness and time projections. However, a limitation of ITL is that the intervals within its framework are considered to be a sequence of discrete states. Against this back- drop, the current research provides an extension to ITL with the view to deal with verification and other related issues that centres around hybrid systems. The novelty within this new proposition is new logic termed SPLINE Interval Temporal Logic (SPITL) in which not only a discrete behaviour can be expressed, but also a continuous behaviour can be represented in the form of a spline i.e. the interval is considered to be a sequence of continuous phases instead of a sequence of discrete states. The syntax and semantics of the newly developed SPITL are provided in this thesis and the new extension of the interval temporal logic using a hybrid system as a case study. The overall framework adopted for the overall structure of SPITL is based on three fundamental steps namely the formal specification of hybrid systems is expressed in SPLINE Interval Temporal Logic, followed by the executable subset of ITL, called Tempura, which is used to develop and test a hybrid system specification that is written in SPITL and finally a runtime verification tool for ITL called AnaTempura which is linked with Matlab in order to use them as an integrated tool for the verification of hybrid systems specification. Overall, the current work contributes to the growing body of knowledge in hybrid systems based on the following three major milestones namely: i. the proposition of a new logic termed SPITL; ii. executable subset, Tempura, integrated with SPITL specification for hybrid systems; and iii. the development of a tool termed Ana Tempura which is integrated with Matlab to ensure accurate runtime verification of results.

Dynamic adaptivity of a computer system is its ability to modify the behavior according to the environment in which it is executed. It allows the system to achieve better performance, but usually requires specialized architecture and brings more complexity. The thesis presents an analysis and design of a framework that allows simple and fluent performance-based adaptive development at the level of functions and methods. It closely examines the API requirements and possibilities of integrating such a framework into the Scala programming language using its advanced syntactical constructs. On theoretical level, it deals with the problem of selecting the most appropriate function to execute with given input based on measurements of previous executions. In the provided framework implementation, the main stress is laid on modularity and extensibility, as many possible future extensions are outlined. The solution is evaluated on a variety of development scenarios, ranging from input adaptation of algorithms to environment adaptations of complex distributed computations in Apache Spark.

No description available.

No description available.

This work is focused on the design of an algorithm for run-time verification over requirements given as formulas in metric temporal logic (MTL). Tree structure is used for verification of these requirements, which is similar to run of alternating timed automata from which the final algorithm is derivated. Designed algorithm is able to verify given MTL formulas over the runs of a program without a need to remember the whole program's trace. This allows to monitor a given program on potentially infinite runs.

No description available.

This study introduces a dynamic approach to sorting, making use of predictions and data gathered during run-time to optimize the sorting of the current data set. This approach is used to develop a sorting algorithm called DynamicSort which partitions data and calculates a partial standard deviation for each partition to determine which of two sorting algorithms should be used to sort the partition. The algorithm is tested against Quicksort and radix sort on data sets of different sizes and standard deviation with the intent of finding advantages of the approach. In order to adapt to modern applications, the algorithm is tested in an environment utilizing parallel processing on multiple machines on data sets generated to mimic the characteristic size of big data. To accommodate this the data is divided at start and merged together after sorting using a k-way merge sort. While the tests conducted do not show any concrete gain in performance there are several factors that could be further optimized and evaluated. We find that it is not enough to simply consider the standard deviation in this approach. While no real instance of big data was used the algorithm was adapted for limited cache sizes and multiple hosts working in parallel.

No description available.

Adaptive computing systems have proven useful for implementing a wide range of algorithms. A limitation of current systems is the relatively small amount of reconfigurable hardware resources. Many algorithms require more hardware resources than are available. One solution to this problem is runtime reconfiguration (RTR). Using RTR techniques, a large algorithm is implemented as a collection of configurations for the reconfigurable hardware. These configurations are loaded onto the reconfigurable hardware as necessary to implement the algorithm. A primary limitation of RTR is that the reconfiguration process is slow. Therefore, methods of decreasing reconfiguration time are desirable. Another method of implementing large algorithms on small hardware is to use multiple configurable computing platforms connected via a communication network. RTR techniques can be used in conjunction with this method to further increase hardware availability. In this case reconfiguration time is increased by the overhead of transmitting data across the communication network. Methods of decreasing network overhead are desirable. This thesis discusses the use of caching techniques to decrease reconfiguration time. An architecture for caching configurations is implemented on a configurable computing system platform. The use of caching to decrease network overhead is discussed and exhibited. An example application is implemented and used to evaluate the effects of caching on reconfiguration time and algorithm performance. / Master of Science

The reprogrammable nature of configurable computing machines has led to a wealth of research in run-time reconfigurable systems and applications. A limitation often encountered in this research is the slow configuration time with respect to the system clock speed. One technique to deal with these configuration delays has been to develop devices that can hold multiple rapidly interchangeable configurations. This technique is known as context-switching. This thesis discusses the development of a framework to support applications which execute on a run-time reconfigurable system containing context-switching devices. The framework is divided into a number of layers: hardware, middleware, software, and applications. The design, implementation, and details of each layer are presented. / Master of Science