Integrating runtime assertions with dynamic types: Structuring a derivation from an incomputable specification

An inherent incomputability in the specification of a functional language extension that combines assertions with dynamic type checking is isolated in an explicit derivation from mathematical specifications. The combination of types and assertions (into "dynamic assertion-types" - DATs) is a significant issue since, because the two are congruent means for program correctness, benefit arises from their better integration in contrast to the harm resulting from their unnecessary separation. However, projecting the "set membership" view of assertion-checking into dynamic types results in some incomputable combinations. Refinement of the specification of DAT checking into an implementation by rigorous application of mathematical identities becomes feasible through the addition of a "best-approximate" pseudo-equality that isolates the incomputable component of the specification. This formal treatment leads to an improved, more maintainable outcome with further development potential.

Specification matching of object-oriented components

Object-orientation supports software reuse via features such as abstraction, information hiding, polymorphism, inheritance and redefinition. However, while libraries of classes do exist, one of the challenges that still remains is to locate suitable classes and adapt them to meet the specific requirements of the software developer. Traditional approaches to library retrieval are text-based; it is therefore difficult for the developer to express their requirements in a precise and unambiguous manner. A more promising approach is specification-based retrieval, where library component interfaces and requirements are expressed using a formal specification language. In this case retrieval is based on matching formal specifications. In this paper we describe how existing approaches to specification matching can be extended to handle object-oriented components.

Improved joint control using a genetic algorithm for a humanoid robot

This paper describes experiments conducted in order to simultaneously tune 15 joints of a humanoid robot. Two Genetic Algorithm (GA) based tuning methods were developed and compared against a hand-tuned solution. The system was tuned in order to minimise tracking error while at the same time achieve smooth joint motion. Joint smoothness is crucial for the accurate calculation of online ZMP estimation, a prerequisite for a closedloop dynamically stable humanoid walking gait. Results in both simulation and on a real robot are presented, demonstrating the superior smoothness performance of the GA based methods.

A helicopter named Dolly: Behavioural cloning for autonomous helicopter control

This paper considers the pros and cons of using behavioural cloning for the development of low-level helicopter automation modules. Over the course of this project several Behavioural cloning approaches have been investigated. The results of the most effective Behavioural cloning approach are then compared to PID modules designed for the same aircraft. The comparison takes into consideration development time, reliability, and control performance. It has been found that Behavioural cloning techniques employing local approximators and a wide state-space coverage during training can produce stabilising control modules in less time than tuning PID controllers. However, performance and reliabity deficits have been found to exist with the Behavioural Cloning, attributable largely to the time variant nature of the dynamics due to the operating environment, and the pilot actions being poor for teaching. The final conclusion drawn here is that tuning PID modules remains superior to behavioural cloning for low-level helicopter automation.

Helicopter automation using a low-cost sensing system

This paper details the design of an autonomous helicopter control system using a low cost sensor suite. Control is maintained using simple nested PID loops. Aircraft attitude, velocity, and height is estimated using an in-house designed IMU and vision system. Information is combined using complimentary filtering. The aircraft is shown to be stabilised and responding to high level demands on all axes, including heading, height, lateral velocity and longitudinal velocity.