Permanent URI for this collection
Browse
Recent Submissions
Publication Verification of the diagnosability of discrete-event systems in waters(Working Paper, Department of Computer Science, The University of Waikato, 2018-11-21) McGrath, NicholasThe task of detecting faults and reacting to them appropriately is a crucial aspect of a building a stable system. If a fault cannot be directly observed, its occurrence must be inferred from what can be observed. In the realm of discrete-event systems, the property of diagnosability has been defined, and several algorithms for testing diagnosability have been presented. Diagnosability relates to the ability for all possible faults to be correctly detected or inferred within a finite amount of time from their occurrence. WATERS (Waikato Analysis Toolkit for Events in Reactive Systems) is a software toolkit for the creation and analysis of discrete-event systems. In this report pre-existing existing algorithms for the verification of diagnosability and the implementation of one of these algorithms into WATERS are discussed. The created implementation can verify the diagnosability of a discrete-event system in polynomial time with respect to its state space and provide a counterexample if the discrete-event system was found to be not diagnosable.Publication Using augmented reality to enhance children’s books(Working Paper, Department of Computer Science, The University of Waikato, 2018) Vanderschantz, Nicholas; Hinze, Annika; AL-Hashami, AyshaThis paper reports a case study on using Augmented Reality in children's books in which we explored the use of various types of interactions at different levels. The paper describes the design process and the insights gained through investigations into the requirements for enhancing children’s books with Augmented Reality. Using evidence from the literature along with our own observations, an interaction design model and resulting interface design are developed to explore interactivity in printed books using Augmented Reality. We report on an expert walk-through and discuss possible improvements and implications from our case study.Publication Framework and proofs for synthesis of least restrictive controllable supervisors for extended finite-state machines with variable abstraction(Working Paper, Department of Computer Science, The University of Waikato, 2018) Malik, Robi; Teixeira, MarceloThis working paper presents an algorithm that combines modular synthesis for extended finite-state machines (EFSM) with abstraction of variables by symbolic manipulation, in order to compute least restrictive controllable supervisors. Given a modular EFSM system consisting of several components, the proposed algorithm synthesises a separate supervisor for each specification component. To synthesise each supervisor, the algorithm iteratively selects components (plants and variables) from a synchronous composition until a least restrictive controllable solution is obtained. This improves on previous results of the authors where abstraction is only performed by the selection of components and not variables. The working paper explains the theory of EFSM synthesis and abstraction and includes formal proofs of all results. An example of a flexible manufacturing system illustrates how the proposed algorithm works to compute a modular supervisor.Publication The explicit conflict check algorithm implemented in the Waters library(Working Paper, Department of Computer Science, The University of Waikato, 2018) Malik, RobiThis working paper describes the implementation of explicit model checking algorithms to verify the nonblocking or nonconflicting property of discrete event systems. Explicit algorithms enumerate and store all reachable states of a synchronous composition. Three alternatives optimised for memory consumption or runtime are described and compared. The algorithms have been implemented in C++ in the discrete event systems library Waters, and experimental results show that they can explore more than 100 million states on standard computers.