School of Information Technology and Electrical Engineering Publications - UQ eSpace
http://espace.library.uq.edu.au/
The University of QueenslandenFez http://blogs.law.harvard.edu/tech/rssA face biometric benchmarking review and characterisation
http://espace.library.uq.edu.au/view/UQ:272233
In order to advance face recognition research, algorithm performance has to be measured and compared using a range of metrics and operating characteristics. While public challenges such as the NIST-sponsored FERET, FRVT, FRGC, and MBGC are helpful to gauge comparative performance and improvement for a particular scenario, they typically are not sufﬁcient to fully characterise the strengths and weaknesses of the face recognition algorithm, thus researchers need to do additionally benchmarking independently. This paper provides: (1) a detailed review and categorisation of publicly available face biometrics benchmarks; (2) a discussion of metrics and performance factors to consider; (3) a proposal for a meta-face biometric benchmarking regime which suggests guidelines for benchmarking across multiple datasets to more fully characterise and quantify face recognition performance across various operating characteristics; and (4) a sample demonstration which compare the performance of a face recognition algorithm before and after inclusion of a face quality metric.2012-04-04T10:15:44Z
Mau, Sandra; Dadgostar, Farhad; Cullinan, Ian; Bigdeli, Abbas; Lovell, Brian C. A Family of Defeasible Reasoning Logics and its Implementation
http://espace.library.uq.edu.au/view/UQ:9696
Defeasible reasoning is a direction in nonmonotonic reasoning that is based on the use of rules that may be defeated by other rules. It is a simple, but often more efficient approach than other nonmonotonic reasoning systems. This paper presents a family of defeasible reasoning formalisms built around Nute's defeasible logic. We describe the motivations of these formalisms and derive some basic properties and interrelationships. We also describe a query answering system that supports these formalisms and is available on the World Wide Web.2005-03-21T00:00:00Z
Antoniou, Grigoris; Billington, David; Governatori, Guido; Maher, Michael J.; Rock, Andrew A family of non-quasiprimitive graphs admitting a quasiprimitive 2-arc transitive group action
http://espace.library.uq.edu.au/view/UQ:143770
Let Gamma be a simple graph and let G be a group of automorphisms of Gamma. The graph is (G, 2)-arc transitive if G is transitive on the set of the 2-arcs of Gamma. In this paper we construct a new family of (PSU(3, q(2)), 2)-arc transitive graphs r of valency 9 such that Aut Gamma = Z(3).G, for some almost simple group G with socle PSU(3, q(2)). This gives a new infinite family of non-quasiprimitive almost simple graphs. (C) 1999 Academic Press.2008-06-10T14:36:20Z
Fang, XG; Havas, G; Wang, J A family of perfect hashing methods
http://espace.library.uq.edu.au/view/UQ:57372
Minimal perfect hash functions are used for memory efficient storage and fast retrieval of items from static sets. We present an infinite family of efficient and practical algorithms for generating order preserving minimal perfect hash functions. We show that almost all members of the family construct space and time optimal order preserving minimal perfect hash functions, and we identify the one with minimum constants. Members of the family generate a hash function in two steps. First a special kind of function into an r-graph is computed probabilistically. Then this function is refined deterministically to a minimal perfect hash function. We give strong theoretical evidence that the first step uses linear random time. The second step runs in linear deterministic time. The family not only has theoretical importance, but also offers the fastest known method for generating perfect hash functions.2007-08-13T16:35:53Z
Majewski, BS; Wormald, NC; Havas, G; Czech, ZJ A fast and adaptive method for estimating UAV attitude from the visual horizon
http://espace.library.uq.edu.au/view/UQ:256339
This study describes a novel method for automatically obtaining the attitude of an aircraft from the visual horizon. A wide-angle view of the environment, including the visual horizon, is captured and the input images are classified into fuzzy sky and ground regions using the spectral and intensity properties of the pixels. The classifier is updated continuously using an online reinforcement strategy and is therefore able to adapt to the changing appearance of the sky and ground, without requiring prior training offline. A novel approach to obtaining the attitude of the aircraft from the classified images is described, which is reliable, accurate, and computationally efficient to implement. This method is therefore suited to real-time operation and we present results from flight tests that demonstrate the ability of this vision-based approach to outperform an inexpensive inertial system.2011-10-17T11:34:40Z
Moore, Richard J. D.; Thurrowgood, Saul; Bland, Daniel; Soccol, Dean; Srinivasan, Mandyam V. A Fast and Practical Imaging Scheme for a Rotating RF Coil at 9.4T by Using Ultra-Short TE Sequence in Radial Trajectory, Investigation of acoustic noise reduction method for MRI-LINAC hybrid system
http://espace.library.uq.edu.au/view/UQ:377189
2016-01-18T11:57:02Z
Li, M. Hugger; Weber, E.; Jin, J.; Liu, F.; Ullman, P.; Stark, S.; Tesiram, Y.; Yang, Y.; Junge, S. A fast computational neural network for economic load dispatch
http://espace.library.uq.edu.au/view/UQ:188993
2009-12-03T12:34:09Z
Sode-Yome. Arthit; Kwang, Y. Lee; Mithulananthan, Nadarajah A fast multi-resolution differential evolution method for multimodal image registration
http://espace.library.uq.edu.au/view/UQ:293494
A new method of finding optimal variables using self-adaptive differential evolution derived multi-modal image registration is proposed. The method features multi-resolution images achieved through down-sampling at different stages of the transformation model variable optimization process. The performance of the method is illustrated by registering magnetic resonance images to histological sections. We provide an investigation of the impact of the down-sampling factor and convergence criteria. Our findings show that given appropriately down-sampled images, and by using the proposed approach, it is possible to find optimal registration transformation model variables faster than if appropriate down-sampling is not used.2013-03-12T14:34:07Z
Yang, Zhengyi; Vegh, Viktor; Reutens, David A fast number theoretic finite radon transform
http://espace.library.uq.edu.au/view/UQ:326020
This paper presents a new fast method to map between images and their digital projections based on the Number Theoretic Transform (NTT) and the Finite Radon Transform (FRT). The FRT is a Discrete Radon Transform (DRT) defined on the same finite geometry as the Finite or Discrete Fourier Transform (DFT). Consequently, it may be inverted directly and exactly via the Fast Fourier Transform (FFT) without any interpolation or filtering [1]. As with the FFT, the FRT can be adapted to square images of arbitrary sizes such as dyadic images, prime-adic images and arbitrary-sized images. However, its simplest form is that of prime-sized images [2]. The FRT also preserves the discrete versions of both the Fourier Slice Theorem (FST) and Convolution Property of the Radon Transform (RT). The NTT is also defined on the same geometry as the DFT and preserves the Circular Convolution Property (CCP) of the DFT [3, 4]. This paper shows that the Slice Theorem is also valid within the NTT and that it can be utilized as a new exact, integer-only and fast inversion scheme for the FRT, with the same computational complexity as the FFT. Digital convolutions and exact digital filtering of projections can also be performed using this Number Theoretic FRT (NFRT).2014-03-19T11:08:38Z
Chandra, S.; Svalbe, I. A fast parallel imaging rotary phased array head coil with improved sensitivity profile deep in the center of the brain
http://espace.library.uq.edu.au/view/UQ:135168
A new class of a receive-only 2 T 4-element rotary phased array head coil has been proposed for MRI brain imaging applications. Coil elements of the rotary phased array head coil have "paddle-like" structures consisting of a pair of main conductors located on opposite sides, inserted equi-angularly around and over the head. Using such a unique design, the proposed rotary head coil can improve the sensitivity deep at the centre of the brain and produces highly homogeneous brain images. The rotary phased array head coil is numerically modeled using a hybrid MoM/FEM method and a prototype was constructed accordingly. In vivo MR brain imaging using the prototype rotary phased array head coil has been undertaken and the acquired brain images show high homogeneity as anticipated. In addition, parallel imaging, VD-GRAPPA, is used in conjunction with the rotary phased array head coil to enable rapid imaging.2008-04-11T16:47:15Z
Weber, E.; Li, B. K.; Liu, F.; Crozier, S. A fast, segmentation-free, method for constructing a biomechanical model of the breast from DCE-MRI data
http://espace.library.uq.edu.au/view/UQ:176465
This paper presents a method for constructing a biomechanical breast model which does not require an initial time- and labour-intensive segmentation of the breast tissue. This is achieved by mapping voxel intensity and enhancement levels directly to Youngpsilas modulus values characteristic of the respective tissues. We demonstrate this new method by incorporating it into a biomechanically based registration evaluation framework, which produces qualitatively the same results as a segmentation based model.2009-04-16T19:56:59Z
Hill, A.; Mehnert, A.; Crozier, S. A FDTD analysis to investigate capabilities of an UWB radar for breast tumor detection
http://espace.library.uq.edu.au/view/UQ:103870
2007-08-23T21:53:32Z
Wang, Hua; Bialkowski, Marek E.; Liu, Feng; Crozier, Stuart A FDTD model for the calculation of gradient-induced eddy currents in MRI magnets
http://espace.library.uq.edu.au/view/UQ:100524
2007-08-23T19:32:50Z
Liu, F.; Crozier, S. A feasibility study to investigate the use of oximetry and dual RIP bands for pre-PSG screening of OSA in children
http://espace.library.uq.edu.au/view/UQ:234974
2011-03-11T12:27:02Z
Iyer, K.; Mason, D.G.; Suresh, S.; Terrill, P.I.; Wilson, S.J. Affective Web Service Design
http://espace.library.uq.edu.au/view/UQ:8055
In this paper, we propose that, in order to improve customer satisfaction, we need to incorporate communication modes (e.g., speech act) in the current standards of web services specifications. We show that with the communication modes, we can estimate various affects on service consumers during their interactions with web services. With this information, a web-service management system can automatically prevent and compensate potential negative affects, and even take advantage of positive affect.2006-07-28T00:00:00Z
Song, I.; Governatori, G. A Fibred Tableau Calculus for BDI Logics
http://espace.library.uq.edu.au/view/UQ:8554
In [12,16] we showed how to combine propositional BDI logics using Gabbay's fibring methodology. In this paper we extend the above mentioned works by providing a tableau-based decision procedure for the combined/fibred logics. To achieve this end we first outline with an example two types of tableau systems, (graph and path), and discuss why both are inadequate in the case of fibring. Having done that we show how to uniformly construct a tableau calculus for the combined logic using Governatori's labelled tableau system KEM.2006-03-20T00:00:00Z
Padmanabhan, Vineet; Governatori, Guido A Fibred Tableau Calculus for Modal Logics of Agents
http://espace.library.uq.edu.au/view/UQ:13298
In previous works we showed how to combine propositional multimodal logics using Gabbay's \emph{fibring} methodology. In this paper we extend the above mentioned works by providing a tableau-based proof technique for the combined/fibred logics. To achieve this end we first make a comparison between two types of tableau proof systems, (\emph{graph} $\&$ \emph{path}), with the help of a scenario (The Friend's Puzzle). Having done that we show how to uniformly construct a tableau calculus for the combined logic using Governatori's labelled tableau system \KEM. We conclude with a discussion on \KEM's features.2007-04-02T16:05:12Z
Padmanabhan, V.; Governatori, G A field study of aging in paper-oil insulation systems
http://espace.library.uq.edu.au/view/UQ:309767
The paper used to insulate the windings of power transformers is mostly made from wood pulp, a cellulosic material. Over decades the paper is slowly attacked by water, oxygen, oil acids, and high temperatures and eventually degrades to the point where it is no longer an effective insulator. The transformer is then likely to fail. Power utilities need to know when a transformer is nearing the end of its useful life in order to plan its replacement. However, a problem with monitoring the condition of the paper within a transformer is that it may be difficult to obtain a sample to test. Furthermore, a particular sample may not accurately reflect the overall paper condition. A power transformer operating in Australia failed in 2010. Thus we had the opportunity to study the paper condition at various points within the transformer and evaluate the validity of the current understanding of paper aging. In this article we discuss the mechanisms of cellulose degradation, and the associated equations, and apply them to the paper insulation in the failed transformer.2013-09-20T09:00:43Z
Lelekakis, Nick; Guo, Wenyu; Martin, Daniel; Wijaya, Jaury; Susa, Dejan A field study of two online dry-out methods for power transformers
http://espace.library.uq.edu.au/view/UQ:309772
Dry-out methods for transformers, using cellulose cartridges and molecular sieves, were compared. The latter are preferable for keeping a dry transformer dry, whereas the former are more efficient in drying a wet transformer. In this article, we compare the effectiveness of the cellulose cartridge filter and molecular sieve methods. Two identical transformers with similar insulation wetness were used. We estimated the water content of the paper (WCP) insulation from (1) the water activity of the oil, (2) the dielectric response of the transformer, and (3) the water content of individual paper samples determined by Karl Fischer titration. We also measured the acid number of the oil, its interfacial tension, dielectric strength, furan content, dissolved gas content, and particle count.2013-09-20T09:10:58Z
Lelekakis, Nick; Martin, Daniel; Guo, Wenyu; Wijaya, Jaury; Lee, Meng A finite-difference method for the design of biplanar transverse gradient coil in MRI
http://espace.library.uq.edu.au/view/UQ:240832
This paper presents a finite difference method for the design of gradient coil in MRI. In this method, a linear matrix equation is formulated using a finite-difference approximation of the current density in the source domain and an optimization procedure is then carried out to solve the resulting inverse problem and the coil winding pattern are found. The developed algorithm is tested with a transverse biplanar gradient coil design example. Compared with conventional design methods such as target-field, standard stream function or boundary element schemes, the new design approach is relatively easy to implement and flexible to manage the local winding pattern for 2D or 3D geometries.2011-05-13T18:24:57Z
Zhu, Minhua; Shou, Guofa; Xia, Ling; Li, Xia; Liu, Feng; Crozier, Stuart A finite difference method for the design of gradient coils in MRI-an initial framework
http://espace.library.uq.edu.au/view/UQ:287792
2012-12-23T00:49:20Z
Zhu, Minhua; Xia, Ling; Liu, Feng; Zhu, Jianfeng; Kang, Liyi; Crozier, Stuart A finite element model for the analysis of steady state heat transfer in disc coil transformer winding
http://espace.library.uq.edu.au/view/UQ:309782
A general formulation for the analysis of the steady state heat transfer was developed and implemented in MATLAB, to become part of a coupled thermal-hydraulic model for solving the temperature and fluid flow distributions in a disc coil transformer winding. It uses Finite Element Method and computes temperature distributions in the solid part of the disc coil, i.e. in conductors and insulating paper. The model takes non-uniform heat generation rate and convective boundary conditions for solving the heat conduction problem. Axisymmetry of the coil geometry is used to reduce the problem to two-dimensions. The FEM code developed was validated by comparing computation results with those obtained from COMSOL Multiphysics software. As demonstrated, the results were in very good agreement with one another.2013-09-20T09:40:28Z
Wijaya, Jaury; Czaszejko, Tadeusz; Lelekakis, Nick; Martin, Daniel; Susa, Dejan A First Order Predicate Logic Formulation of the 3D Reconstruction Problem and its Solution Space
http://espace.library.uq.edu.au/view/UQ:77939
This paper defines the 3D reconstruction problem as the process of reconstructing a 3D scene from numerous 2D visual images of that scene. It is well known that this problem is ill-posed, and numerous constraints and assumptions are used in 3D reconstruction algorithms in order to reduce the solution space. Unfortunately, most constraints only work in a certain range of situations and often constraints are built into the most fundamental methods (e.g. Area Based Matching assumes that all the pixels in the window belong to the same object). This paper presents a novel formulation of the 3D reconstruction problem, using a voxel framework and first order logic equations, which does not contain any additional constraints or assumptions. Solving this formulation for a set of input images gives all the possible solutions for that set, rather than picking a solution that is deemed most likely. Using this formulation, this paper studies the problem of uniqueness in 3D reconstruction and how the solution space changes for different configurations of input images. It is found that it is not possible to guarantee a unique solution, no matter how many images are taken of the scene, their orientation or even how much color variation is in the scene itself. Results of using the formulation to reconstruct a few small voxel spaces are also presented. They show that the number of solutions is extremely large for even very small voxel spaces (5 x 5 voxel space gives 10 to 10(7) solutions). This shows the need for constraints to reduce the solution space to a reasonable size. Finally, it is noted that because of the discrete nature of the formulation, the solution space size can be easily calculated, making the formulation a useful tool to numerically evaluate the usefulness of any constraints that are added.2007-08-15T07:24:25Z
Robinson, M.; Kubik, K.; Lovell, B. A Flexible Framework For Defeasible Logics
http://espace.library.uq.edu.au/view/UQ:9694
Logics for knowledge representation suffer from over-specialization: while each logic may provide an ideal representation formalism for some problems, it is less than optimal for others. A solution to this problem is to choose from several logics and, when necessary, combine the representations. In general, such an approach results in a very difficult problem of combination. However, if we can choose the logics from a uniform framework then the problem of combining them is greatly simplified. In this paper, we develop such a framework for defeasible logics. It supports all defeasible logics that satisfy a strong negation principle. We use logic meta-programs as the basis for the framework.2005-03-23T00:00:00Z
Antoniou, Grigoris; Billington, David; Governatori, Guido; Maher, Michael J. A Flexible Framework For Defeasible Logics
http://espace.library.uq.edu.au/view/UQ:9695
Logics for knowledge representation suffer from over-specialization: while each logic may provide an ideal representation formalism for some problems, it is less than optimal for others. A solution to this problem is to choose from several logics and, when necessary, combine the representations. In general, such an approach results in a very difficult problem of combination. However, if we can choose the logics from a uniform framework then the problem of combining them is greatly simplified. In this paper, we develop such a framework for defeasible logics. It supports all defeasible logics that satisfy a strong negation principle. We use logic meta-programs as the basis for the framework.2005-03-21T00:00:00Z
Antoniou, Grigoris; Billington, David; Governatori, Guido; Maher, Michael J. A flexible method for rapid force computation in elliptical magnets
http://espace.library.uq.edu.au/view/UQ:60950
The design of open-access elliptical cross-section magnet systems has recently come under consideration. Obtaining values for the forces generated within these unusual magnets is important to progress the designs towards feasible instruments. This paper presents a novel and flexible method for the rapid computation of forces within elliptical magnets. The method is demonstrated by the analysis of a clinical magnetic resonance imaging magnet of elliptical cross-section and open design. The analysis reveals the non-symmetric nature of the generated Maxwell forces, which are an important consideration, particularly in the design of superconducting systems.2007-08-14T16:53:06Z
Snape-Jenkinson, C. J.; Crozier, S.; Forbes, L. K. A flexible multiplacation unit for an FPGA logic block
http://espace.library.uq.edu.au/view/UQ:96162
2007-08-24T00:17:39Z
Rajagopalan, K.; Sutton, P. R. A folded-monopole model for electrically small NRI-TL metamaterial antennas
http://espace.library.uq.edu.au/view/UQ:262770
2011-12-02T16:21:34Z
Antoniades, M. A.; Eleftheriades, G. V. A folded quarter-elliptical wideband antenna for portable devices
http://espace.library.uq.edu.au/view/UQ:231166
In the last decade, compact low-profile antennas featuring multiband operation have drawn a considerable interest from designers of portable wireless devices. The demand for these antennas stems from the fact that modern portable devices have to access an increased number of wireless services across the frequency spectrum from approximately 880MHz to 5850MHz.2011-03-04T13:43:27Z
Bialkowski, Marek E.; Razali, Ahmad Rashidy; Boldaji, Ashkan A Formal Analysis of a Business Contract Language
http://espace.library.uq.edu.au/view/UQ:8412
This paper presents a formal system for reasoning about violations of obligations in contracts. The system is based on the formalism for the representation of contrary-to-duty obligations. These are the obligations that take place when other obligations are violated as typically applied to penalties in contracts. The paper shows how this formalism can be mapped onto the key policy concepts of a contract specification language, called Business Contract Language (BCL), previously developed to express contract conditions for run time contract monitoring. The aim of this mapping is to establish a formal underpinning for this key subset of BCL.2006-05-16T00:00:00Z
Governatori, Guido; Milosevic, Zoran A Formal Approach to Negotiating Agents Development
http://espace.library.uq.edu.au/view/UQ:9607
This paper presents a formal and executable approach to capture the behaviour of parties involved in a negotiation. A party is modeled as a negotiating agent composed of a communication module, a control module, a reasoning module, and a knowledge base. The control module is expressed as a statechart, and the reasoning module as a defeasible logic program. A strategy specification therefore consists of a statechart, a set of defeasible rules, and a set of initial facts. Such a specification can be dynamically plugged into an agent shell incorporating a statechart interpreter and a defeasible logic inference engine, in order to yield an agent capable of participating in a given type of negotiations. The choice of statecharts and defeasible logic with respect to other formalisms is justified against a set of desirable criteria, and their suitability is illustrated through concrete examples of bidding and multi-lateral bargaining scenarios.2005-04-11T00:00:00Z
Dumas, Marlon; Governatori, Guido; ter Hofstede, Arthur H. M; Oaks, Philippa A Formal Approach To Protocols And Strategies For (Legal) Negotiation
http://espace.library.uq.edu.au/view/UQ:9619
We propose a formal and executable framework for expressing protocols and strategies for automated (legal) negotiation. In this framework a party involved in a negotiation is represented through a software agent composed of four modules: (i) a communication module which manages the interaction with the other agents; (ii) a control module; (iii) a reasoning module specified as a defeasible theory; and (iv) a knowledge base which bridges the control and the reasoning modules, while keeping track of past decisions and interactions. The choice of defeasible logic is justified against a set of desirable criteria for negotiation automation languages. Moreover, the suitability of the framework is illustrated through two case studies.2005-04-11T00:00:00Z
Governatori, Guido; Dumas, Marlon; ter Hofstede, Arthur H. M; Oaks, Philippa A formal basis for a program compilation proof tool
http://espace.library.uq.edu.au/view/UQ:83960
2007-08-14T13:23:59Z
Wildman, L. P. A Formal Basis for a Program Compilation Proof Tool
http://espace.library.uq.edu.au/view/UQ:2473
This paper presents a case study in verified program compilation from high-level language programs to assembler code using the Cogito formal development system. A form of window-inference based on the Z schema is used to perform the compilation. Data-refinement is used to change the representation of integer variables to assembler word locations.2006-04-11T17:21:35Z
Wildman, Luke A formal denotational semantics of UML in object-z
http://espace.library.uq.edu.au/view/UQ:59394
2007-08-14T15:46:03Z
Kim, S.; Carrington, D. A. A formal development approach for self-organising systems
http://espace.library.uq.edu.au/view/UQ:352734
2015-03-02T09:43:13Z
Li, Q.; Smith, G. A formal framework for modelling and analysing mobile systems
http://espace.library.uq.edu.au/view/UQ:100426
This paper presents a formal framework for modelling and analysing mobile systems. The framework comprises a collection of models of the dominant design paradigms which are readily extended to incorporate details of particular technologies, i.e., programming languages and their run-time support, and applications. The modelling language is Object-Z, an extension of the well-known Z specification language with explicit support for object-oriented concepts. Its support for object orientation makes Object-Z particularly suited to our task. The system structuring techniques offered by object-orientation are well suited to modelling mobile systems. In addition, inheritance and polymorphism allow us to exploit commonalities in mobile systems by defining more complex models in terms of simpler ones.2007-08-23T19:28:48Z
Smith, G. P. A formalism to describe design patterns based on role concepts
http://espace.library.uq.edu.au/view/UQ:203993
Design patterns are typically defined imprecisely using natural language descriptions with graphical annotations. It is also common to describe patterns using a concrete design example with implementation details. Several approaches have been proposed to describe design patterns abstractly based on role concepts. However, the notion of role differs in each approach. The behavioral aspects of patterns are not addressed in the role-based approaches. This paper presents a rigorous approach to describe design patterns based on role concepts.Adopting metamodeling and formalism, our work defines an innovative framework where generic pattern concepts based on roles are precisely defined as a formal role metamodel using Object-Z. Individual patterns are specified using these generic role concepts in terms of pattern role models. Temporal behaviors of patterns are also specified using Object-Z and integrated in the pattern role models. Patterns described this way are abstract, separating pattern realization information from the pattern description. They are also precise providing a rigorous foundation for reasoning about pattern properties. This paper also formalizes the properties that must be captured in a class model when a design pattern is deployed. These properties are defined generically in terms of role bindings from a pattern role model to a class model. They provide a precise basis for checking the validity of pattern utilisation in designs. Our work is supported by tools. We have developed an initial role metamodel using an existing modeling framework, Eclipse Modeling Framework (EMF) and have transformed the metamodel to Object-Z using model transformation techniques. Complex constraints are added to the transformed Object-Z model. More importantly, we implement the role metamodel. Using this implementation, pattern authors can develop an initial pattern role model in the same modeling framework and convert the initial model to Object-Z using our transformation rules. The transformed Object-Z model is then enhanced with behavioral features of the pattern. This tool support significantly improves the practicability of applying formalism to design patterns.2010-04-22T11:31:23Z
Kim, Soon Kyeong; Carrington, David A formal mapping between UML models and object-z specifications
http://espace.library.uq.edu.au/view/UQ:147470
2008-06-06T13:32:14Z
Kim, S.; Carrington, D. A. A formal metamodeling approach to a transformation between the UML state machine and object-z
http://espace.library.uq.edu.au/view/UQ:97290
A significant problem with currently suggested approaches for transforming between models in different languages is that the transformation is often described imprecisely, with the result that the overall transformation task may be imprecise, incomplete and inconsistent. This paper presents a formal metamodeling approach for transforming between UML and Object-Z. In the paper, the two languages are defined in terms of their formal metamodels, and a systematic transformation between the models is provided at the meta-level in terms of formal mapping functions. As a consequence, we can provide a precise, consistent and complete transformation between them.2007-08-24T01:09:46Z
Kim, Soon-Kyeong; Carrington, David A Formal Metamodeling Approach to a Transformation between Visual and Formal Modeling Techniques
http://espace.library.uq.edu.au/view/UQ:10542
Formal modeling notations and visual modeling notations can complement each other when developing software models. The most frequently adopted approach is to define transformations between the visual and formal models. However, a significant problem with the currently suggested approaches is that the transformation itself is often described imprecisely, with the result that the overall transformation task may be imprecise, incomplete and inconsistent. This paper presents a formal metamodeling approach to transform between UML and Object-Z. In the paper, the two languages are defined in terms of their formal metamodels, and a systematic transformation between the models is provided at the meta-level in terms of formal mapping functions. As a consequence, we can provide a precise, consistent and complete transformation between a visual model in UML and a formal model in Object-Z.2004-04-08T00:00:00Z
Kim, Soon-Kyeong; Carrington, David A Formal Model Of Cognitive Processes For An Air Traffic Control Task
http://espace.library.uq.edu.au/view/UQ:10573
This document describes a formal model of the cognitive processes involved in a simplified Air Traffic Control task. The model has been developed as part of the SafeHCI project, which is investigating detection and prevention of human error in safety-critical systems. The model will serve as the basis for development of new techniques for prediction of error sources and classification of error types. This document describes the cognitive model in detail.2004-05-19T00:00:00Z
Connelly, Simon; Lindsay, Peter; Neal, Andrew; Humphreys, Mike A formal model of real-time program compilation
http://espace.library.uq.edu.au/view/UQ:62286
Program compilation can be formally defined as a sequence of equivalence-preserving transformations, or refinements, from high-level language programs to assembler code, Recent models also incorporate timing properties, but the resulting formalisms are intimidatingly complex. Here we take advantage of a new, simple model of real-time refinement, based on predicate transformer semantics, to present a straightforward compilation formalism that incorporates real-time constraints. (C) 2002 Elsevier Science B.V. All rights reserved.2007-08-14T17:46:28Z
Lermer, K.; Fidge, C. A formal model of UML metamodel: The UML state machine and its integrity constraints
http://espace.library.uq.edu.au/view/UQ:97289
2007-08-24T01:09:43Z
Kim, S.; Carrington, D. A. A formal object-oriented approach to defining consistency constraints for UML models
http://espace.library.uq.edu.au/view/UQ:100518
We discuss how integrity consistency constraints between different UML models can be precisely defined at a language level. In doing so, we introduce a formal object-oriented metamodeling approach. In the approach, integrity consistency constraints between UML models are defined in terms of invariants of the UML model elements used to define the models at the language-level. Adopting a formal approach, constraints are formally defined using Object-Z. We demonstrate how integrity consistency constraints for UML models can be precisely defined at the language-level and once completed, the formal description of the consistency constraints will be a precise reference of checking consistency of UML models as well as for tool development.2007-08-23T19:32:38Z
Kim, S.; Carrington, D. A. A Formal Ontology Reasoning with Individual Optimization: A Realization of the Semantic Web
http://espace.library.uq.edu.au/view/UQ:9048
Answering a query over a group of RDF data pages is a trivial process. However, in the Semantic Web, there is a need for ontology technology. Consequently, OWL, a family of web ontology languages based on description logic, has been proposed for the Semantic Web. Answering a query over the Semantic Web is thus not trivial, but a deductive process. However, the reasoning on OWL with data has an efficiency problem. Thus, we introduce optimization techniques for the inference algorithm. This work demonstrates the techniques for instance checking and instance retrieval problems with respect to ALC description logic which covers certain parts of OWL.2005-10-25T00:00:00Z
Pothipruk, Pakornpong; Governatori, Guido A formal V&V framework for UML models based on Model transformation techniques
http://espace.library.uq.edu.au/view/UQ:103130
2007-08-23T21:22:53Z
Kim, S. K.; Carrington, D. A. A framework and tool support for the systematic testing of model-based specifications
http://espace.library.uq.edu.au/view/UQ:67052
Formal specifications can precisely and unambiguously define the required behavior of a software system or component. However, formal specifications are complex artifacts that need to be verified to ensure that they are consistent, complete, and validated against the requirements. Specification testing or animation tools exist to assist with this by allowing the specifier to interpret or execute the specification. However, currently little is known about how to do this effectively. This article presents a framework and tool support for the systematic testing of formal, model-based specifications. Several important generic properties that should be satisfied by model-based specifications are first identified. Following the idea of mutation analysis, we then use variants or mutants of the specification to check that these properties are satisfied. The framework also allows the specifier to test application-specific properties. All properties are tested for a range of states that are defined by the tester in the form of a testgraph, which is a directed graph that partially models the states and transitions of the specification being tested. Tool support is provided for the generation of the mutants, for automatically traversing the testgraph and executing the test cases, and for reporting any errors. The framework is demonstrated on a small specification and its application to three larger specifications is discussed. Experience indicates that the framework can be used effectively to test small to medium-sized specifications and that it can reveal a significant number of problems in these specifications.2007-08-15T02:28:02Z
Miller, T.; Strooper, P. Μίνθα: a framework for auto-programming and testing of railway controllers for varying clients
http://espace.library.uq.edu.au/view/UQ:274105
2012-05-15T14:41:13Z
Süß, Jörn Guy; Carrington, David; Robinson, Neil; Strooper, Paul A framework for correctness criteria on weak memory models
http://espace.library.uq.edu.au/view/UQ:367091
The implementation of weak (or relaxed) memory models is standard practice in modern multiprocessor hardware. For efficiency, these memory models allow operations to take effect in shared memory in a different order from that which they occur in a program. A number of correctness criteria have been proposed for concurrent objects operating on such memory models, each reflecting different constraints on the objects which can be proved correct. In this paper, we provide a framework in which correctness criteria are defined in terms of two components: the first defining the particular criterion (as it would be defined in the absence of a weak memory model), and the second defining the particular weak memory model. The framework facilitates the definition and comparison of correctness criteria, and encourages reuse of existing definitions. The latter enables properties of the criteria to be proved using existing proofs. We illustrate the framework via the definition of correctness criteria on the TSO (Total Store Order) weak memory model.2015-08-11T02:53:30Z
Derrick, John; Smith, Graeme