Dependable Dynamite - Formal modelling in the commercial development of an optimising dynamic binary translator

Speaker: John Fitzgerald

13th February 2003 , 3pm , Room 519 Claremont Tower

Abstract

Dynamite is an optimising binary translator developed from research prototype to commercial product over the last two years. It allows programs written for one CPU to be executed on another while run-time optimisations are applied to blocks of code in order to recover translation overhead. Dynamite's translation kernel is configured with a variety of front- and back-ends for different instruction sets. For example, translators have been developed for x86-MIPS, Arm-MIPS and PPC-x86 combinations.

Assuring the dependability of Dynamite poses particular challenges. The product is small but intricate, and faces demanding performance and reliability requirements. This seminar will examine the use of model-oriented specification alongside more conventional technology as part of the defect avoidance strategy for Dynamite's software. Formal modelling techniques aim to help designers master system complexity by encouraging abstraction and providing tools to exploit the formal semantics of the model through validation. Modelling technology has advanced considerably in recent years, but what happens when it is faced with the realities of industrial software development for a demanding product in a volatile development environment?

The main features of Dynamite and its development environment will be introduced. The use of formal modelling will be illustrated with examples drawn from the VDM model of the product kernel. The successes and failures of formal modelling in this environment will be identified and form a basis for identifying challenges for formal methods in the future.