This year was notable for the approval of the new integrated strategy for research support put forward by the Board's Computing Facilities Committee. The Engineering Applications Support Environment, EASE, began to take shape as a replacement for the three separate programmes, the Interactive Computing Facility, the Single User System Common Base and Engineering Applications.
1988 was the last full year of the Laboratory's involvement with the national advanced information technology programme coordinated and managed by the Alvey Directorate. Much of the year has been spent in winding down the infrastructure, coordination and support activities which have been provided by RAL over the past five years.
SERC is committed to using international standards where they exist and are appropriate. In information technology, standards are often at an embryonic stage. To ensure that due weight is given to European requirements and those of the UK in particular, RAL staff participate in British Standards Institute (BSI) committees, also acting as BSI representatives at international meetings with the aim of ensuring that standards relevant to the UK do appear. RAL provides support to a number of BSI activities.
RAL has been involved in most of the major standardisation activities in computer graphics for the last ten years.
GKS was the first graphics standard for input and output. It defined the main principles and methodology upon which the set of graphics standards is based. Some of the features in GKS came from RAL experience of producing graphics systems since 1966. RAL staff are document editors for the standard. They are responsible for ensuring a consistent style and layout for the document and that concepts and functionality are compatible. RAL's software engineering research in formal specification grew out of the involvement with GKS. The review cycle for GKS is about to start, when known errors will be corrected and enhancements considered.
RAL has been involved in the definition of PHIGS, a functional standard aimed at displaying highly structured 3-dimensional graphics and GKS-3D, a 3-dimensional extension of GKS. PHIGS is particularly useful for CAD applications. RAL has been concerned with ensuring consistency between PHIGS and GKS in functionality and document style. In some areas, formal specification of the equivalences between the standards has been defined.
The functional graphics standards need to be interfaced to the set of standard languages in a consistent and appropriate way. RAL has participated in this activity as a whole and been document editor for the FORTRAN binding to GKS-3D.
Research at RAL in formal specification techniques applied to graphics has demonstrated that significant parts of the graphics standards can be formally specified. Out of this has come an understanding of how the various parts fit together. From this, a proposal for a reference model for computer graphics has been developed initially by RAL and the University of East Anglia. If accepted by ISO, the International Standards Organisation, this will be used as the basis for all future standards. The model defines components (similar to abstract data types) and frameworks (constraints on how the components can be used). Fig 2.1 shows an example of the major parts of a graphics system defined in this notation.
RAL is a member of the ESPRIT CAD Interfaces Project (CAD*I) which is a European contribution towards producing a new standard for engineering product data exchange. RAL has been involved in the area of finite element modelling and analysis demonstrating that neutral files of finite element mesh data can be transferred between a structural analysis package and both pre- and post-processing systems.
Practical experience gained in the CAD*I project is being used to refine the specification of the new international standard STEP (Standard for Exchange of Product Data). RAL has been actively involved in the ISO meetings.
PROLOG is a programming language used for solving problems involving entities and the relationship between them. It is particularly useful in areas such as artificial intelligence, symbolic computation, knowledge representation and natural language understanding. The widespread use of the language over the last few years has led to the arrival of many variants and hence the need for a standard version.
Standardisation is at an early stage with a set of subcommittees formed, each dealing with one area. RAL has contributed to the subcommittee concerned with the built-in predicates. Similar to the intrinsic functions in FORTRAN, they add to the basic language a set of useful predicates which often cannot be defined in PROLOG itself.
RAL has been involved in the Alvey IPSE 2.5 project which is developing a support environment for formal methods of software engineering in particular VDM (Vienna Development Method). RAL researchers have contributed to BSI standardisation activities for VDM.
TAPDANCE, the Alvey Process and Device Analysis Command Environment (Fig 2.2), is an integrated computational modelling environment which enables the process/design engineer to simulate all the steps involved in making and operating a semiconductor device within a single piece of software. RAL has been responsible for the overall design of the system which consists of a shell of basic software (database, database manager, command parser, graphics post-processor and an overall controller) and a number of kernels which perform the various simulation tasks (geometric specification, ion implantation, diffusion, oxidation, mesh generation and device modelling).
RAL has provided the shell, geometry, mesh and device modelling kernels plus a simple implantation kernel, SIMPLANT. The other, more sophisticated, processing kernels have been provided by university partners. SIMPLANT simulates ion beam implantation into any target made of semiconductor device fabrication materials. A typical target consists of irregular abutting regions of silicon, silicon oxide and silicon nitride (Fig 2.3).
The project is targeted at an integrated approach to process and device modelling for 1 Jµm CMOS and bipolar technologies. The priority is to provide sophisticated and accurate modelling of critical process steps in a form which allows somebody with minimal specialist knowledge to use the TAPDANCE environment. To aid this, a comprehensive HELP system has been included.
DEVMOD, the RAL device modeller, solves the fundamental semiconductor device equations with the current transport given by the drift-diffusion model. A set of benchmark 2-dimensional problems has been run on the system and the results compared with data from a variety of sources. Good agreement has been achieved. Recently the ability to solve the on-state problem (ie when current is flowing in the devices) has been added.
TAPDANCE has been released to four external sites (University of Kent and University College, Swansea, STL and Plessey. The system runs on PRIME and VAX computers.
TAPDANCE is a 2-dimensional device modelling system. RAL has also been involved in an ESPRIT project with the more ambitious goal of developing robust and efficient algorithms to simulate the steady state and time-dependent behaviour of 3-dimensional semiconductor devices. EVEREST (European Venture for Research in Semiconductor Technology) has ten partners. RAL is project leader and partner with responsibility for the overall design of the software suite. This has a number of similarities with TAPDANCE, being highly modular and providing facilities for pre-processing data, doping, solving and post-processing the results.
The project is less advanced than TAPDANCE with work still to be done on software integration, adaptive mesh generation, handling transients, and developing the database (Fig 2.4).
As computers are used more and more in so-called 'safety-critical' systems, such as nuclear reactor control and fly-by-wire aircraft, and as the cost of maintaining large suites of software rises inexorably, there is an increasing appeal to mathematics in software engineering for techniques to specify what a system is supposed to do and to verify that the software code satisfies this specification. In essence the verification step amounts to proving theorems about the code. To make such techniques tractable to the practising software engineer, considerable effort is being devoted to the development of software tools to ease the theorem proving process. It has to be said at the outset that the goal of making such techniques available in every software engineer's toolbox is still years away. Nevertheless it is an area of great importance and one to which RAL has contributed through the ERIL project.
The subject of mechanical theorem proving, or automated deduction, has a long history which predates the advent of digital computers. One mathematical system which has received considerable attention is equational reasoning, or reasoning with equations. Equality is a fundamental logic concept of universal importance. Equations are often a natural way of expressing mathematical knowledge (and lie at the heart of the class of specification methods known as algebraic specification ), and the properties of the equality relation allow us to reason by replacing equals by equals, a very powerful and general technique. The following simple example illustrates this.
Given the equations (or axioms):
0 + x = x (1)
x + 0 = x (2)
(-x) + x = 0 (3)
(x + y) + z = x + (y + z) (4)
prove that:
(- (-a) ) = a for any a
A typical human presentation of a proof might be:
(i) (-(-a)) = (-(-a)) + 0 by (2) (ii) = (-(-a)) + ((-a) + a) by (3) (ill) = ((-(-a)) + (-a)) + a by (4) (iv) = 0 + a by (3) (v) = a by (1)
How may this process be automated?
The process involved in automating such reasoning includes unification (finding variable bindings which will unify. an expression with one side of an axiom, for example replacement of x by (-(-a)) in axiom (2) in step (i) above), rewriting (replacing one side of an axiom by the other side within the context of an expression (replacing equals by equals) and strategy (finding the sequence of axiom applications to show that two expressions are equal).
The major difficulty in automating equational reasoning lies in strategy. Any strategy chosen needs to have two properties, first soundness (any solution found must be correct) and second completeness (if there is a solution, it will be found). Much equational reasoning research is based on the Knuth-Bendix algorithm, a complete and sound strategy for solving the equality problem expressed by a given set of axioms. Interestingly, this important algorithm was first presented by Knuth at a workshop organised in Oxford by the former Atlas Computer Laboratory in 1970.
A key idea in equational reasoning is to treat a set of equations as rules for rewriting expressions. A rewrite rule written L = .R is an equation which is used in only one direction, ie L may be replaced by K but not vice versa. In the context of the example above, the equations can be written as:
0 + x = .x
x + 0 = .x
-x + x = .0
(x+y) + z = .x + (y+z)
A set of rewrite rules is called a rewrite system. If none of a set of rewrite rules apply to an expression E, then E is said to be in normal form with respect to that set.
There are two fundamentally important properties of rewrite systems. The rewrite system is said to be terminating if there are no infinite rewriting sequences E =.E' =.E" =...... . This is important because it guarantees that every expression has a normal form. The second property is that every expression has just an unique normal form, a property often called confluence. Confluence coupled with termination ensures that every expression has just one normal form and whether or not any two expressions are equal in such an equational system can be determined by checking whether or not those expressions have the same normal form. A set of rewrite rules which has these two properties is canonical. Intuitively a set of rewrite rules is finite, terminating if each of the right hand sides is somehow simpler than its left hand side. This can be ensured if an ordering of a certain type (termination ordering) can be associated with expressions. Given a terminating set of rewrite rules, the Knuth-Bendix algorithm essentially then adds new rules to the system to make it canonical.
ERIL is basically a very flexible tool to support equational reasoning. At the heart of ERIL is an implementation of the Knuth-Bendix algorithm which is rather more powerful than the original version. ERIL is able to handle algebraic structures which involve partial-functions (for example the division function which is not defined for division by zero) through a technique known as ordered sorts. Much of the power of ERIL derives from its interactive and highly configurable nature. It is possible to set up different sets of axioms, rules, canonical hypotheses and other equality sets, linking them in many different ways, thus providing a very flexible tool for research in equational reasoning.
Not all sets of equations generate sets of rewrite rules. An example is the commutative equation x + y = y + x. Such an equation can be applied an infinite number of times to an expression involving the operator +. No termination ordering can ever orientate such an equation since both sides have exactly the same structure and are derived from one another by a permutation of the variables concerned. There are ways in which such permutative equations may be handled in certain special situations, however, and ERIL is being extended to incorporate the use of these.
Recent work has indicated ways in which the Knuth-Bendix process can be used in proving theorems in classic logic and work is in hand to assess its benefits compared with more traditional approaches.
The ERIL system is now in use at 25 sites in the UK and at overseas universities. It is serving as an implementation test bed for ideas in a number of SERC grant-aided projects in UK universities, including Royal Holloway and Bedford New College, University of Glasgow and Imperial College, London.