Computing Science

University of Stirling

Autumn 1999 Seminars

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 Ken Turner (Phone 01786-467-420, Email kjt@cs.stir.ac.uk).

24th September 1999

Specification and Verification of Synchronous Hardware using LOTOS

Ji He, University of Stirling

DILL (Digital Logic in LOTOS) is an approach for specifying and analysing digital logic using the LOTOS formal specification language. After an overview of DILL, the talk will focus on the application of DILL to specification and analysis of synchronous circuits. Models of building blocks such as logic gates, flip flops and whole circuits will be given. Verification can then be achieved by equivalence or temporal logic model-checking. Two standard benchmark circuits have been specified using these models, and analysed by the LOTOS toolset CADP (Cæsar/Aldébaran Package).

15th October 1999

Digital Hardware Specification with A Protocol Specification Language

Dr. Gusztáv Adamis, Technical University of Budapest, Hungary

Apart from Hardware Description Languages, FDTs (Formal Description Techniques) are suitable for the specification of digital hardware elements. One of the most popular FDTs is SDL (Specification and Description Language) that was originally developed for specification of telecommunications protocols. SDL supports hierarchical system specification, high-level communication. and timing. These features make it suitable for description of hardware systems. But in SDL there is no way to define real-time timers, so signals may in fact not be consumed in the order they were sent. We have developed methods for ordering signals to avoid this problem. The presentation will also give examples of how the approach can be used to describe simple digital hardware elements.

22nd October 1999

A New Protection Model for Component-Based Operating Systems

Greg Law, City University, London

This seminar describes a new model of program protection particularly suited to component-based Operating Systems. Instead of the traditional separate user and kernel processor modes and paging, traditional segmentation is combined with a simple software technique to avoid the use of separate processor modes while maintaining full protection. This new model offers dramatically improved performance, simplified and improved architectures, and increased flexibility.

A component-based Operating System (called Go!) has been implemented using such techniques. Early experiences with it will be presented. In particular, Go! offers fully-protected round-trip RPC in just 85 cycles on a Pentium processor. Single-processor mode allows the ORB (Go!'s analogue of a kernel) to be responsible for component management only. Such a system allows multi-threading, device management and even interrupt handling to be provided by separate `application level' components.

5th November 1999

The Use of Non-Speech Sound in A Range of Computing Devices

Stephen Brewster, University of Glasgow

I will discuss the possibilities for the use of sound to improve interaction in computing devices, from desktop machines to hand-held devices. I will give an introduction to non-speech sound and then focus on two experiments we have recently performed:

Sonically-enhanced drag and drop

I will describe an experiment to investigate if the addition of non-speech sounds to `drag and drop' would increase usability. There are several problems with drag and drop that can result in the user not dropping a source icon over the target correctly. These occur because the source can visually obscure the target, making it hard to see if the target is highlighted. Structured non-speech sounds were added to indicate when the source was over the target, when it had been dropped on the target, and when it had not. Results from the experiment showed that subjective workload was significantly reduced, and overall preference significantly increased, without sonically-enhanced drag and drop being more annoying to use. Results also showed that time taken to do drag and drop was significantly reduced. Therefore, sonic enhancement can significantly improve the usability of drag and drop.

Sound in mobile computing devices (PDAs, HPCs etc.)

These devices have a limited amount of screen space as the device must fit into the user's hand/pocket. We wanted to see if sound could help overcome this problem. A 3Com Palm III was used. The aim of the pilot study conducted was to see if additional audio cues could improve the usability of buttons on the display, also allowing the size of the buttons to be reduced but still being usable. Preliminary results indicated that for large buttons there was a decrease in mental workload when sound was added (as measured by NASA TLX), an increased user preference, and an increased number of strings entered. For small buttons there was a decrease in workload across almost all workload categories, an increase in preference, and an increased number of strings typed.

3rd December 1999

Informatics turns Logic Upside-Down
(or, what's missing from Aristotelian thinking)

Dr. David Pym, Queen Mary and Westfield College, London

The following three observations are characteristic of traditional, i.e. mathematical and philosophical, approaches to a logical account of reasoning:

1. in problem-solving, deduction is prior to reduction
2. object-theory is prior to meta-theory
3. consequence is prior to relevance

I will explain these observations and argue that the concerns of informatics lead us to overturn each of them, illustrating my arguments with examples drawn from my research in each of the following three areas:

1. algorithmic proof-search, theorem proving and the science of reasoning
2. logical frameworks, from type-theoretic and algebraic perspectives
3. resource semantics and the design and implementation of logic programming languages

I will conclude with a long-term, unifying objective.

Up one level to Computing Science Seminars