Dr. D J Greaves: Research in Progress.

System Design Methodology.

Note: Everything linked on this page is work in progress and likely to be incomplete!

I study how systems are designed. I am looking at the automated design and checking of hardware circuits, embedded firmware, and control applications in mission-critical systems.

I have two research projects underway at the moment, but the plan is that they will shortly meet in the middle! They are:

1. Trustable Application Scripting (AutoHAN/Pebbles/Pushlogic),

2. SoC and firmware design methodology at (and above) the ESL level.

These two strands can meet, for example, where I compile applications coded in Pushlogic into native firmware for CAN (car-area-network) node ASICs and thus am formally modelling complete nodes.

A near-term goal is to develop new form of machine-readable datasheet for controller components. This will be designed to support an incremental and compositional formal method for checking component assemblies. In general terms, it will be applicable in a huge number of fields, ranging over hardware design, middleware, web services and application software. I expect my first widely-disseminated result will be in the field of automotive electronics, where today even modest cars are built with tens of embedded controllers. Project proposal: LINK.

1. Pebbles, Incremental Model Checking and Trusted Scripting

The Pebbles project is currently investigating incremental model checking of networks of embedded systems and dynamic binding between software components based on information stored in a DL ontology.

Pebbles: are passive hardware or software components that can be stitched together by scripts to form applications. The scripts can implement something as simple as a timer-activated light or as complex as a telephone exchange with voice mail. The object form of the scripts (which can be in .net CIL) is amenable to automated reasoning. An experimental scripting language, Pushlogic, has been developed to test these ideas for embedded CAN networks, web services and distributed passive tuple spaces. Pushlogic embodies some novel features, including reversible execution for error recovery and idempotency to promote protocol soundness and to avoid flickering.

Pebbles stated as a collaborative CMI project with MIT for goal-oriented systems programming. In this project, we were creating a generative or 'first-class' mobile-agent system where formal specifications serve both as the internal DNA to an agent and to describe the surroundings that an agent enters. The first-class generative aspect requires all mobile agents to have the power to divide, specialise or spawn offspring. MIT was focussed on the mechanisms for automatic assembly while we worked on proving correctness of the systems.

Pebbles and Trusted Scripting is the current main activity with our over-arching AutoHAN scripting system, where programs are generated and edited in many forms (or views), including natural language and tangible interfaces, such as the Media Cubes. Also in this work, we are investigating to what extent the following three forms of programming can be supported in a common framework: 1. real-time control, such as `open the gates now', 2. execute once commands, such as `turn the lights off at midnight', and 3. complex application programs such as a TiVo or phone exchange.

2. SoC/ESL Design Techniques

ESL level (electronic system level) design is where components are brought together as software entities, using UML, XML, SystemC and C++, and only later converted to hardware languages when the system architecture is mature.

Most of the techniques that are significant for software design are becoming directly applicable to hardware design, both at the System On Chip (SoC) scale and for assemblies of components in sensor/actuator/controller networks. (Indeed, formal methods are more mature in hardware flows and are only recently being considered as a mainstream part of software design.) System development is facilitated when behavioural or transactional hardware models can be called directly from firmware without modelling the target machine code or SoC netlist. Three active projects are:

CSEW: Rapid development of network node ASICs by compiling firmware to gates and MicroCode Formal Equivalence Checking (PIC Processors).

Generic Systems Synthesis from Formal Specification. Orangepath.

Direct Synthesis of Logic using a SAT, QBF and SSMG.

Other Areas: Tuple Space Middleware

Apart from these two active strands, I am also taking an active interest in the future of middleware. Middleware is the glue between applications and the components they use. With the increasing use of distributed systems and dynamic, shared libraries, middleware is having to make more and more automated decisions. I believe the same approaches can be deployed for eternal, evolvable software systems as are useful for rapid development of bespoke systems.

Also I can envisage a rather significant migration from traditional computing paradigms, such as the integer, flat file and byte stream, where more meaningful datatypes are supported by the HLLs used for applications. Immutable types are needed for the time of day, addresses and electronic cash and so on, and these will become first-class rather than being treated as non-branded strings and integers. There are some initial ideas here: An Active Object layer providing a universal computing substrate (UCS). Specific systems will be built on this substrate for dedicated applications. But there remains a fundamental dichotomy between robust coding with compile-time warnings and errors (as supported by current HLL's for hardware and software) and generating flexible, robust, eternal systems that can tolerate and adapt to huge changes in their execution environment and in their peers. Bridges over this dichotomy are an integral part of any new approach to system synthesis.

Another, related interest is how e-commerce will insinuate itself into the binding operations provided by middleware libraries. I reckon that binding in middleware services will become the major e-marketplace. If we are not careful, there could be ten levels of indirection through ten different `value added' service providers each time we switch on the light in the bathroom!

Formal spec of a heating controller: LINK, other draft items: LINK.