Automated layout of small lattices using layer diagrams

Good quality concept lattice drawings are required to effectively communicate logical structure in Formal Concept Analysis. Data analysis frameworks such as the Toscana System use manually arranged concept lattices to avoid the problem of automatically producing high quality lattices. This limits Toscana systems to a finite number of concept lattices that have been prepared a priori. To extend the use of formal concept analysis, automated techniques are required that can produce high quality concept lattice drawings on demand. This paper proposes and evaluates an adaption of layer diagrams to improve automated lattice drawing. © Springer-Verlag Berlin Heidelberg 2006.

Using machine vision classification to control access of animals to water

Invasive vertebrate pests together with overabundant native species cause significant economic and environmental damage in the Australian rangelands. Access to artificial watering points, created for the pastoral industry, has been a major factor in the spread and survival of these pests. Existing methods of controlling watering points are mechanical and cannot discriminate between target species. This paper describes an intelligent system of controlling watering points based on machine vision technology. Initial test results clearly demonstrate proof of concept for machine vision in this application. These initial experiments were carried out as part of a 3-year project using machine vision software to manage all large vertebrates in the Australian rangelands. Concurrent work is testing the use of automated gates and innovative laneway and enclosure design. The system will have application in any habitat throughout the world where a resource is limited and can be enclosed for the management of livestock or wildlife.

Normal ranges for automated analysis of global LV function using 2D Strain

Background: Automated measurement of LV function could extend the clinical utility of echo by less expert readers. We sought to define normal ranges of global 2D strain (2DS) and strain-rate (SR) in an international, multicenter study of healthy subjects, and to assess the determinants of variation. Methods: SR and 2DS were measured in 18 myocardial segts in both apical and short axis views of 227 normal subjects (38% men, 48±14y) with no cardiac history, risk factors or drug therapy. The association of age and resting hemodynamics with global strain indices was sought using multiple regression. Differences in variance were expressed as F values. Results: Baseline SBP was 127±18 mmHg, pulse was 76±13/min and ejection fraction 50±20%. Although global longitudinal strain was influenced by endsystolic volume (F=4.2, p

Flexible proof reuse for software verification

Proof reuse, or analogical reasoning, involves reusing the proof of a source theorem in the proof of a target conjecture. We have developed a method for proof reuse that is based on the generalisation replay paradigm described in the literature, in which a generalisation of the source proof is replayed to construct the target proof. In this paper, we describe the novel aspects of our method, which include a technique for producing more accurate source proof generalisations (using knowledge of the target goal), as well as a flexible replay strategy that allows the user to set various parameters to control the size and the shape of the search space. Finally, we report on the results of applying this method to a case study from the realm of software verification.

An automated failure mode and effect analysis based on high-level design specificication with behavior trees

Formal methods have significant benefits for developing safety critical systems, in that they allow for correctness proofs, model checking safety and liveness properties, deadlock checking, etc. However, formal methods do not scale very well and demand specialist skills, when developing real-world systems. For these reasons, development and analysis of large-scale safety critical systems will require effective integration of formal and informal methods. In this paper, we use such an integrative approach to automate Failure Modes and Effects Analysis (FMEA), a widely used system safety analysis technique, using a high-level graphical modelling notation (Behavior Trees) and model checking. We inject component failure modes into the Behavior Trees and translate the resulting Behavior Trees to SAL code. This enables us to model check if the system in the presence of these faults satisfies its safety properties, specified by temporal logic formulas. The benefit of this process is tool support that automates the tedious and error-prone aspects of FMEA.

The production of male of-only offspring in beef cattle - a proof of principle project

The Australian beef industry places the greatest value in bulls, in comparison to cows, for prime beef production. Male carcasses can be sold for a larger profit due to their increased muscle mass. This project aims to demonstrate the feasibility of producing male animals that can sire male only offspring, through a transgenic approach in mice that could later be translated into livestock production systems. The mouse Sry (Sex determining region on the Y) gene has been shown to provide the initiating molecular signal leading to male sex determination in mammals. Sry has also been shown to cause sex reversal in XX mice transgenic for the gene. In this project Sry will be targeted to a locus not subject to X-inactivation on the X chromosome of XY mice. These mice will be bred to determine how the transgene is passed on, to determine expression of the transgene, and to assess its activity in causing XX sex reversal. The male mice transgenic for the Sry gene on their X chromosome will be produced using tetraploid aggregation, which in a single step produces 100% ES cell derived embryos. The same target locus can later be used to introduce the bovine SRY gene onto the X chromosome of bovidae species and using germ cell transplantation produce sex reversed animals. This would bypass the need for expensive chimera crosses and provide farmers with a stud bull capable of producing only sons.