Formal change impact analyses for emulated control software

Processor emulators are a software tool for allowing legacy computer programs to be executed on a modern processor. In the past emulators have been used in trivial applications such as maintenance of video games. Now, however, processor emulation is being applied to safety-critical control systems, including military avionics. These applications demand utmost guarantees of correctness, but no verification techniques exist for proving that an emulated system preserves the original system’s functional and timing properties. Here we show how this can be done by combining concepts previously used for reasoning about real-time program compilation, coupled with an understanding of the new and old software architectures. In particular, we show how both the old and new systems can be given a common semantics, thus allowing their behaviours to be compared directly.

The BCD transient recorder revisited: firmware for the ISA-to-USB bridging card and software for the graphical user interface

This report describes recent updates to the custom-built data-acquisition hardware operated by the Center for Hypersonics. In 2006, an ISA-to-USB bridging card was developed as part of Luke Hillyard's final-year thesis. This card allows the hardware to be connected to any recent personal computers via a (USB or RS232) serial port and it provides a number of simple text-based commands for control of the hardware. A graphical user interface program was also updated to help the experimenter manage the data acquisition functions. Sampled data is stored in text files that have been compressed with the gzip for mat. To simplify the later archiving or transport of the data, all files specific to a shot are stored in a single directory. This includes a text file for the run description, the signal configuration file and the individual sampled-data files, one for each signal that was recorded.

Digitally-implemented naturally sampled PWM suitable for multilevel converter control

For dynamic closed loop control of a multilevel converter with a low pulse number (ratio of switching frequency to synthesized fundamental), natural sampled pulse-width modulation (PWM) is the best form of modulation. Natural sampling does not introduce distortion or a delayed response to the modulating signal. However previous natural sampled PWM implementations have generally been analog. For a modular multilevel converter, a digital implementation has advantages of accuracy and flexibility. Re-sampled uniform PWM is a novel digital modulation technique which approaches the performance of natural PWM. Both hardware and software implementations for a five level multilevel converter phase are presented, demonstrating the improvement over uniform PWM.

Electromagnetic modeling of conformal wideband and multi-band patch antennas by bridging a solid-object modeler with MoM software

The advantages of antennas that can resemble the shape of the body to which they are attached are obvious. However, electromagnetic modeling of such unusually shaped antennas can be difficult. In this paper, the commercially available software SolidWorks(TM) is used for accurately drawing complex shapes in conjunction with the electromagnetic software FEKO(TM) to model the EM behavior of conformal antennas. The application of SolidWorks and custom-written software allows all the required information that forms the analyzed structure to be automatically inserted into FEKO, and gives the user complete control over the antenna being modeled. This approach is illustrated by a number of simulation examples of single, wideband, multi-band planar and curved patch antennas.

Use of CLIMEX modelling to identify prospective areas for exploration to find new biological control agents for prickly acacia

Selection of biocontrol agents that are adapted to the climates in areas of intended release demands a thorough analysis of the climates of the source and release sites. We present a case study that demonstrates how use of the CLIMEX software can improve decision making in relation to the identification of prospective areas for exploration for agents to control the woody weed, prickly acacia Acacia nilotica ssp. indica in the arid areas of north Queensland.

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.

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.

A reference architecture for instructional educational software

Our extensive research has indicated that high-school teachers are reluctant to make use of existing instructional educational software (Pollard, 2005). Even software developed in a partnership between a teacher and a software engineer is unlikely to be adopted by teachers outside the partnership (Pollard, 2005). In this paper we address these issues directly by adopting a reusable architectural design for instructional educational software which allows easy customisation of software to meet the specific needs of individual teachers. By doing this we will facilitate more teachers regularly using instructional technology within their classrooms. Our domain-specific software architecture, Interface-Activities-Model, was designed specifically to facilitate individual customisation by redefining and restructuring what constitutes an object so that they can be readily reused or extended as required. The key to this architecture is the way in which the software is broken into small generic encapsulated components with minimal domain specific behaviour. The domain specific behaviour is decoupled from the interface and encapsulated in objects which relate to the instructional material through tasks and activities. The domain model is also broken into two distinct models - Application State Model and Domainspecific Data Model. This decoupling and distribution of control gives the software designer enormous flexibility in modifying components without affecting other sections of the design. This paper sets the context of this architecture, describes it in detail, and applies it to an actual application developed to teach high-school mathematical concepts.

A software audit framework for spyware risk mitigation

Our research described in this paper identifies a three part premise relating to the spyware paradigm. Firstly the data suggests spyware is proliferating at an exponential rate. Secondly ongoing research confirms that spyware produces many security risks – including that of privacy/confidentiality breaches via illicit data collection and reporting. Thirdly, anti-spyware controls are improving but are still considered problematic for several reasons. Our research then concludes that control measures to counter this very significant challenge should merit compliance auditing – and this auditing may effectively target the vital message passing performed by all illicit data collection spyware. Our research then evolves into an experiment involving the design and implementation of a software audit tool to conduct the desired compliance auditing. The software audit tool is positioned at the protected network’s gateway. The software audit tool uses ‘phone-home’ IP addresses as spyware signatures to detect the presence of the offending software. The audit tool also has the capability to differentiate legitimate message passing software from that produced by spyware – and ‘learn’ both new spyware signatures and new legitimate message passing profiles. The testing stage of the software has proven successful – albeit using very limited levels of network message passing variety and frequency.

Implementation of a triple modular redundant FPGA based safety critical system for reliable software execution

This paper describes the implementation of a TMR (Triple Modular Redundant) microprocessor system on a FPGA. The system exhibits true redundancy in that three instances of the same processor system (both software and hardware) are executed in parallel. The described system uses software to control external peripherals and a voter is used to output correct results. An error indication is asserted whenever two of the three outputs match or all three outputs disagree. The software has been implemented to conform to a particular safety critical coding guideline/standard which is popular in industry. The system was verified by injecting various faults into it.