The Department of Computing Science and Mathematics presents the following seminars. Unless otherwise stated, seminars will take place in Room 4B94 of the Cottrell Building, University of Stirling from 15.00 to 16.00.
If you would like to give a seminar to the department in future or if you need more information, please contact the seminar organiser Carron Shankland (Phone 01786-467-444, Email ces@cs.stir.ac.uk).
Charles Rattray, University of Stirling
Design is ubiquitous. We are all designers, every day, in Simon's sense. That is, whenever we define a set of actions to transform a current situation (state) to one meeting our requirements for a preferred situation (new state), we are involved in design. This purposeful adaptation is our common experience and gives us all an intuitive understanding of design. Yet it is clear that design is both an evolutionary process (ontogenetic or phylogenetic) and an abstract product (a pattern, a template, an abstract representation of an artifact).
An `intuitive understanding of design' is not enough, though. We are led to the question `How is design possible?' since it generally seems very much an art rather than a science, except for certain particular problem domains.
We know design is possible, of course, but can we develop a theory to answer the question which will explain how (or why) design is possible in a useful sense? A good theory should provide a framework in which what is required to be said becomes nearly obvious, whereas a bad theory would lead to contradiction and disconnection. Most design theories associated with systematic design, design method and, possibly, computer-aided design generally fail to render evidence about design being `nearly obvious'. For example, syncretic generation of potential prototype or outline designs are often dismissed as undesirable since any rational design approach must develop the solution directly from the analysis, with synthesis of problem requirements and constraints. Thus, rationality apparently demands the purging of the designer's mind of preconceptions: the `method' will create the design. But any analysis of what practical designers do shows clearly that their knowledge (pre-structures, types, artifacts) plays a fundamental role in design.
The aim of this talk is to suggest an answer to the question of the title by developing a sketch of a theory of design.
Dr. Andrew Ireland, Heriot-Watt University
Formal verification techniques are making inroads within the computer
industry, as demonstrated by the increasing use of model checking for
hardware design. General purpose theorem provers remain, however, primarily
the tool of the academic researcher. Automation will play an important role
in bridging the gap between the needs of academia and industry. In this talk
I focus upon the notion of a proof plan, and the unique benefits that it
offers those investigating strategies for automating theorem proving. In
particular, I focus upon what I believe are the three key benefits of the
proof planning approach:
Examples drawn from previous work will be presented that demonstrate each of the benefits claimed above. Future plans will also be outlined.
Prof. Ken Turner, University of Stirling
The Chisel notation was developed by Bellcore as an informal graphical notation for describing telecomms services and features. This paper presents Cress (Chisel Representation Employing Systematic Specification) as an enhanced version of Chisel. Cress has tightly defined rules for the syntax and static semantics of diagrams. More importantly, Cress has formal denotations given by SDL (Specification and Description Language) and LOTOS (Language Of Temporal Ordering Specification). This allows Cress descriptions to be rigorously checked, analysed and prototyped. The accompanying toolset has been written in an open and extensible manner, permitting a variety of front-end diagram editors, back-end code generators, and platforms for running the tools. It is indicated how the approach can be used to support automated detection of feature interactions.
Prof. Ken Turner, University of Stirling
Digital hardware is treated as a collection of interacting parallel components. This permits the use of a standard formal technique for specification and analysis of circuit designs. The ANISEED method (Analysis In SDL Enhancing Electronic Design) is presented for specifying and analysing timing characteristics of hardware designs using SDL (Specification and Description Language). A signal carries a binary value and an optional time-stamp. Components and circuit designs are instances of block types in library packages. The library contains specifications of typical components in single/multi-bit and untimed/timed forms. Timing may be specified at an abstract, behavioural or structural level. Timing properties are investigated using an SDL simulator or validator. Consistency of temporal and functional aspects may be assessed between designs at different levels of detail. Timing characteristics of a design may also be inferred from validator traces. A variety of examples is used, ranging from a simple gate specification to realistic examples drawn from a standard hardware verification benchmark.
Dr. Carron Shankland, University of Stirling
Symbolic transition systems give meaning to process algebras with data by abstracting away from the data, but talking about properties of processes requires some information how the data affects process behaviour.
I will give a symbolic semantics for LOTOS and discuss expressing properties of symbolic transition systems using modal logic. Essentially the logic is that of Hennessy and Milner, but modified to take account of data. A desirable property of the logic is that it is adequate with respect to symbolic bisimulation, i.e. it identifies the same processes. Therefore, I will also talk about how bisimulations can be defined over symbolic transition systems, what that means in terms of some simple examples, and the evidence supporting adequacy.
This is work in progress; the syntax and semantics of the logic is still in flux, subject to finalising a formal proof of adequacy.
Bruce Graham, University of Edinburgh
Artificial neural networks and biological nervous systems are similar in the sense that they both consist of large networks of computing units that interact to perform information processing tasks. There are significant differences, however, in most aspects of their respective operation, including information coding, signal transmission, plasticity or learning, computing units (neurons), and network architecture. To illustrate these differences I will give examples of computer simulations of synaptic (signal) transmission at a mammalian central nervous system synapse, and the operation of a cortical pyramidal neuron. The ultimate question of interest is: can a greater understanding of the nervous system provide new computational principles that can be employed in artificial systems?
To
Computing Science and Mathematics Seminars (Current Series)
To
Computing Science and Mathematics Research
To
Computing Science and Mathematics Home Page