The main thrust of NADA research at Kent has been on exploring ways of describing structures (for example, circuit diagrams) and their relations to behaviours. Structures are characterised by sets of nodes, sets of components and an incidence relation. The description is expressed in terms of dependently-typed higher-order logic. From this description, and working within the same logic, a predicate defining the behaviour may be extracted. The use of a dependently-typed logic is particularly beneficial since it allows types to occur both as values (in structural descriptions) and as types (in behavioural descriptions). This work was presented as a paper at the 1994 EUROFORM working group in Marseille.
Work has also been undertaken in developing a methodology for describing and reasoning about digital circuits at the analogue level. This allows formal methods to be satisfactorily applied to varieties of circuit design logic, such as pass transistor logic, which are widely used in practice but are presently beyond the reach of formal methods. This work benefited from liason within the MHDL (Microwave Hardware Design Language) working group, which also addresses the task of formally describing analogue systems.