Working Paper Series index
S. Mohajerani, R. Malik and M. Fabian
This working paper describes a framework for compositional nonblocking verification of reactive systems modelled as extended finite-state machines. The nonblocking property can capture the absence of livelocks and deadlocks in concurrent systems. Compositional verification is shown in previous work to be effective to verify this property for large discrete event systems. Here, these results are applied to extended finite-state machines communicating via shared memory. The model to be verified is composed gradually, simplifying components through abstraction at each step, while conflict equivalence guarantees that the final verification result is the same as it would have been for the non-abstracted model. The working paper concludes with an example showing the potential of compositional verification to achieve substantial state-space reduction.
S. J. Cunningham, H. Alqurashi, A. Hinze, N. Vanderschantz, C. Timpany and R. Heese
Library users should be conveniently interact with collections and be able to easily choose books of interest as they explore and browse a physical book collection. While there exists a growing body of naturalistic studies of browsing and book selection in digital collections, the corresponding literature on behaviour in the physical stacks is surprisingly sparse. We add to this literature in this paper, by conducting observations of patrons in a university library as they selected books from the shelves. Our aim is to further our understanding of patterns of behaviour in browsing and selection in physical collections.
F. Reinhart, K. Schlieper, M. Kugler, E. André, M. Masoodian and B. Rogers
There is considerable global effort being made towards identifying ways of reducing energy consumption to cope with growing demands. Although there is potential for energy saving in many sectors, our focus is on reducing energy consumption in residential homes. We have developed a system which combines home automation and energy usage monitoring technologies. The system offers a range of tools designed for mobile devices to assist users with monitoring their energy usage and provides mechanisms for setting up and controlling home appliances to conserve energy. In this paper we describe our system and a user study we have conducted to evaluate its effectiveness. The findings of the study show the potential benefits of this type of mobile technology.
M. D. Apperley and M. M. Alahmari
The growing importance of batteries in the delivery of primary energy, for example in electric vehicles and isolated off-grid electricity systems, has added weight to the demand for simple and reliable measures of a battery’s remaining stored energy at any time. Many approaches to estimating this battery state-of-charge exist, ranging from those based on a full appreciation of the chemistry and physics of the storage and delivery mechanisms used, and requiring extensive data on which to base an estimate, to the naïve and simple, based only, for example, on the terminal voltage of the battery. None, however, is perfect, and able to deliver a simple percentage-full figure, as in a fuel gauge. The shortcomings are due to a range of complicating factors, including the impact of rate of charge, rate of discharge, battery aging, and temperature, to name just some of these.
This paper presents a simple yet effective method for tracking state-of-charge in an off-grid electricity system, where batteries are in continuous use, preventing static parameter measurements, and where charge/discharge cycles do not necessarily follow an orderly sequence or pattern. A reliable indication of state-of-charge is, however, highly desirable, but need be only of fuel gauge precision, say to the nearest 12-20%. The algorithm described utilises knowledge of the past, and constantly adapts parameters such as charge efficiency and total charge capacity based on this knowledge, and on the occurrence of specific identifiable events such as zero or full charge.
J. G. Cleary, M. Utting and R. Clayton
It is proposed that Normal Logic Programs with an explicit time ordering are a suitable basis for a general purpose parallel programming language. Examples show that such a language can accept real-time external inputs and outputs, and mimic assignment, all without departing from its pure logical semantics. This paper describes a fully incremental bottom-up interpreter that supports a wide range of parallel execution strategies and can extract signicant potential parallelism from programs with complex dependencies.
M. Utting, M.-H. Weng and J. G. Cleary
This paper introduces the JStar parallel programming language, which is a Java-based declarative language aimed at discouraging sequential programming, encouraging massively parallel programming, and giving the compiler and runtime maximum freedom to try alternative parallelisation strategies. We describe the execution semantics and runtime support of the language, several optimisations and parallelism strategies, with some benchmark results.
This report proposes to improve compositional nonblocking verification through the use of two special event types: always enabled and selfloop-only events. Compositional verification involves abstraction to simplify parts of a system during verification. Normally, this abstraction is based on the set of events not used in the remainder of the system. Here, it is proposed to exploit more knowledge about the system and abstract events even though they are used in the remainder of the system. This can lead to more simplification than was previously possible. Abstraction rules from previous work are extended to respect the new special events and proofs show these rules still preserve nonblocking. The rules have been implemented in Waters and experimental results demonstrate that these extended simplification rules help verify several industrial-scale discrete event system models while achieving better state-space reduction than before.
M. Apperley and B. Rogers
This paper presents a modified computer mouse, the Ori-enting Mouse, which delivers orientation as an additional dimension of input; when the mouse is moved on a flat surface it reports, in addition to the conventional x, y translation, angular rotation of the device in the x, y plane.
The orienting mouse preserves important properties of the standard mouse; all measurements are relative and movement is tracked only while the mouse is on its flat surface. If the user lets go of the mouse, leaving it on the surface, its position and orientation do not change until it is touched again. Picking the mouse up and putting it down in a different orientation leaves the angle and posi-tion unchanged.
While the concept of sensing mouse rotation is not new, our work focuses on movement and navigation in 3D, rather than on precision positioning tasks. We describe a number of sample applications developed to test its ef-fectiveness in this context. Specific features exploited and described include (i) an algorithm for calculating the mouse angle which cancels drift between the two sensors, and (ii) the use of angular gearing which avoids unnatural and uncomfortable hand positions when moving through large angles; informal user testing validates this idea.
A. C. Zaicu and A. Hinze
In this project we use an electronic rabbit called Karotz, created by French company Violet. The rabbits have the ability to connect autonomously to a WI-FI network. IN this project we use Karotz to record an audio log that will contain sounds of the environment. We also programmed a way for the rabbit to send audio to its other Karotz friend. We explored if Karotz can be used to help people stay in contact with each other and to feel less homesick.
M. Fowke, A. Hinze and R. Heese
This report covers the implementation of software that aims to identify document versions and se-mantically related documents. This is important due to the increasing amount of digital information. Key criteria were that the software was fast and required limited disk space. Previous research de-termined that the Simhash algorithm was the most appropriate for this application so this method was implemented. The structure of each component was well defined with the inputs and outputs constant and the result was a software system that can have interchangeable parts if required.
M. Fowke, A. Hinze and R. Heese
Document classification and provenance has become an important area of computer science as the amount of digital information is growing significantly. Organisations are storing documents on computers rather than in paper form. Software is now required that will show the similarities between documents (i.e. document classification) and to point out duplicates and possibly the history of each document (i.e. provenance). Poor organisation is common and leads to situations like above. There exists a number of software solutions in this area designed to make document organisation as simple as possible. I'm doing my project with Pingar who are a company based in Auckland who aim to help organise the growing amount of unstructured digital data. This reports analyses the existing literature in this area with the aim to determine what already exists and how my project will be different from existing solutions.
M. Fowke, A. Hinze and R. Heese
This research looks at the most appropriate similarity measure to use for a document classification problem. The goal is to find a method that is accurate in finding both semantically and version related documents. A necessary requirement is that the method is efficient in its speed and disk usage. Simhash is found to be the measure best suited to the application and it can be combined with other software to increase the accuracy. Pingar have provided an API that will extract the entities from a document and create a taxonomy displaying the relationships and this extra information can be used to accurately classify input documents. Two algorithms are designed incorporating the Pingar API and then finally an efficient comparison algorithm is introduced to cut down the comparisons required.
J. Bellamy and A. Hinze
This report goes over and details the progress of the 2013 COMP477 project “Augmenting Memory: The Digital Parrot on Mobile Devices” undertaken by Jake Bellamy and supervised by Annika Hinze at the University of Waikato.
The report begins with an overview on the problem with remembering events in people’s lives and details the background information on the Digital Parrot system. It also describes the previous project that preceded this one, which began to conceptualize the Digital Parrot on mobile devices. It analyses problems with the current design of the system and addresses them.
The report then goes on to conduct an in depth user study with the functioning version of the software. The user study finds design flaws and incorrect functionality in the application that would not have otherwise been apparent.
Finally, the report concludes with a proposed user interface concept that addresses all of the issues found in the user study and describes how the system would work. It describes the initial implementation that has begun in building this system.
Working Paper Series index