These works are under preparation and their titles, abstracts and contents may change.
Many of these papers are co-authored with my PhD students.
The first listed is the most recently worked on and potentially the most drafty.
|
We describe the Pushlogic language and its implementation over the Tuplecore distributed data plane. Pushlogic is a constrained language for a dynamic population of devices (sensors/processors/actuators) and dynamic number of concurrent applications in a reliable or safety-critical system. System stability is assured by idempotency constraints and intrinsic error recovery capabilities arise from the reversible nature of Pushlogic programs. Disclosed material: LINK. Citations: Mace, Sinfonia, Alloy. |
|
This work takes three different implementations of an on-chip bus protocol, proves them equivalent using model checking and demonstrates their usefulness for synthesis of transactors, bus monitors and a bus router in Verilog and SystemC. The generated designs were tested as part of the design flow for an ASIC in industry. The three implementations use, repsectively, property-specification language (PSL), SysML statecharts and a stylised C-like imperative form that can be interpreted either as an input behaviour or an output behavior. A new algorithm is presented, that can convert an executable specification for protocols into either the initator, target or monitor for that protocol. The novel aspect of this work is that, in all cases, the input can be any mix of the three different languages and these are converted to a common form before processing by the algorithm. Disclosed material: LINK. |
|
Automated safety checking of a dynamic assembly of networked components is investigated using successively more-detailed models of link and node failure. Nodes contain state and lock variables that are annotated with automated behaviours to ensure safety under fault conditions. Examples using synthetic and real applications were checked with the XXX model checker. The individual components rected their application behaviour using .NET bytecode, carried using XML over HTTP to a checker for the domain. Keywords: CLR, .net, Pervasive Computing, Incremental Model Checking; Application Digest; Feature Interaction. |
|
Description logic underlies most formal ontology systems and these systems are being increasingly considered as a means to trigger dynamic instantiation of network services and applications, as well as providing dynamic binding for resources needed by these services and applications. This paper investigates where to draw the boundaries between description and execution, bearing in mind that description systems are not Turing-complete and that automated reasoning for feature interactions cannot handle arbitrary executable code. |
ESL design methodoloy mixes the conventional netlist approach to hardware modelling with behavioural modelling using thread calls between modules. These two forms of modelling are not directly compatible: a port modelled with a shared variable for each pin cannot communicate with a port that uses threads. Transactors are dual-ported adaptors that embody the protocol used at a port and convert from one style of modelling to the other. In this paper, we automatically extract the protocols from transactors in order check consistency and to re-synthesise new transactors with different port configurations. |
An abstract definition of the PIC family of processors, together with firmware from PIC ROMs, is compiled to hardware that uses fewer clock cycles. The process also supports reachability analysis, liveness and safety checks and proof of equivalence between designs. In this work, the instruction set and programmers' model for a number of small microprocessors, taken from the MicroChip Pic range, together with a model of the Controller Area Network (CAN) bus, are read into a model checker for refinement, equivalence and property checking. Since a full vehicle system, using ten or more nodes may explode our tool, we must slice the system in various ways. Previous work has looked at correctness of horizontal protocol layers (e.g. (?) used UPAALL to model check a CAN network at the device driver and and OS packet buffer level), but here we report on vertical collapsing of firmware together with its processor and an abstraction of the CAN bus. Disclosed material: LINK. |
Second draft, December 1999. Lightly updated in 2007 and perhaps 2014! In the current work, we propose a compiler or set of rules that map the abstract syntax tree of an imperative language, such as C, Java or behavioural Verilog, into a form where as many assignments as possible are formed in parallel. This form then maps well onto sequential clocked logic, where all flip-flops and synchronous RAMs are updated on one clock edge. Most RAM memory elements have restricted access and so rules for generating sequential access to the elements are included. The rules take into account the number and nature of the ports for each RAM. We allows any variable to be placed in any target RAM. We include an interpreter and an RTL (register transfer language) generator for the resulting structure. |
The adoption of formal methods and ESL methodology means that high-level, machine-readable specifications are becoming available for standard bus interfaces and ports on custom IP blocks. Automatic synthesis of interface automata between these components is now possible. Bus monitors that perform logging and error detection can also be synthesised. This paper reports on the synthesis of various interfaces between the GPIB (IEEE-488) and Centronix Parallel Port. Disclosed material: LINK. |
We present an architecture where a controller for a varying population of devices contains a varying number of rules that determine the desired behaviour of the system as a whole. We show how to generate these rules from a conventional, imperative, OO scripting language, give them relative priorities, how the controller determines whether a new rule can be accepted and how the controller executes the rules. The aim is to execute a number of concurrent applications of varying complexity and to be sure in advance of their potential interactions. This work is carried out under the CMI Goals/Pebbles project [1]. |
This CTOV compiler converts almost arbitrary C/C++ code to a hardware netlist. It operates by building the datapath for a VLIW-like processor and a sequencer to control the datapath that may or may not be microprogrammed. The datapath may consist of any number of RAMs and ALUs and also holding registers for data that cannot be transferred to/from RAM at the current time owing to RAM port bandwidth constraints. There are many possible datapaths that will serve to execute a given program, trading time for space. The compiler will generate a datapath using an internal heuristic that places each array present in the source code in a different RAM and converts all other state-bearing variables to flip-flops. However, the user can override the default action to control the datapath shape: he may specify the location of every variable stating whether it should be placed in a RAM or not, and if so, which RAM. The number of RAMs used and the style and number of ports on each RAM can also be fully specified by the user. This allows complete flexibility within a design space that encompasses a pair of opposite points: one point where all state is held in flip-flops and another point that places all programming-model state in a single, single-ported RAM. |