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 on Friday afternoons during semester time.
If you would like to give a seminar to the department or if you need more information, please contact the seminar organiser Carron Shankland (Phone 01786-467-444, Email ces@cs.stir.ac.uk).
Eerke Boiten, University of Kent at Canterbury.
In various research projects, we have looked at how a number of existing specification languages could be used for partial (or viewpoint-) specification. Generalising from these experiences, we are now attempting to distill the properties of specification languages that make them suitable for partial specification - on the basis of syntax, semantics, and pragmatics. The outcomes of this analysis will feed into an ongoing research project aimed at defining a general constructive framework for partial specification.
Lionel Morel, Verimag and Department of Computing Science, University of Stirling.
lustre is a synchronous language designed for the description of reactive systems. Among other happy industrial collaborators of the lustre team are EADS (for both the new A380 Airbus, and Ariane 5), Schneider-Electric (power plants), SNCF (French National Train Society), RATP (responsible for Paris subway), etc...
Most of the systems lustre is used for are called critical, because any deficience in their behaviour can have dramatic consequences on either human being or environment. Thus, one expects the code produced for a lustre program (and then used in an airplane or a power plant) to be efficient and safe. The delicate balance is then between efficiency and expressiveness (and in fact, what constructions we allow the programmer to use).
Arrays have been introduced to the language but, as the constructions provided first were specifically designed for the development of hardware systems, these constructions appear not to be satisfactory for programming software systems. Inspired by functional programming constructions, iterators have been proposed by Halbwachs/Maraninchi to overcome these flaws.
The idea of the MSc project presented here was to study the effective usefulness of the iterators and to develop a theoretical and experimental framework for the compilation and code optimizations of these new constructions.
Corin Gurr, Human Communication Research Centre and Division of Informatics, University of Edinburgh.
Diagrams are popular, as many people find them more readily ``accessible'' than other forms of representation. Diagrams typically contain far more visible structure than any text-based representation and this structure can be used to reflect the structure of whatever it is that the diagram represents. Diagrams, however, are not are not always or automatically the most effective forms of representations. Furthermore, diagrams are typically not as expressive as text-based representations; the structures inherent in diagrams which make certain information more visible and inferences easier, also constrain what they are able to easily express. Often the most effective diagrams are those which are very simple. However there is a strong tendency, particularly prevalent in visual formal modelling and specification languages, to take a diagrammatic language which at core is very simple, and then add many extensions and features to make it more expressive -- often making it so expressive that the diagrams produced in the language are no longer readable; or at least, the diagrams are no longer obviously a more effective form of representation than a text-based one.
I shall discuss guidelines for both the design of effective visual formal modelling and specification languages, and the effective formalisation of (the semantics of) such visual languages. These guidelines draw upon results from visual language theory, cognitive science, empirical psychology and graphic design. Integrating results from such diverse fields is a non-trivial task, which we approach through a decomposition of the study of issues of effectiveness in diagrammatic languages according to analogous understandings of (written and spoken) natural languages.
Peter Saffrey, University of Glasgow.
Model checking is a formal technique for proving properties of systems. A system is modelled using a particular modelling language and the possible states of this model enumerated to check its conformance to various properties. Complex systems can result in very large state spaces, and despite a great deal of work in the field, reduction techniques are not able to deal with many real world problems.
Like conventional programming languages, modelling languages often contain a degree of flexibility in how a system may be modelled. Differing models, whilst modelling the same system, can result in differing state space sizes. This knowledge can be used not only in the construction of efficient models from scratch, but also in the refinement of existing models. What kind of refinements can be applied, and when, will be the subject of this talk. Particular attention will be paid towards ensuring refinements are property preserving. Examples will be presented with reference to the model checker Spin and its modelling language Promela.
Perdita Stevens, University of Edinburgh.
In the Unified Modelling Language, use cases are provided as a way of summarising the requirements on a system. They are defined informally as specifications of sets of sequences of actions, and several relationships between use cases are informally defined. Dependable, tool-supported software development necessitates precise definitions of all these concepts but the topic has so far received little attention in the literature, beyond what is present in Catalysis. This talk, which is an extended version of one given at FASE this year, explores how these notions can be formalised whilst staying as close as possible to the UML standard. I'll make some suggestions for improving UML and talk about some areas which I think deserve more investigation.
Stephan Reiff-Marganiec, University of Stirling.
The feature interaction problem in telecommunications can be attacked in a number of different fashions. I explain why it is neccessary to detect and resolve interactions at runtime. After providing an overview of the detection method, this talk concentrates on resolution.
This talk is about the work I did for my PhD thesis, and hence was conducted while I was at the University of Glasgow.
Ken Turner, University of Stirling.
Graphical notations for describing services will be briefly overviewed. The talk will then concentrate on CRESS (Chisel Representation Employing Systematic Specification). This derives from the Chisel notation developed by BellCore (now Lucent and Telcordia). CRESS therefore reflects industrial practice in defining services. To Chisel it adds precision and the ability to translate service diagrams automatically into various target languages. A portable toolset makes it possible to describe, analyse and implement services on a variety of platforms. The talk will introduce the main capabilities of CRESS using the IN (Intelligent Network) and SIP (Session Initiation Protocol) as sample application domains.
Ramanee Peiris, University of Dundee.
Research has shown that some people find it easier to be open and honest with a computer rather than another person. This is particularly true when the topic is personal, embarrassing or the interviewee feels that the interviewer is in some way in authority over them. The reasons include that computers don't judge, don't blush and don't rush the interviewee. In this talk I will describe research in this field, including our own work with various organisations, including those who counsel alcholics, and those who work with survivors of sexual abuse.
John Derrick, University of Kent at Canterbury.
Z is a formal specification language, which uses mathematical notation to describe the system under consideration. Refinement is the name given to the process of developing one specification into another (more concrete) specification. Thus refinement aims to show that an implementation meets the requirements set out in an initial specification.
In this talk we briefly describe the Z approach to refinement and discuss recent generalisations of refinement targetting towards new applications where some traditional assumptions break down.
Bruce Graham, University of Stirling.
Artificial neural networks in general use a simple form of connection between computing units (or neurons) in which the output of one unit is multiplied by a connection weight to give an input value to a receiving unit. Learning algorithms are used to set these connection weights. While this can be said to be a model of how real neurons communicate, the actual communication between neurons is much more complex. This seminar will largely be a tutorial introduction (no neuroscience knowledge assumed) to the chemical synapse that forms the point of connection between two neurons. This synapse is a highly complex dynamic system. The "weight" of the connection provided by such a synapse has not only a long term average value, but changes on multiple time scales, from milliseconds to minutes, depending on the activity of the neuron that the synapse arises from. I will describe the mechanisms that underly the dynamic operation of the synapse and introduce the modelling work I am doing on a particular synaptic connection in the mammalian auditory system, the calyx of Held. Finally, I will talk about the possible functional consequences of short and long-term changes in synaptic weights.
Dave Marples, Honorary Professor at the University of Stirling
Even with the current slight downturn in the high-tech segment, the pace of technical development has never been so fast as it is now. In this talk we consider some of the emerging trends and try to guess at what the implications of these changes mean for us and our societies. We will consider advances in personal devices, network connectivity and processor capability, amongst other things, to guess at some of the good, and some not so good, things the future might have in store for us.
For further technical detail, see the complete set of slides from Dave's talk. Also available are the slides from Dave's later talk on careers.
If you want more information, email Dave.
Bing Qian, University of Stirling.
It is argued that complex safety-critical systems such as the control systems of radiotherapy machines need a systematic basis for their software testing. The talk will focus on the CONFORMED (Conformance Of Radiological/Medical Devices) project. It will describe an application of protocol specification and testing methods to radiotherapy accelerators. An outline specification will be given in LOTOS of the accelerator control system. It is completely infeasible to use this directly for test generation. Instead, specification inputs are restricted using annotations in a Parameter Constraint Language (PCL). This is automatically translated into LOTOS and combined with the accelerator specification. It then becomes manageable to generate tests of the actual accelerator to check that it agrees with its specification according to the relation ioconf (input-output conformance).
Amir Hussain, University of Stirling.
To
top of this page
To
Computing Science and Mathematics Research
To
Computing Science and Mathematics Home Page
Last Update: 25th September 2001.