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).
Robert Hiromoto, University of Texas at San Antonio
Dr. Carron Shankland, University of Stirling
In formal methods we are always searching for new and interesting examples to which we can apply our techniques. In this talk I will introduce a case study based on the Philips "Firewire". (More specifically, the tree identify protocol of a high performance serial multimedia bus (IEEE standard 1394)). The description, given using muCRL, is made in varying levels of detail and I show, using the cones and foci technique of Groote and Spring in t'veldt, that these different descriptions are all equivalent under branching bisimulation. I'll also talk about the techniques used, and make some observations about properties of the protocol.
Dr. Jan-Friso Groote, University of Amsterdam
In this talk I will explain how we verified the Philips new remote control standard RC6 whose proof we checked using the proof checker COQ. Then I will spend some time on how we showed safety of the Vital Processor Interlocking in use at the Dutch railway company. If time permits, I will also make some remarks about Cones, Foci and mCRL with real time.
Dr. Adriana Compagnoni, University of Edinburgh
In trying to use Abadi and Cardelli's object calculi as a foundation for a programming language, the addition of algebraic data types arises naturally. This work defines such an extension, shows a motivating example, and explores the new calculi by establishing properties such as Church-Rosser, subject reduction and uniqueness of types. The work is joint with Maribel Fernandez (ENS Paris).
Prof. Ken Turner, University of Stirling
The specification of digital logic in SDL (Specification and Description Language) is investigated. A specification approach is proposed for multi-level descriptions of hardware behaviour and structure. The modelling method exploits features introduced in SDL-92. The approach also deals with the specification, analysis and simulation of timing aspects at any level in the specification of digital logic.
Dr. Bob Clark University of Stirling
Creating a full LOTOS specification is not only difficult, it includes many detailed and rather tedious tasks especially in the data typing area. We demonstrate how outline full LOTOS specifications can be generated automatically from OO models. A major part of this task is identifying the mappings between OO and LOTOS constructs. The OO models used are expressed in UML (Unified Modeling Language) which is being adopted as the industrial standard OO modelling notation. This work is in collaboration with the Systems Engineering Research Institute in Korea.
Up one level to Computing Science Seminars