Colloquia

Colloquia are presentations by visitors and speakers, who are invited from around the country. They are held roughly every two weeks during term time, traditionally from 2.00-3.00pm, and adjourn to a general discussion over tea or coffee. Research students and staff are especially invited to attend.

At the moment there are no colloquia scheduled

Past Colloquia

August 2, 2011 2pm, Computing Science, Claremont Tower 7.01
Defining the operational semantics of languages with state and aliasing more simply
Ian Hayes

Plotkin's structural operational semantics defines the semantics of a language with state via an (unlabelled) relation over pairs of programs and states, whereas the operational semantics of (stateless) process algebras like CSS and CSP use an event-labelled relation over programs. In this talk we outline how a labelled relation over programs can be used to define the operational semantics of languages with state. In this case the labels are either state tests or state updates. Using this approach the semantics of local variables can be defined more simply using an explicit local state construct; the approach avoids having to add locations and environments to the semantics. A local aliasing/renaming construct can be defined in a similar manner, also without recourse to the use of locations. This allows by-reference parameters to procedures to be defined more simply.

April 6, 2011 3pm, Computing Science, Claremont Tower 7.01
A Layered Approach to Bottom-to-Top Assurance of Trustworthy Systems
Peter G. Neumann, SRI International

This talk will consider some of the challenges of designing predictably trustworthy total systems, with specific reference to an emerging system architecture being developed for DARPA by SRI and the University of Cambridge. This system involves the design of new capability-based hardware and a hybrid total-system architecture that permits coexistence of high-assurance software with legacy code. The basis for this work stems from hierarchical trustworthy systems such as Multics (rings of protection, symbolic dynamic linking, nested directories, least privilege) and SRI's Provably Secure Operating System PSOS design (formally specified hardware-software design for a tagged and typed more-or-less object-oriented capability-based system), other capability systems, separation kernels, virtual machines, and recently, Robert Watson's Capsicum and contributions to FreeBSD. Some of the underlying concepts include abstraction, strong encapsulation, explicit mappings between layers, dependency analyses, formal methods, and basic principles that can enhance predictable composition.

Some relevant URLs include:

• http://www.csl.sri.com/neumann/psos/psos.pdf (PSOS)
• http://www.csl.sri.com/neumann/psos03.pdf (PSOS)
• http://www.csl.sri.com/neumann/chats04.html and .pdf (Composition)
• http://www.csl.sri.com/neumann/law10.pdf (Layered Assurance)
• http://www.csl.sri.com/neumann/randell75.pdf (Brian Randell festschrift)
• http://www.csl.sri.com/neumann/ (website)
• http://www.cl.cam.ac.uk/research/security/capsicum/
• http://www.watson.org/~robert (Robert Watson's website)

March 16, 2011 1pm, Devonshire building G21/G22
Software Engineering for Business Application Development - Current Challenges in Research from an Industrial Point of View
Andrea Roth, SAP

Business applications are increasingly critical software components supporting the processes of companies. The expectations for and the technical architecture of these applications has changed a lot in recent years, imposing massive challenges on their creation and maintenance. In this talk we will report on experiences on advanced software engineering techniques applied to business application development, as for instance the use of Formal Methods, and we will highlight selected research challenges which we consider relevant from the point of view of a business software manufacturer.

January 24, 2011 11am-12.30pm, Room 1.02, Claremont Tower
A Formal Framework for Processes Inspired by Biochemistry
G.Rozenberg

Natural Computing is an interdisciplinary field of research that investigates human-designed computing inspired by nature as well as computation taking place in nature, i.e., it investigates models, computational techniques, and computational technologies inspired by nature as well as it investigates phenomena/processes taking place in nature in terms of information processing. One of the research areas from the second strand of research is the computational nature of biochemical reactions. It is hoped that this line of research may contribute to a computational understanding of the functioning of the living cell, which is based on interactions between (a huge number of) individual reactions. These reactions are regulated, and the main regulation mechanisms are facilitation/acceleration and inhibition/retardation. The interactions between individual reactions take place through their influence on each other, and this influence happens through these two mechanisms. In our lecture we present a formal framework for the investigation of processes carried by biochemical reactions. We motivate this framework by explicitly stating a number of assumptions that hold for a great number of biochemical reactions, and we point out that these assumptions are very different from the ones underlying traditional models of computation. We discuss some basic properties of processes carried by biochemical reactions, and demonstrate how to capture and analyse, in our formal framework, some biochemistry related notions. Besides providing a formal framework for reasoning about processes instigated by biochemical reactions, the models discussed in the lecture are novel and attractive from the (theoretical) computer science point of view. The lecture is of a tutorial style and self-contained, in particular no knowledge of biochemistry is required. FOLLOW-UP COURSE In the days following the colloquium, Professor Rozenberg will present a course on the topics relating to his talk. A tentative schedule is as follows: Tuesday, 25 January 2011, 11am-1pm Wednesday, 26 January 2011, 11am-1pm Thursday, 27 January 2011, 12noon-2pm The lectures will be delivered in Room 1.02, Claremont Tower.

November 25, 2010 2:15pm, 701, Claremont Tower
Information Sharing for the Financial IT Infrastructure
Professor Roberto Baldoni, University of Rome

With the joint advent of web 2.0, the ultra broadband and of the (private/public) cloud computing technologies, a new era is opening concerning the opportunity of sharing, processing and correlating a huge amount of information in a timely manner on the top of the Internet. It becomes indeed possible to customize virtual environments where group of partners share and correlate information that can be used, for example, to increase the partner’s security level from hackers’ attacks by raising situation awareness of each partner. The talk will discuss opportunities, requirements, technical solutions (including data dissemination, distributed event processing and cloud computing) and challenges for collaborative information sharing in the context of Financial Infrastructure. The talk will also going through the main achievements of the EU Project CoMiFin focussed on developing an innovative distribututed computing platform for Information Sharing for the Financial IT infrastructure.

November 19, 2010 2pm, Room 701, Claremont Tower
Places Everyone: Creating an Animated Background
Asst. Professor Jan Allbeck, George Mason University

Creating virtual scenarios that simulate a human population with typical and varied behaviors can be an overwhelming task. In addition to modelling the environment and characters, tagging the environment with semantic data, and creating motions for the characters, the simulation designer also needs to create character profiles for the population and link these character traits to appropriate behaviors to be performed at appropriate times and places during the simulation. At present, simulations either have a limited number of character profiles or are meticulously hand scripted. I'll describe an architecture, called CAROSA (Crowds with Aleatoric, Reactive, Opportunistic, and Scheduled Actions), that facilitates the creation of heterogeneous populations for simulations by using Microsoft Outlook®, a Parameterized Action Representation (PAR), and crowd simulator. The CAROSA framework enables the specification and control of actions for more realistic background characters in virtual worlds such as buildings and cities, links human characteristics and high level behaviors to animated graphical depictions, and relieves some of the burden in creating and animating heterogeneous 3D animated human populations.

August 9, 2010 2pm, Room 701, Claremont Tower
Chip and PIN is still broken
Mike Bond, University of Cambridge

At the beginning of year, BBC Newsnight reported startling news of how a stolen credit card can be used for fraud without knowing the PIN. Speaker Mike Bond is coauthor of the controversial paper "Chip and PIN is broken" [1] that described how this can be done, and the talk will explain how the attack works, and what went wrong. But, despite all the fuss, six months on, the same attack still works and has not been fixed by many banks. Is the attack proving harder than expected to fix? Was the attack over-hyped and is a fix not justified? Or do the banks have more urgent concerns to deal with first? The speaker will try to address some of the above questions, set the latest attack in context with the state-of-the-art in card fraud techniques, and internet banking attacks, and compare the relative importance.

June 18, 2010 2pm, Room 701, Claremont Tower
Modelling, Verification and Testing of the electronic payment system EP2 in CSP-CASL
Dr Markus Roggenbach, Swansea University

Computer systems often involve the distributed processing of data. Electronic payment systems are a typical example: The amount of money that a customer wants to pay by credit card needs to be communicated from a terminal to the financial institute which actually carries out the money transfer. On the other hand, the terminal and the finance institute act as independent processes. To synchronise their behaviour, terminal and finance institute communicate with each other. In our talk we discuss the design and tool support of the specification language CSP-CASL. CSP-CASL is dedicated to the integrated description of processes and data, where the algebraicspecification language CASL is used for data description and theprocess algebra CSP offers primitives to describe reactive behaviours. On the application side, we report on the modelling, verification and testing of the electronic payment system EP2 within CSP-CASL

June 18, 2010 10am, Room 701, Claremont Tower
Provable Secretless Security
Professor John Knight, University of Virginia

In this presentation, I will introduce a new security architecture called an N-variant system. N-variant systems employ artificial diversity, but, unlike other diversity-based approaches, N-variant systems thwart attacks without requiring secrets such as passwords. In addition, details of the implementation including known vulnerabilities can be made public without harm. An N-variant system uses redundancy to require an attacker to simultaneously compromise multiple variants with the same input.Carefully tailored diversity across the variants makes it impossible to compromise all the variants with the same input for given attack classes. Any attempt leads to a detectable failure of one of the variants. I will introduce the N-variant systems framework, and discuss variations that can be used to detect attacks that involve referencing absolute memory addresses, executing injected code, and certain types of data corruption. For each, I will present performance results from prototype implementations. Finally, I will present a comprehensive model of the N-variant system concept and show how it can be used to tailor N-variant systems to have specific security properties.

May 21, 2010 2pm, Room 701, Claremont Tower
Towards Ontology Repair in Physics
Alan Bundy

We investigate the problem of automatically repairing inconsistent ontologies. A repair is triggered when a contradiction is detected between the current theory and new experimental evidence. We are working in the domain of physics because it has good historical records of such contradictions and how they were resolved. We use these records to both develop and evaluate our techniques. To deal with problems of inferential search control and ambiguity in the atomic repair operations, we have developed ontology repair plans, which represent common patterns of repair. They first diagnose the inconsistency and then direct the resulting repair. Several such plans have been developed to repair ontologies that disagree, e.g., over the value and the dependencies of a function. We have implemented the repair plans in the GALILEO system and successfully evaluated GALILEO on a diverse range of examples from the history of physics.

May 20, 2010 10.00am, Room 3.13, Daysh Building
Mistakes in CAPTCHA design and implementation
Dr. Julio Cesar Hernandez-Castro

The design of CAPTCHAs suffers nowadays from a total lack of proper development methodologies. The natural consequence of this is that many designs are based on very poor ideas and/or frequently present faulty implementations. In this presentation we will review some well-known classical cases, but will also present our recent results against a variety of other proposals, including some commercial ones, and examine how their security can and should be improved.

May 17, 2010 2pm, Room 701, Claremont Tower
On the reliability of correct programs
Marie-Claude Gaudel

Verification and Validation of computerised systems rely on numerous methods. This lecture will focus on two of them: program proving and system testing, with some mention of model checking. The intriguing question of the interactions and complementarities of these methods will be discussed. What can we say of the reliability of a software-based system where some proofs have been done on the program?

April 7, 2010 2pm, Room 701, Claremont Tower
Uncertainty Explicit Methods for Reliability Assessment of Fault-tolerant Software
Dr Peter Popov

The talk will present a Bayesian assessment method suitable for software system built with diverse channels (software diversity) and demonstrate its applicability on a range of case-studies: assessment of an on-demand protection systems, selection of the most suitable pair of RDBMS (SQL servers) from a pool of products available off-the-shelf, a managed on-line upgrade of a web-service. The talk will also discuss the issues of scaling the method to more complex structures and will present early results from applying this ‘multiple views’ approximation on contrived examples. The accuracy of the Bayesian predictions achievable with the method is explicitly controlled using advanced statistical methods. About the presenter. Dr Popov has been with the Centre for Software Reliability, City University London since 1997. Currently he is Reader in Systems Dependability and Director of Innovation at CSR. He holds a PhD degree in computer engineering from the Polytechnic University (KPI) in Kiev, Ukraine. His research interests include methods for software and systems dependability assessment based on probabilistic modelling; using software diversity for building reliable software systems from off-the-shelf software. More recently he became involved in developing methods and tool support for interdependency analysis of critical infrastructures.

April 7, 2010 11am, the Hub, Culture Lab
Attention for Multi-Modal Human-Machine Interaction
Boris Schauerte

Attention is the cognitive process of focusing the processing of sensory information onto salient, i.e. potentially relevant and thus interesting data. Focusing the attention is a crucial task, because it enables efficient, real-time processing of the relevant information despite limited cognitive processing resources. Accordingly, during the last decade, (computational) attention models attracted an increasing interest in psychology, computational neuroscience, computer vision, and robotics. In natural human-machine interaction computational models of attention can either be used to focus the attention of the human or the machine. This talk will focus on the latter and indroduce a multi-modal attention model for smart environments. The model integrates auditory and visual saliency in a microphone-array and active multi-camera setup. By transferring the most important attention mechanisms, it is able to focus computationally complex operations on salient information as well as to support the human perception in multi-camera environments. Furthermore, a biologically motivated model to identify the referred-to object in multi-modal referring acts is introduced. Visually identifying the referred-to object, especially if the object was not verbally specified or is unknown, is an important aspect of natural interaction and a key aspect in order to relate the visual appearance of objects with their verbal specifications.

March 23, 2010 2pm, Room 701, Claremont Tower
Formal validation of web services compositions
Yamine Ait Ameur

Several web services compositions languages and standards are used to describe different applications available over the web. These languages are essentially syntactic ones and do not offer any guarantee that the described services achieve the goals they have been designed for. The objective of this talk is twofold. First, it focuses on the formal modelling, design and validation of web services compositions using the Event\_B method. We suggest a refinement based method that encodes BPEL models decompositions. Second, we show that relevant properties formalized as Event\_B properties can be proved. We will focus on transactional properties. At end, we discuss the basic architecture of the BPEL2B Rodin Plug-in tool encoding the proposed approach.

January 14, 2010 2pm, CLT701
Optimistic Fault Models for Low-Cost Byzantine-Fault Tolerant Systems
Marco Serafini

We are increasingly relying on computer systems to carry out critical tasks with very high degrees of dependability. For example, safety-critical systems have long been used in the aerospace domain. The trend towards storing and managing personal information online is extending the need for dependable services to a growing range of applications, from emailing, to calendars, to the storage of photos. High dependability requirements can be met with higher assurance by systems that are able to tolerate worst case failures, which are often named as Byzantine. Byzantine Fault Tolerance (BFT) is required by certification authorities for most safety-critical applications and is being advocated for critical Internet services too. BFT can be achieved by replicating logical functionalities over multiple physical nodes of a distributed system. However, the entailed replication costs are quite high. This talk points out that it is possible to reduce these costs by using optimistic fault models. In fact, Byzantine faults represent the exception rather than the rule since faults are often of more benign nature. The talk will review three modern technology trends which can be leveraged for cost reduction using optimistic fault models. The first trend is the foreseen raise in the ratio of transient faults compared to permanent faults in modern hardware due to reduced geometries and lower voltage levels. The second is the development of trusted nodes which only fail in a restricted, benign manner. The third is that replication clusters are relatively small, even in large-scale systems. The talk will then focus on the last trend and present a novel algorithm, called Scrooge, which can be used to achieve low-cost BFT in large scale or geographically-distributed systems.

November 18, 2009 1pm, Space 2, Culture Lab
A custom computer for older people
David Frohlich

Abstract The complexity of Internet computing is increasing rapidly as services diversify and connectivity extends to new platforms such as the mobile phone, TV, game stations and even photo frames. At the same time, many government and commercial transactions are moving on-line at the expense of traditional off-line transactions with service staff. These trends disadvantage some groups of older people who have never engaged with digital technology, or find it increasingly difficult to do so with age or disability. In this paper I discuss one response to this issue in the form of a custom computer or 'CC' which is simplified, managed and optimised for an older people's market. What this should do and what form it should take was the subject of two creative workshops with older peoples' groups on the SUS-IT project, funded by the New Dynamics of Ageing programme in the UK. Using a combination of drama and new technology demonstration we presented a simple touch-screen device with a stripped down suite of applications and some novel interactive features, to both PC and non-PC users of retirement age. Participant reactions and their own design ideas will be presented as the basis of recommendations for this approach. Biography David Frohlich is professor of Interaction Design at the University of Surrey. Since 2005 he has worked as Director of Digital World Research Centre which carries out user-centred innovation studies on new media technology (http://www.dwrc.surrey.ac.uk/). Prior to joining Digital World, David worked for 14 years as a senior research scientist at HP Labs, conducting user studies to identify requirements and test new concepts for mobile, domestic and photographic products. This allowed him to pursue ongoing research interests in tangible interfaces to computing, new media design, and the global digital divide. He holds a number of patents in the area of digital storytelling and augmented paper, arising from his work on audiophotography. David has a PhD in psychology from the University of Sheffield and post-doctoral training in Conversation Analysis from the University of York. He also worked as a Human Factors Consultant and Research Psychologist, and held visiting positions at the Helen Hamlyn Research Centre, Royal College of Art, and the Department of Psychology, University of York. He is currently Visiting Professor at Manchester Business School and is founding editor of the international journal Personal and Ubiquitous Computing.

November 10, 2009 2pm, Room 701, Claremont Tower
Software Productivity Assessment
John Richards

Following a quick tour of the Software Engineering Department at IBM's Thomas J. Watson Research Center, I'll review our work in support of the creation of a new, commercially viable, peta scale super computer. The fact that we are crossing the barrier to sustained petaflop performance is interesting. Even more interesting is the fact that the project has aggressive requirements for productivity, not just performance. This reflects the field's growing realization that a major barrier to further advances in parallel and scientific computing is the ability of humans to write, debug, tune, deploy, and administer software at this scale. I'll discuss how we are assessing improvements in human productivity attributable to new parallel programming languages and new tools and environments. I'll conclude with a few thoughts on how productivity assessment can be woven into the more general practice of software engineering. Bio of speaker - John Richards joined the Computer Science research staff at IBM's Thomas J. Watson Research Center in 1978 after receiving his Ph.D. in Cognitive Psychology. He has served in research, programming and management roles in numerous networking and interpersonal communications projects and has been recognized for his contributions in the area of digital voice mail systems by the Human Factors Society. Most recently, he has been involved in the design and programming of solutions in areas including Internet access for students and teachers, wireless e-business, web accessibility, social computing, end-user programming, and software productivity assessment. Dr. Richards has been active in the ACM SIGCHI, SIGPLAN, and SIGACCESS communities. He chaired the OOPSLA'91 Conference and served as chair of the OOPSLA Steering Committee from 1991 to 1996. He was elected a Fellow of the ACM in 1997 and a member of the IBM Academy of Technology in 2006.

August 26, 2009 2pm, Room 701, Claremont Tower
Displays and Sensors Everywhere - (only) a First Step Towards Interacting with Information in the Real World
Albrecht Schmidt

Computing is inevitably moving towards computing in context: it takes place in situations in the real world that are very different current desktop computer systems. In our research we explore how embedding pervasive computing technologies will change the way we live and interact with information systems and communication devices. Conceptually the challenge is to embed technologies in such a way that their appearance and usage is compatible with and supportive of the primary tasks done by the user. Technically this requires the embedding of display, interaction, and tracking technologies. By sensing the user’s behaviour and actions in the real world, the acquisition of contextual information, and by means for truly multimodal presentation we can embed interaction with information seamlessly into environments, vehicles, devices, and artefacts. Hereby the aim is that users are supplied with relevant information, without the need to actively interact with computers and without having to look deliberately for information. In such a vision the interplay of pervasive display networks, distributed sensor systems, and proactive information provision is essential. The talk will discuss fundamental technology trends that will make the vision of pervasive and contextual information systems possible. Gathering and predicting information as well as proactive and contextual presentation are key research challenges towards this goal. The talk will show several examples of pervasive computing systems that have been developed in our lab, e.g. mobile context-aware public display system and automotive user interfaces. Short bio of the speaker: Albrecht Schmidt is a professor in Computer Science and heads the chair for Pervasive Computing and User Interface Engineering at the University of Duisburg-Essen in Germany. Previously he was at the Fraunhofer institute for intelligent information and analysis systems(IAIS) and professor at the University of Bonn. From 2003 to 2006 he headed the embedded interaction research group at the University of Munich. Albrecht studied in Ulm, Manchester, Karlsruhe, and Lancaster where he completed his PhD on the topic “ubiquitous computing ­computing in context”. His teaching and research interests are in media informatics and ubiquitous computing, and in particular in the area of user interface engineering. Albrecht enjoys creating new interaction techniques and interfaces technologies for specific environments such as public spaces, the home, or the car. Over recent years he organized several workshops and conferences and served in various committees in pervasive computing community. His blog is at http://albrecht-schmidt.blogspot.com/

August 5, 2009 2pm, Room 701, Claremont Tower
Conversational information seeking and exchange
Elizabeth Churchill

The Internet has always been about communication, conversation and collaboration. In this talk I will draw on a number of research projects that have looked at the communicational aspects of collaborative and cooperative activity. I will consider the ways in which certain tools, applications and platforms do and do not support collaborative conversations. Through this work, I will recast information search as a social practice, complementing - and perhaps challenging - the dominant vision of search as the attempt by an individual to satisfy an information need. I will open discussion to how this shifting view affects the design of social search technologies. Profile of the speaker: Elizabeth Churchill is a Principal Research Scientist at Yahoo! Research where she manages the Internet Experiences research group. Originally a psychologist by training, for the past 15 years she has drawn on diverse areas to consider how to design effective communication situations- both face to face and technologically mediated. Prior to joining Yahoo!, she worked at PARC, the Palo Alto Research Center in Palo Alto, California, and was the lead of the Social Computing Group at FX Palo Laboratory, Fuji Xerox's research lab in Palo Alto. She was recently elected Vice President of ACM SigCHI. See: http://elizabethchurchill.com/

July 10, 2009 2pm, Room 701, Claremont Tower
Formal methods and user-centred design
Steve Reeves

As computers and software applications become ubiquitous the systems we build are increasingly required to run on not just a single piece of hardware, but rather be available for different platforms, different types of hardware and offer different modes of interaction depending on the context of use. Within a formal development process when we consider building interactive systems we therefore need to consider not only the transformation of abstract specifications and models into single implementations but also the possibility of several implementations with differing interactive requirements. In such cases the changing requirements in general and changes to the user interface in particular make supporting the development by formal development challenging. One way to solve this problem is to extend our notion of refinement which, having first motivated the whole question of putting together formal and user-centred design methods (not a natural fit, perhaps!),we look at in this seminar.

June 23, 2009 2pm, 701 Claremont Tower
Of Bugs and Men (and Plugins too)
Michel Wermelinger

This talk presents a cursory view on our preliminary investigations into architectural evolution, socio-technical congruence, and bugs, taking Eclipse as the case study. We look at how the architecture has grown over 6 years and whether it follows some principles stated in the literature. We use formal concept analysis to group developers according to the bugs they fix and discuss. We try to visualise bug report characteristics in a compact way.

June 9, 2009 2pm, Room 701, Claremont Tower
How to participate in Embedded Systems (ES) research in Europe even though you're not part of the ES community, yet,
Dr Carlos Juiz

In this talk, Dr Carlos Juiz, will focus on the ARTEMIS platform view of ES and his related research in ES as a member of the Industrial Association

June 2, 2009 2pm, 701 Claremont Tower
Verifying non-blocking and fine-grained concurrent algorithms.
Matthew Parkinson

In the quest for tractable methods for reasoning about concurrent algorithms both rely/guarantee logic and separation logic have made great advances. They both seek to tame, or control, the complexity of concurrent interactions, but neither is the ultimate approach. Rely- guarantee copes naturally with interference, but its specifications are complex because they describe the entire state. Conversely separation logic has difficulty dealing with interference, but its specifications are simpler because they describe only the relevant state that the program accesses. In this talk, I will describe our recent research on combining ideas from both rely-guarantee and separation logic. I will demonstrate this combination by showing how to verify a series of intricate concurrent algorithms.

April 21, 2009 2pm, G21/22 Devonshire Building
Global Predicate Detection in Faulty Distributed Systems
Arshad Jhumka

We study the problem of global predicate detection in presence of permanent and transient failures. We term the transient failures as small faults. We show that it is impossible to detect predicates in an asynchronous distributed system prone to small faults even if nodes are equipped with a powerful device known as \emph{failure detector sequencer} (denoted by $\Sigma$). To redress this impossibility, we introduce a theoretical device, known as a \emph{small fault sequencer} (denoted by $\Sigma_{SF}$), and show that $\Sigma_{SF}$ is necessary and sufficient for predicate detection. Unfortunately, we also show that $\Sigma_{SF}$ cannot be implemented even in a synchronous distributed system. Fortunately,however, we show that predicate detection \emph{can} be achieved with high probability in synchronous systems. This is joint work with Felix Freiling, Dept of Computer Science, Uni Mannheim.

March 24, 2009 2pm, 701 Claremont Tower
The Hadrian Project, turning castles into digital fortresses!
Phil Butler

Phil will aim to introduce his self and the project explaining what the project is about, how it originated, why he is doing it and how he is engaging with the local community.

February 24, 2009 2pm, 701 Claremont Tower
Investigating Collaboration Around the TableTop - effects of input device configuration on awareness and equity of participation.
Eva Hornecker

I will discuss recent research conducted with my collaborators at the Pervasive Interaction Lab at the OU on collaboration and tabletop interaction. Our research investigates interfaces that support co- located and co-present interaction. We propose ‘shareable interfaces’as a more inclusive term focusing on the kinds of activity to be supported rather than on the design of the interface per se (tangible, tabletop, large displays etc.). It is still a research question how best to support group interaction around interactive tabletops, and the effects of different configurations of input devices and setups. Our study has two parts, investigating the effect of touch interaction versus mice on awareness, and the effects of touch versus mice as well as the number of access points (one/multiple mice/touch) on equity of participation. We found higher levels of both positive and negative measures of awareness in the touch condition. A subsequent qualitative analysis indicated that the interactions in the touch condition were more fluid and integrated. Overall, our findings indicate that interactive touch surfaces facilitate collaboration through enabling more fluid work. Our analysis highlights the importance of allowing groups to handle interferences as they occur as a design imperative (in contrast to avoiding interference). In the second part of our study we found an effect on 'manual' participation of both touch and multi-input as well as strong effects on the subjective perception of over- and under-participation. Qualitative analysis suggests that effects are bigger for heterogenous groups than for groups of similar status and talkativeness. Eva Hornecker is a Lecturer in the Department of Computer and Information Sciences at the University of Strathclyde in Glasgow, UK.In previous lives, she was a Postdoctoral Research Fellow at the Pervasive Interaction Lab at the Open University and the University of Sussex (working on the Equator project) in the UK, and an Acting Lecturer at the University of Canterbury in New Zealand and at the TU Vienna in Austria. She wrote a PhD theses on 'Tangible Interfaces as a medium for collaboration support' at the University of Bremen. Her research interests concern multimodal, tangible and embodied interaction, user research, design methods, and qualitative research methods for understanding user interaction with ‘beyond the desktop’technologies.

February 19, 2009 2pm, 701 Claremont Tower
The Next Big Idea in Languages for Distributed Computing
Andy Gordon

The talk will be in 2 parts: a one hour overview, followed by a two-hour more detailed investigation. Everyone is welcome to attend only the overview, but please could staff encourage research students and RAs to attend the full session: this is the chance to learn in more detail what our Visiting Professor is working on. A refinement type is a type qualified by a logical constraint; an example is the type of even numbers, that is, the type of integers qualified by the is-an-even-number constraint. Although this idea has been known in the research community for some time, it has been assumed impractical, because of the difficulties of constraint solving. But recent advances in automated reasoning have overturned this conventional wisdom, and transformed the idea into a practical design principle. This lecture is a primer for developers on the design, implementation, and application of refinement types. I will explain: - How diverse features such as security labels, units of measure, and pre- and post-conditions may be unified as instances of the general idea of refinement types. - How we statically check integrity and secrecy properties of security critical code, such as an implementation of CardSpace, using a system of refinement types for the F# programming language. - How a static checker for the Oslo modeling language M allows us to check for errors in server configurations; intended constraints on configurations are expressed with refinement types, so that configuration validation reduces to type checking. - How to largely eliminate the burden of writing refinement types via automatic inference.

February 5, 2009 2pm, 701 Claremont Tower
New Challenges in Network Optimization - P2P-based Systems
Dr Krzysztof Walkowiak

I will discuss recent research conducted with my collaborators at the offline modelling and optimization of P2P-based systems. In recent years P2P systems has been gaining much popularity. According to many statistics more than 50% of the Internet traffic is generated by various P2P systems. Thus, it would be decisive to reduce this load simultaneously maintaining the performance of P2P systems at acceptable level. Therefore, there is a growing need to deploy effective tools enabling modelling and optimization of network flows in P2P systems. Most of previous works on the network optimization was limited to unicast flows, which are not efficient for modelling of P2P networks. Therefore, we propose new Integer Programming models of network flows in P2P-based systems. Major assumptions and inspirations are taken from the BitTorrent protocol and previous works on this subject. As the main objectives of the optimization we propose to use: cost, time, system capacity and network survivability. During the talk we will give a brief introduction into network optimization issues. Next, our new proposals related to modelling of flows in P2P systems will be presented. We will also show some preliminary results illustrating our research.

January 13, 2009 2pm, 701 Claremont Tower
MetaB defining flexible semantics for EventB
David Streader

One of the initial design decisions in building a formal model is what aspects to formalise and what to leave informal. Consequently building formal models in the early stages of step wise program development can make the development fragile as these initial design decisions might need to be changed. Both Z and Event B have adopted a formal semantics that is open to many interpretations. This flexibility reduces the fragility of formal models built with them. We propose to extend this approach by showing how formalise the (re)interpretation of a model built using such semantics. At a more practical level we have started tobuild our general theory into a theorem prover both to give greater confidence as to the correctness of our approach and to be able to use the theorem prover to generate proof obligations for the chosen specific interpretation. By this means we are able to allow some very natural development steps that have previously been thought to not be covered by formal refinement steps. For more information on David Streader please see http://www.cs.waikato.ac.nz/~dstr/.

December 2, 2008 2pm, 701 Claremont Tower
Understanding designed-in errors in interactive devices
Prof Harold Thimbleby

Human error causes perhaps 20,000 "preventable" hospital deaths from adverse events per year in the UK. Computerisation in one form or another is often presented as a solution, however computer systems have the problem that latent errors in design can increase errors yet channel blame from the manufacturer, developers or hospital to the operators at the point of care. Thus many incident reports say "the device worked as designed" and hence conclude that operator behaviour, training or mismanagement is the key causal factor. This talk will show how very poor "state of the art" interactive device design is, and it will raise some concrete ideas (basically:ideas for better programming) for seeking remedies. The talk will be illustrated by examples of designed-in latent errors in drug dosage calculation, radiotherapy, and chemotherapy - all examples that are easily fixable from an apparently novel point of view: namely, putting computer science to good use.

November 11, 2008 2pm, Room 701, Claremont Tower
Finitely generated groups and expanders
Alina Vdovina

Expander graphs are simultaneously sparse and highly connected graphs. They are not only of theoretical importance but also useful in computer science. We give a new construction of a family of expander graphs of vertex degree 4, which are all coverings of each other. Each graph has twice as many edges as it has vertices. Our construction is very explicit, our graphs are Cayley graphs of finitely presented groups, with two generators and four relations.

November 6, 2008 2pm, Devonshire G21/22
Making sense of the Senseless
Dr. Chris Fowler,

> > The ISIS Project is investigating an integrated sensor information > system for crime prevention and detection on public transport. A > remote multi-modal sensor array will be investigated and deployed, > together with an integration platform designed to combine risk from > background criminology data and real-time dynamic risk from sensor > data, to give an overall crime/security risk assessment on the > network.

July 3, 2008 1pm, Space 7, Culture Lab
An Advanced Collaborative Infrastructure for the Real-Time Computational Steering of Large Scientific Simulations
Pierre Boulanger

Advances in computer processing power and networking over the past few years have brought a significant change to the modeling and simulation of complex phenomena. Problems that formerly could only be tackled in batch mode, with their results visualized afterwards, can now be monitored whilst in progress using graphical means, in certain cases it is even possible to alter parameters of the computation whilst it is running, depending on what the scientist sees in the current visual output. This ability to monitor and change parameters of the computational process at any time and from anywhere is called computational steering. By combining this capability with advanced communications tools, like the Access Grid, over high-speed network it is now possible for a group of scientists located across various continents to work collaboratively on simulations allowing them to compare ideas and to share their experience. This is a key advance as the notion of a scientist working alone in his laboratory is disappearing, as scientific problems get larger and more complex. At the University of Alberta numerous scientific projects are already using this technology, to name a few: * The Virtual Wind Tunnel Project at the Computer Science Department * Project CyberCell at the Institute for Bio-molecular Design * The Earth Core Simulation at the Department of Physics * Simulation of Subatomic Physics at the Department of Physics Many of these projects use high performance computing facilities such the one provided by the WestGrid infrastructure. Some projects are very close to the final goal of a truly interactive simulator and some are planning to do so. Form our experience collaborating with various Departments it is clear that there is a great need for such systems and for an infrastructure capable of providing this capability. During this presentation, we will present the current status in the development of these facilities and share our experience gained so far.

June 24, 2008 2pm, Room 701, Claremont Tower
Engineering sociability in embodied agents
Stefan Kopp

Embodied agents that figure either as humanoid robots or as 3D virtual characters are becoming increasingly popular for novel forms of human- computer collaboration and interaction. One of their main potential assets is the possibility for users to interact with a machine as if communicating inuitively and naturally with other humans. Along this line, a large body of work has been directed to develop machine capabilities for recognizing, categorizing, interpreting, planning, or synthesizing communicative behavior. It is thereby commonly presumed that comunicative behavior consists of more or less structured composites of meaning-encoding signs, sent over a conduit in order to merely transfer a piece of information from the sender to the receiver. In this talk, I will argue that what is equally needed is to create a good deal of „sociability“ in such agents. That is, we need to build systems that are able and willing to associate and resonate with others, to be supportive and companionable, and easy and pleasant to communicate with. I will present a number of projects that try to contribute important capabilities to this overarching goal: (1) the modeling of co-verbal expressivity, particularly by gestures that are known to be highly influenced by the sociality and engagement of discourse; (2) the sensorimotor grounding of non-verbal communication in close perception-action couplings that enable to interact in socially more „resonant“ ways, e.g., by implicit mimicry or alignment; (3) the acquisition of communicative behavior and its grounding in such couplings through imitation learning, and the taking of these couplings to higher levels of compositionality, symbolic encoding, and gesture meaning.

June 10, 2008 1pm, Room 701, Claremont Tower
Experiencing Design Research: Accommodation, Appropriation and Aesthetics in the Curious Home
John Bowers

A characteristic feature of the work of the Interaction Research Studio at Goldsmiths is our concern to put designs in the hands of users for long term field trials. People's encounters with our artefacts are studied using broadly ethnographic methods to develop a rich picture of their experience. In particular, we have developed a number of pieces under the umbrella of 'the Curious Home' which have a novel take on interaction with technology in domestic environments. Reviewing research from studies over a five year period, I will discuss a variety of issues: how people 'accommodate' technologies within their domestic routines, how people appropriate artefacts in manners not anticipated in design, how people develop an aesthetic appreciation of things. I will close with some broader meditations on how empirical study of this sort can help develop novel approaches to interactivity and aesthetic experience of relevance in the design of contemporary interactive technology.

June 3, 2008 2pm, Room 701, Claremont Tower
Modeling Security of Voting Protocols
Olivier de Marneffe

Voting systems are complex systems for which security assessment is desirable (or even mandatory). With this intention, we need to have ways to define security and introduce a model in which those definitions can be validated or refuted. One approach to do so is known as ``simulation-based definition of security''. In this framework, namely the UC-framework presented a few years ago by Canetti, security is defined through the specification of an ideal world in which ideal functionalities are being used. The ideal world specifies the communication network (type of channels,what is controllable by the adversary, what is observable by the adversary,...) and ideal functionalities are definitions of how we feel some part of the actual protocol should ``behave''. In this talk, we will discuss why and how to prove voting protocols in this framework. Starting from a definition of coercion-resistance (ensuring a voter can freely express her opinion) proposed by Moran and Naor (CSS'07), we will show that (a simplified version of) the Lee et al. protocol achieves such coercion-resistance. This example,introducing how simulation-based security works in practice, is also the starting point of a current reflexion about how to manage security under different assumptions. Indeed, authorities are involved in most of the voting protocols: how can we efficiently study what happens when one (or more) authorities get corrupted?

May 29, 2008 1pm, Room 701, Claremont Tower
Expert Software Designers' Strategies For Dealing With Complex and Intractable Problems
Marian Petre, The Open University UK

Software design is a realm of messy problems that are often too big, too ill-defined, too complex for easy comprehension and solution. At the design level, problems arise from structural complexity, emergent behaviours, conflicts among constraints, contradictory requirements, and so on. This talk reports on strategies expert designers use in dealing with complex and intractable problems. The report arises from a series of in situ observations and interviews with ten expert software engineers in the US and UK over two years. The experts were members of high-performing teams in small, multi-disciplinary, engineering consultancies, in the business of generating intellectual-property. It appears that experts manage intractable problems by transforming them: abstracting, simplifying, deferring parts of the problem, and so on. The talk will presents the observed strategies in turn and provide illustrative examples. It will discusses implications of expert reasoning about intractable problems for design practice and support.

May 13, 2008 1PM, Room 701 Claremont Tower
Visual Passwords: Cure-All or Snake-Oil?
Karen Renaud

'Dog-boat-flower-car' could be your password in the near future; and all you will have to do is to point at the corresponding pictures amongst a challenge group of displayed images in order to read your e-mail, place a mobile call or withdraw money at an ATM. This is an example of the use of the so-called "visual password" - an alternative to the traditional password whereby users have to recognize a set of assigned images rather than recall an alphanumeric string to gain access to a secure system. A number of visual passwords are already available in the marketplace, especially for PDAs, and the field is exhibiting signs of increasing popularity. Given this upsurge of interest we need to pose the question: "Are these passwords the panacea they are often claimed to be?" The current state of the art will be reviewed, and give the viability and potential of the graphical alternative to the humble and much-maligned password will be explored.

April 22, 2008 1pm, Claremont Tower. Room 701
Networked Information Processing and Changing Attitudes to Privacy in Japan
Andrew Adams

Dr Adams has spent nine months in 2007 visiting Meiji University in Tokyo, funded by a Global Research Award from the Royal Academy of Engineering. He has been studying the legal and social approach to privacy of electronic data in Japan and will present some of the results of his study. There is a myth amongst researchers that there is no such thing as 'Privacy' in Japan. Dr Adams refutes that and shows that the advent of networked information processing of personal data has brought Japanese attitudes to information privacy to a highly similar position to Western attitudes. Grounded in the social and psychological literature about Japan, this work explains the emergence of Japanese legal protection for personal data in recent years.

April 15, 2008 1pm, Room 701 Claremont Tower
An Introduction and Evaluation of Martlet - a Scientific Workflow Language for Abstracted Parallelisation
Daniel Goodman

The workflow language Martlet described in this talk implements a programming model that allows users to write parallel programs and analyse distributed data without having to be aware of the details of the parallelisation. Martlet abstracts the parallelisation of the computation and the splitting of the data through the inclusion of constructs inspired by functional programming. These allow programs to be written as an abstract description that can be adjusted automatically at runtime to match the data set and available resources. Using this model it is possible to write programs to perform complex calculations across a distributed data set such as Singular Value Decomposition or Least Squares problems, as well as creating an intuitive way of working with distributed systems. Having described and evaluated Martlet against other functional languages for parallel computation, we go on to look at how Martlet might develop. In doing so it covering both possible additions to the language itself, and the use of JIT compilers to increase the range of platforms it is capable of running on.

March 25, 2008 1pm, Room 701 Claremont Tower
``The Talking Sink'': Automated Assistance for Persons with Dementia.
Jesse Hoey, University of Dundee.

In this talk, I will present a real-time system fo assisting persons with dementia during handwashing, an important activity of daily living that often poses difficulty with this population. The system uses only video inputs, and assistance is given as either verbal or visual prompts, or through the enlistment of a human caregiver's help. The system must trade off the competing objectives of getting the user's hands clean, reducing caregiver burden, and preserving user feelings of independence. The objectives, actions and video observations are modeled simultaneously with a probabilistic, decision theoretic model, specifically a partially observable Markov decision process, or POMDP. The key strengths of the POMDP are that it is able to deal with uncertainty and multiple, long-term objectives, and that it is able to learn and adapt to user characteristics and context by observing behaviour. I will introduce POMDPs and I will discuss how non-invasive sensing devices such as cameras can be integrated into this model. I will discuss the specific handwashing model, I will show results from an eight week user trial conducted in 2007. I will conclude by showing a sample of other applications that use the same decision theoretic framework, and will discuss the work yet to be done to make this type of system ubiquitous.

February 26, 2008 2pm, Room 701 Claremont Tower
"Evidence-based Development"
Dr Jeremy Dick, integrate systems engineering ltd

Evidence-based Development (EbD) addresses the challenge of achieving progressive assurance of the fitness-for purpose of high-integrity systems and software. Developers of complex systems are required by law, by standards and by customers to provide evidence that their products are fit-for-purpose. While the system is being designed, systems engineers are required to supply evidence in the form, for example, of safety cases, design justifications and compliance statements for review and sign-off. While the system is being built and tested, further evidence of the verification process has to be gathered and presented. While in operation, evidence for the correct functioning of the system may be required. Finally, evidence should be provided that the system may be disposed of safely at the end of its useful life. To meet these challenges frameworks, processes and tools are required that help coordinate and organise the collection, review and publication of validation and certification evidence. EbD supplements existing development processes with information structures and processes that contribute to progressive assurance. It does not replace any of the wide variety of existing analysis and modelling techniques - rather, it acts as a broker for the collection of evidence from those already in use. In effect, EbD provides an evidential back-bone for progressive assurance, capturing a growing body of evidence for the correctness of a system, starting from the earliest possible stages with rationale associated with the verification of design intention against requirements, through to the fulfilment of the design and associated test results. It is a uniform approach to argumented verification and validation. The talk will describe EbD, review its origins and relationships to other techniques, and demonstrate DOORS/Traceline, a tool designed to support it.

February 21, 2008 2pm, Room 701 Claremont Tower
Formal development of fault tolerant systems by refinement Elena Troubitsyna, Åbo Akademi University, Turku, Finland
Elena Troubitsyna

Modern software-intensive systems are usually complex and prone to errors of various natures. To achieve high degree of dependability of such systems we should integrate formal development methods with the techniques for fault tolerance. Formal refinement-based methods provide us with the powerful design techniques enabling development of systems correct by construction. Meanwhile, techniques for achieving system fault tolerance give us the means to cope with failures of physical components and certain design mistakes. In this talk I will overviews some advances in specification and refinement of complex fault tolerant systems. In particular, I will present a general formal specification pattern that can be recursively applied to specify fault tolerance mechanisms at each architectural layer of a control system. Iterative application of this pattern via stepwise refinement enables development of a layered fault tolerant system correct by construction. I will also briefly describe our approach to formal model-driven development of complex communication systems.

February 12, 2008 1pm, Room 701 Claremont Tower
Autonomic QoS control in enterprise Grid environments using online simulation
Samual Kounev

As Grid Computing increasingly enters the commercial domain, performance and Quality of Service (QoS) issues are becoming a major concern. The inherent complexity, heterogeneity and dynamics of Grid computing environments pose some challenges in managing their capacity to ensure that QoS requirements are continuously met. The talk will present a comprehensive framework for autonomic QoS control in enterprise Grid environments using online simulaton. The framework includes a novel methodology for designing autonomic QoS-aware resource managers that have the capability to predict the performance of the Grid components they manage and allocate resources in such a way that service level agreements are honored. Support for advanced features such as autonomic workload characterization on-the-fly, dynamic deployment of Grid servers on demand, as well as dynamic system reconfiguration after a server failure is provided. The goal is to make the Grid middleware self-configurable and adaptable to changes in the system environment and workload. The approach is subjected to an extensive experimental evaluation in the context of a real-world Grid environment and its effectiveness, practicality and performance are demonstrated.

February 5, 2008 1pm, Room 701 Claremont Tower
Cryptographic Protocol Composition
Joshua Guttman, The MITRE Corporation

Cryptographic Protocol Composition via the Authentication Tests Joshua Guttman The MITRE Corporation Compositionality results for cryptographic protocols say that they still achieve the same security goals, even after some change. We provide here compositionality results based on the completeness of the authentication tests. The authentication tests are a pair of principles that say what must have happened in an execution, given that a particular message component occurs in a transformed form. We give first a new proof of a known compositionality result. If a new protocol transforms a disjoint set of cryptographic values from those used in an existing protocol, then the existing protocol still achieves the same security goals as when it was the only protocol in use. Its security goals are independent of the addition of the new protocol. A new compositionality result concerns a form of protocol refinement. Suppose a protocol is refined by possibly adding more messages, and possibly providing more detail about the messages sent in existing steps. If those message components that participate in authentication tests used by the original protocol undergo no new transformations after refinement, then all its security goals are preserved under the refinement. Examples illustrate the utility of these results.

January 29, 2008 1pm, Room 701 Claremont Tower
Attacking IPsec in Encryption-only Configurations
Kenny Paterson (ISG, Royal Holloway, University of London)

Title: Attacking IPsec in Encryption-only Configurations Abstract: We describe attacks breaking implementations of IPsec making use of encryption-only ESP in tunnel mode. The attacks are both efficient and realistic: they are ciphertext-only and need only the capability to eavesdrop on ESP-encrypted traffic and to inject traffic into the network. We report on our experiences in applying the attacks to a variety of implementations of IPsec. Joint work with Arnold Yau and Jean Paul Degabriele.

January 22, 2008 1pm, Room 701 Claremont Tower
Designing Systems for Dependability and Predictability
Richard West, Associate Professor

It's been argued that academic systems research i irrelevant but would you be happy with your Windows system in 10 years? Is virtualization the answer to all our troubles? This talk argues that while there are numerous systems for server, desktop and embedded platforms, as well as hypervisors and VM kernels for machine virtualization, several key aspects are still missing from today's OSes. Specifically, I will outline three aspects of today's OSes that are problematic: (1) a semantic gap exists between application needs and system service provisions, (2) time is not a first-class resource, and (3) existing systems all suffer from a static structure, be it monolithic or micro-kernel based. Time-permitting, I will focus on two case studies that address the problems of time-management in Linux, and also the notion of "mutable protection domains" (MPDs). MPDs effectively adapt isolation boundaries between component services to trade dependability for predictability of service execution.

December 6, 2007 2pm, Room 701 Claremont Tower
Real-time Program Algebra
Prof. Ian J. Hayes, University of Queensland

We start from the algebra of regular expressions (Kleene algebra) and look at extensions to give one an algebra for programs. This involves using primitives of assignments, tests and assertions, as well as adding operators to handle infinite iteration. We look at ways to represent important concepts like loop invariants and variants (although we treat the later via well founded relations). The algebra allows one to prove properties like Hoare's "axiom" for loops straightforwardly. For real-time programs infinite iteration becomes much more interesting: we want control programs that (conceptually at least) execute forever. We look at rules for reasoning about possibly infinite iterations, and concepts like non-Zeno behaviour of programs.

November 29, 2007 1pm, 701 Claremont Tower
Contract Related Agents
Keith Clark

We describe a multi-threaded declarative agent architecture in which an agent's relationships to other agent's is defined by a set of formal contracts, held inside the agent. Some of these contracts determine services that the agent provides, others are outsourcing contracts for services that other agents provide for it. The contracts are declaratively formalised as event calculus rules. At any time point the state of a contractual relationship is determined by the contract rules /and/ the events that have previously happened pertinent to the contract. The contracts specify which agents are allowed to notify which events. They also specify conditions under which particular events initiate or terminate an obligation on one the agent parties to the contract. Initiated obligations may have deadlines by which they must be discharged. A contract can also specify conditions under which an agent is considered to have violated the contract with respect to some obligation. An initiated obligation typically results in the selection and execution of a plan to discharge the obligation. Such a plan may in turn query the agent's other contracts to determine if they can be used to outsource some sub-goal of the plan. For concreteness we give the rules for a single agent contract for a patrol robot, and the rules for multi-task service contract between a pair of agents in which tasks have maximum completion times and payments related to completion time.

November 14, 2007 2pm, Room 701
Algebraic Reasoning for Probabilistic Programs
Larissa Meinicke, Åbo Akademi (Turku, Finland)

Algebraic methods have been used successfully to reason about transformation rules for standard (i.e., non-probabilistic) programs which may include demonic non-determinism. For example, - Kozen and others have used the algebra of regular expressions, Kleene algebra, extended with tests to reason about compiler optimisations in a partial correctness framework, - Back and von Wright have applied algebraic reasoning t verify data refinement theorems, and separation and reduction rules for action systems in a total correctness framework, and - Cohen has used algebraic methods to develop and verify generalised separation and reduction theorems in a partial correctness framework. Probabilistic programs, programs in which probabilistic choices may be made, have applications in areas such as distributed computing, and reliable systems modelling. They may also be preferable over other non-probabilistic algorithms for efficiency reasons. It is my belief that transformation theorems may be used to assist in the development and analysis of probabilistic programs, just as they have proven to be useful in a non-probabilistic context. In recent work I have investigated how algebraic methods may be applied to reason about probabilistic programs in a total correctness framework. In this talk I will give an overview of the results of my investigation, and other related work which has been performed on this topic. In particular I will discuss the algebraic dissimilarities and similarities between standard and probabilistic programs, and how these commonalities and discrepancies effect the transformation theorems which apply to these different kinds of programs.

November 1, 2007 1pm, Room 701 Claremont Tower
A System Development Process with Event-B and the Rodin Platform (a non-technical talk)
Jean-Raymond Abrial

After very short introductions to Event-B and the Rodin platform, I will present the main cause of the difficulty to transfer this approach to industry, namely its incorporation within the industrial development process. I'll remind what is meant by an "industrial development process" and point to the reluctance to change it. Then, I indicate where the Event-B process has to be inserted. This is followed by a description of what is typical in the Event-B development process and how the Rodin platform can help following it. Time permitting, I will present a short demo.

October 23, 2007 1pm, 701 Claremont Tower
Visualisation and Animation of complex systems
Mike Martin

In the mid to late '80s we were inventing the first middleware which sat between proprietary operating systems and enterprise applications. We came across the problem of how to explain and demonstrate stuff that was supposed to remain invisible because it was infrastructure. One idea, originated by Andrew Herbert who was leading the ANSA project at the time, was that of using "projections" to provide distinct frames in which to articulate different aspects of the system. The DEMON project (Distributed Environment MONitor) operationalised these ideas by building a tool for simultaneously visualising the different projections and animating their respective behaviours using real time instrumentation and systems diagnostic logs. What goes around, comes around.The "middle" has moved and is now between the back office applications and the access channels. It is even between independent partner systems in virtual organisations and public service partnerships. And the problem of explaining and demonstrating issues of control, confidentiality and governance, in ways that can be understood by non technical users, has become even more acute. In the Social and Business Informatics Group we have re-implemented a DEMON like platform and developed a set of techniques for participative design and co-production of organisational systems and infrastructure. In this approach, projections are not just applied to the technical system but also to address the need to provide "mirrors" in which participants can see and recognise their own practice and "windows" through which they can observe and engage (and struggle) with each others concerns, values and interests in the co-construction of policies, plans and systems. In this colloquium we will demonstrate the "demonstrator" and explore how it is being used in a number of contexts and projects ranging from GOLD concerned with the creation of infrastructure for virtual organisations to OLDES which is creating tele-medicine and tele-accompany environments for the vulnerable elderly.

October 19, 2007 1.00pm, 701 Claremont Tower
Software Copyrights, Patents, and Free Software
Robert Dewar

Abstract This talk will examine the general issue of how copyrights and patents work, with specific reference to software. We will examine in detail the concept of free software, and the problems that copyright and patent issues present in this context. No previous knowledge of the legal issues is assumed. These issues are of tremendous importance to the future of software development, and potentially affect everyone involved in the software field, both creators and users. Robert Dewar is an Emeritus Professor of Computer Science at the Courant Institute of Mathematical Sciences at New York University. He is past chair of the department, and past associate director of the institute. His research fields include compilers and programming languages, operating systems, and microprocessor architectures. He is an expert in the technical aspects of patent and copyright law, having served as an expert witness in several US Federal trials. He is also the President and CEO of Ada Core Technologies, a company that specializes in providing large scale systems for development of critical systems using Ada Technology. Ada Core Technologies provides all its software using Free Software/Open Source licenses.

October 12, 2007 1pm, 701 Claremont Tower
User-Centered Security: Stepping Up to the Grand Challenge
Mary Ellen Zurko

User-centered security has been identified as one of the four grand challenges in information security and assurance. In other words, the best minds in security think making it usable is both difficult and important. User-centered security is on the brink of becoming an established subdomain of both security and HCI research, and an influence on the product development lifecycle for any end user facing application, from email to Web 2.0 mashups. As practitioners and researchers in security and HCI, we still face major issues when applying even the most foundational tools used in either of these fields across both of them. I will discuss the systemic roadblocks to effective user-centered security that I see as most important. They fall into three categories: social, technical, and pragmatic. The social challenges are the most difficult to address, because there is no obvious constituency that will address them. The other two categories, technical and pragmatic challenges, are naturally attacked by researchers and developers, although they were previously overlooked because they crossed expertise boundaries. While security and uability have historically often been at odds, both rely on the reality of deployment to prove the utility and validity of their work. There is a lot of interesting and important work for teams innovative enough to not just cross those boundaries but actually synthesize security and HCI. I'll also touch on the techniques and principles that I believe are producing (more) effective usable security today. Mary Ellen Zurko leads security architecture and strategy for Lotus Workplace, Portal, and Collaboration Software at IBM. She defined the field of User-Centered Security in 1996. She is on the steering committee for New Security Paradigms Workshop and the International World Wide Web Conference series. She has worked in security since 1986, at The Open Group Research Institute and Digital Equipment Corporation, as well as IBM. She is a contributor to the O'Reilly book "Security and Usability: Designing Secure Systems that People Can Use." Her vita is at http://mysite.verizon.net/resqwf60/id1.html.

July 31, 2007 1pm, 701 Claremont Tower
TBC
Robert Shaw

TBC

July 12, 2007 1pm, 701 Claremont Tower
Towards the integration of Performance Engineering and Software Engineering - some different ways to success (or maybe not) in SPE
Carlos Juiz

Software and Performance Engineering (SPE) is a particular research topic that was developed in last 20 years...however it has not arrived to maturity due to number of methodologies, techniques and tools devoted to this discipline and its reduced critical mass of researchers. The seminar will overview by example some of these methodologies, techniques and tools through simple examples in order to understand the state-of-art and the near future in SPE.

May 30, 2007 1pm, 701 Claremont Tower
Baltic: Service Combinators for Farming Virtual Machines
Andrew D. Gordon

Based on joint work with Karthikeyan Bhargavan, Microsoft Research and Iman Narasamdya, University of Manchester We consider the problem of managing server farms largely automatically, in software. Automated management is gaining in importance with the widespread adoption of virtualization technologies, which allow multiple virtual machines per physical host. We consider the case where each server is service-oriented, in the sense that the services it provides, and the external services it depends upon, are explicitly described in metadata. We describe the design, implementation, and formal semantics of a library of combinators whose types record and respect server metadata. Our implementation consists of a typed functional script built with our combinators, in control of a Virtual Machine Monitor hosting a set of virtual machines. Our combinators support a range of operations including creation of virtual machines, their interconnection using typed endpoints, and the creation of intermediaries for tasks such as load balancing. Our combinators also allow provision and reconfiguration in response to events such as machine failures or spikes in demand. We describe a series of programming examples run on our implementation, based on existing server code for order processing, a typical data centre workload. To obtain a formal semantics for any script using our combinators, we provide an alternative implementation of our interface using a small concurrency library. Hence, the behaviour of the script plus our libraries can be interpreted within a statically typed process calculus. Assuming that server metadata is correct, a benefit of typing is that various server configuration errors are detected statically, rather than sometime during the execution of the script.

May 22, 2007 2pm, 701 Claremont Tower
Test-data Generation by Proof
Ana Cavalcanti

Many tools can check if a test set provides control coverage; they are, however, of little or no help when coverage is not achieved and the test set needs to be completed. In this seminar, we describe how a formal characterisation of a coverage criterion can be used to generate test cases; we present a procedure based on traditional programming techniques like normalisation, and weakest precondition calculation. They are a basis for automation using an algebraic theorem prover. In the worst situation, we are left with a specification of the compliant test sets.

May 15, 2007 2pm, 701 Claremont Tower
Artificial Biochemistry
Luca Cardelli

Systems Biology is a new discipline aiming to understand the behavior of biological systems as it results from the (non-trivial, "emergent") interaction of biological components. In addition to analyzing existing biological networks to understand their function, it is also important to understand from the ground up what simple networks of interacting components "can do". That investigation can be carried out in abstract "artificial" frameworks, as long as the ground rules are kept close enough to the ones of biochemistry. We discuss some biologically inspired networks that are characterized by simple components, but by complex interactions. Subtle and unexpected behavior emerges even from simple circuits, and yet stable behavior emerges too, giving some hints about what may be critical and what may be irrelevant in the organization of biological networks.

May 8, 2007 2pm, 701 Claremont Tower
In Silico Biology, or On Comprehensive and Realistic Modeling
David Harel

The talk shows the way software and systems engineering, especially of reactive systems, can be applied beneficially to the life sciences. We will discuss the idea of comprehensive and realistic computerized modeling of biological systems. In comprehensive modeling the main purpose is to understand an entire system in detail, utilizing in the modeling effort all that is known about the system, and to use that understanding to analyze and predict behavior in silico. In realistic modeling the main issue is to model the behavior of actual elements, making possible totally interactive and modifiable realistic executions/simulations that reveal emergent properties. I will address the motivation for such modeling and the philosophy underlying the techniques for carrying it out, as well as the crucial question of when such models are to be deemed valid, or complete. The examples I will present will be from among the biological modeling efforts my group has been involved in: T cell development in the thymus, lymph node behavior, embryonic development of the pancreas, the C. elegans reproduction system and a generic cell model.

May 1, 2007 2pm, G21/22 Devonshire Building
Practical Verification of Java: Extended Static Checking with ESC/Java2
Joe Kiniry

The Java Modeling Language (JML) is a behavioral interface specification language for the Java programming language. Using JML, one can precisely say as little or as much as one likes about how a Java program is supposed to behave, and a whole host of tools are available to check that these promises are fulfilled. One popular tool for statically reasoning about JML-annotated Java programs is ESC/Java2. This talk will briefly review JML (and how surprisingly like Java it is, with good reason), how JML and ESC/Java2 is (wisely) used in academic and industrial contexts, and new features of recent versions of ESC/Java2 including the use multiple logics and theorem provers for automatic verification. Mention will also be made of other tools that exist to document, runtime check, and prove that assertions about programs hold. Joseph Kiniry is a Lecturer in Computer Science in UCD Dublin, having previously worked extensively in industry and academic research. He holds Degrees from Caltech (Ph.D. Computer Science 2002, MS Computer Science 1998), the University of Massachusetts Amherst (MS Computer Science 1995) and from Florida State University (B.S. Computer Science 1992 and B.S. Pure Mathematics 1992). Joe held a postdoc position at the Radboud University Nijmegen from 2002 to 2004. At UCD Joe's research team focuses on software engineering with applied formal methods. Joe is a major participant in several national and International research grants including the EU FP6 FET "Global Computing II" project MOBIUS and Lero: The Irish Software Engineering Research Centre. Joe has co-founded a number of technology companies and is has been a very active participant in the Free/Libre/Open Source Software movement since the late 1980s. In 1994-1995 he was Senior Research Engineer at the Open Software Foundation Research Institute. Over the past fifteen years he has performed high-level consulting in several domains including applied formal methods, rigorous software engineering, software and system security, and electronic and Internet voting.

April 24, 2007 2pm, 701 Claremont Tower
Autonomic Management of Ubiquitous Systems for e-Health
Emil Lupo

Management in pervasive systems cannot rely on human intervention or centralised decision making functions. It must be devolved, based on local decision making and provide local autonomy for collections of devices. We introduce the concept of a Self-Managed Cell (SMC) as a basic architectural pattern for building autonomous pervasive systems. Although initially aimed at the design of body area networks for health-monitoring, SMCs may also be applied in other contexts such as unmanned vehicles, building management systems and larger distributed systems settings. The SMC pattern is based on an extensible set of loosely coupled services and implements a policy- driven mechanism for adaptation and feedback control. In order to scale to larger environments SMCs must be able to collaborate with each other in a peer-to-peer manner and compose into larger autonomous cells. To support SMC interactions we introduce abstractions that permit constrained exchanges of data, events and policies.

Dr. Emil Lupu is a Senior Lecturer in the Department of Computing at Imperial College London where he leads several research projects in the areas of pervasive computing, trust and security and policy-based network and systems management. He has over 60 publications and serves on the program committee of several international conferences in these areas. Dr. Lupu was program co-chair of the IEEE Enterprise Distributed Object Computing Conference in 2001 and of the IEEE Workshop on Policies for Distributed Systems and Networks in 2001 and 2004. See http://www.doc.ic.ac.uk/~ecl1 for further details and selected publications.

April 17, 2007 2pm, 701 Claremont Tower
Modelling Biochemical Signalling Pathways: concurrency meets the life sciences
Muffy Calder

Yes, this really is a Computing Science seminar!

I will investigate how theories and tools from Computing Science can be used to model and reason about signal transduction pathways -- the fundamental pathways that control important cell responses such as growth, movement, and apoptosis (cell) death. The key idea is that pathways have a stochastic, computational content.

In the talk, I use the stochastic process algebra PEPA, and the model checker PRISM, to develop and analyse a number of novel, predictive models for parts of the ERK pathway. I will discuss why these new models are sound with respect to traditional ODE (differential equation) models, what the biologists say about them and the implications for Computing Science. The work is in collaboration with Cancer Research UK.

No prior knowledge of biochemistry will be assumed!

March 27, 2007 2pm, 701 Claremont Tower
Commitment is hard
Eerke Boiten

This talk presents a reconstruction of the cryptographic primitive of "commitment". Starting from an abstract informal characterisation, all of its usual properties appear. Along the way, there are some convincing arguments that the traditional formal methodists' toolbox won't work for proving correctness (a.k.a. security) in this context ... but can we avoid proofs (by contradiction) over all probabilistic Turing machines in the end?

About the speaker:

Eerke Boiten is a senior lecturer at the University of Kent. All of his research has been in "formal program development", variously from the angles of program transformation, viewpoint specification, and formal methods, particularly refinement. This academic year he is on study leave, looking at the interface between formal methods and the "mathematics of program construction" on the one hand, and cryptography on the other.

March 20, 2007 2pm, 701 Claremont Tower
Autonomic Query Parallelization using Non-dedicated Computers: An Evaluation of Adaptivity Options
Norman Paton

Writing parallel programs that can take advantage of non-dedicated processors is much more difficult than writing such programs for networks of dedicated processors. In a non-dedicated environment such programs must use autonomic techniques to respond to the unpredictable load fluctuations that prevail in the computational environment. In adaptive query processing (AQP), several techniques have been proposed for dynamically redistributing processor load assignments throughout a computation to take account of varying resource capabilities. This talk presents a simulation-based evaluation of these autonomic parallelization techniques in a uniform environment and compares how well they improve the performance of the computation. Three published strategies are compared with two new algorithms that seek to overcome some weaknesses identified in the published approaches. In addition, we explore the use of techniques from online algorithms to provide a firm foundation for determining when to adapt in two of the existing algorithms. The evaluations identify situations in which each strategy may be used effectively and in which it should be avoided.

March 13, 2007 2pm, 701 Claremont Tower
New Media is Dead
Ian Forrester & Matthew Cashmore , BBC Backstage

Ian Forrester and Matthew Cashmore talk about why the New Media world is Old Hat. With more people taking control of how they consume, precipitate and create vast amounts of data and media, they will explore how this New World presents a New Challenge for people in the creative industries.

How can the BBC be a part of this new world? Is the Alpha Geek now calling time on the mega corporations, and how will mash-ups, networked apps and new social patterns of behaviour impact on the daily lives of the average users.

Ian Forrester heads up the BBC's Backstage, a developer/designer network like no other. He's well known for geek social events across the capital including London Geekdinners, BarCampLondon, BBC Backstage London Christmas Bash and recently the BarCampLondon2.

Previously, he worked for the BBC World Service as a New Media Software Engineer. His background is in design and information architecture, which stems from lecturing at Ravensbourne College and working for a design agency during the dot-com era.

Somehow, Ian finds time to blog at cubicgarden.com and think about the next generation of the web at his new blog called flow *

February 27, 2007 2pm, 701 Claremont Tower
Trading assertions in the verified software repository
Jim Woodcock

The recent re-examination of Mondex generated over 2,000 refinement verification conditions discharged amongst four theorem provers. These assertions are to be curated in the verified software repository, and this raises the question of whether such assertions can be traded between different theorem provers. One of the immediate problems to be addressed is in resolving the different treatments of undefinedness. We discuss how classical logic can be used to prove and to refute conjectures in monotonic partial logics, such as those used in the Mondex experiment.

February 21, 2007 12pm, 701 Claremont Tower
A Brief Introduction to the RODIN platform.
Farhad Mehta

One of the aims of the RODIN project is the development of an open and industrial platform for modeling discrete event systems using refinement and proofs. This will be a non-technical talk on the objectives and design of the RODIN platform with emphasis on how it eases the task of 'correct by construction' system development. The talk will include a demonstration of its current capabilities and use of its modeling and proving interfaces.

February 20, 2007 2pm, 701 Claremont Tower
Verifying a Hotel Key Card System
Tobias Nipkow

Most hotels operate a digital key card system. Inspired by a formalization of this system by Daniel Jackson in Alloy, I will present two related models of this key card system: a state based and a trace based one. Both are defined, verified, and proved equivalent in the theorem prover Isabelle/HOL. It is shown that if a guest follows a certain safety policy regarding her key cards, he can be sure that nobody but him can enter his room. Finally I will report on attempts to translate inductive definitions into a form that allows efficient Alloy-style model checking with SAT solvers.

February 6, 2007 2pm, G21/22 Devonshire Building
How does the brain compute?
Jim Austin

There have been many theory’s of how the brain may compute, none have been successful. This talk introduces a possible approach to this problem that is motivated from work on computer architectures an on work on binary neural networks over 20 years. What this tells us is that the abstraction used in computer architectures may be a promising level to describe the general function of the brain. The approach is based on understanding the principles of brain function, rather than how it is exactly wired. This may provide a sufficient level of description that allows computer scientists to build better computing systems and neurobiologists better get to grips with the detailed brain operation.

This talk will overview the approach and outlines a number of basic principles that the brain may use in its every day life.

Jim Austin Advanced Computer Architectures Group Computer Science York.

January 26, 2007 1pm, 701 Claremont Tower
Calligraphic User Interfaces:towards more usable CAD systems
Joaquim Jorge

CAD systems possessing great functionality now enable us to manufacture complex geometric models. However, computers have yet to become usable at the very early stages of product design, where pencil and paper still reign. This is because present-day systems, with their focus on internal representation and dialogue hierarchies, require designers to leap large conceptual gaps from their mental image of a desired object to the geometric model that formally expresses its shape. As computers become more sophisticated and powerful, alternative input modalities and interface techniques are emerging which form the basis for a new generation of sketching applications supporting what we call Calligraphic Interfaces, where artificial dialogue constraints imposed by the previous generation of UIs are removed. We are exploring with minimalist approaches and techniques to approximate traditional methods including modeling, illustration and retrieval. I will talk about ongoing research and projects at the Technical University of Lisbon, towards this goal.

January 23, 2007 2pm, 701 Claremont Tower
Provenance: an open approach to experiment validation in e-Science
Luc Moreau

The importance of understanding the process by which a result was generated in a computation is fundamental to science, engineering or business. For example, without such information, other scientists cannot reproduce, analyse or validate experiments. Likewise, businesses must demonstrate their systems' results were produced in a regulatory-compliant manner. Provenance is therefore important to enable users to trace how a particular result has been arrived at.

Based on the common sense definition of provenance, we propose a new definition of provenance that is suited to the computational model underpinning service-oriented architectures: the provenance of a piece of data is the process that led to the data. Since our aim is to conceive a computer-based representation of provenance that allows us to perform useful reasoning about the origin of results, we examine the nature of such representation, which is articulated around the documentation of execution.

We then examine the architecture of a provenance system, centered around the notion of a provenance store designed to support the provenance lifecycle: during a recording phase some documentation of execution is archived in the provenance store, whereas a reasoning phase operates over the archived documentation. Then, we successively discuss a protocol for recording execution documentation, a query facility to gain access to the contents of the store, and a reasoning system to make inferences. The realisation of such an architecture is particularly challenging in the presence of e-Science experiments since it must be scalable.

The presentation will draw upon our experience in the PASOA (www.pasoa.org) and EU Provenance (www.gridprovenance.org) projects and will rely on explicit use cases derived from e-Science applications in the domain of bioinformatics, high energy physics, organ transplant management and aerospace engineering.

December 19, 2006 2pm, 1.19 Claremont Tower
Aspectizing Design Patterns and Exception Handling: The Devil is in the Details
Alessandro Garcia

It is usually assumed that the implementation of certain kinds of crosscutting concerns can be always better modularized by the use of aspect-oriented programming (AOP). Exception handling and several well-known design patterns are often cited in introductory AOP texts as the "killer applications" of aspect-orientation. However, there is no empirical evidence about the scalability of AOP in more realistic scenarios, such as aspectual composition of design patterns and aspectization of heterogeneous forms of exception handling. This talk will present the results and conclusions of two in-depth investigations of the adequacy of the AspectJ language for modularizing error handling and design patterns. The studies consisted in refactoring a number of existing realistic applications so that the code responsible for implementing compositions of design patterns and complicate error recovery strategies were moved to separate aspects. The case studies are based on distinct application domains, including a CVS plugin, a web-based information system, a reflective middleware, and a measurement tool. We have performed quantitative assessments of several systems based on five fundamental modularity attributes, namely separation of concerns, coupling, cohesion, interface simplicity, and conciseness. Our investigation also included a multi-perspective analysis of the refactored systems, including (i) the reusability of the aspectized code, (ii) the beneficial and harmful aspectization scenarios, and (iii) the scalability of AOP in the presence of complex aspect interactions.

Dr. Alessandro Garcia (http://www.comp.lancs.ac.uk/computing/users/garciaa/ ) is a Lecturer in the Computing Department at Lancaster University. His main research interests are in the areas of aspect-oriented software development, empirical software engineering, software architecture, software metrics, multi-agent systems, and exception handling. He is particularly interested in the investigation of the fundamental properties underlying aspect-oriented design and in their experimental assessment. His recent research has focused on studying the interplay between aspects and software architecture assets. He has recently completed his PhD research, in which he has defined a metrics suite for AOSD and an aspect-oriented framework for developing multi-agent systems. In the last years he co-authored 8 journal/magazine papers, 4 books, 8 book chapters and 40 conference/workshop papers in the areas mentioned above. He has served the AOSD.06 Program Committee and taught tutorials related to AOSD in premier conferences in software engineering, such as ICSE and ICSR. Finally, he is actively involved in three research projects: AOSD-Europe (European Network of Excellence on AOSD), AMPLE - (Aspects, Models, and Product Lines), and TAO (a Testbed for AOSD).

October 31, 2006 2pm , 701 Claremont Tower
Communication about Security of Communication: the e-Voting Debate in the Netherlands
Wolter Pieters

In many countries, electronic voting had already become a controversial topic years ago. The Netherlands, one of the early adopters of offline systems, had been relatively immune to the international scrutiny, even when the Irish refused to use their newly bought Dutch machines in their elections. This summer, however, a major campaign against e-voting was initiated in the Netherlands as well. Close to the November general elections, the leaders of this campaign demonstrated how to manipulate the Nedap machines used in 90% of the districts. This triggered responses by both government and manufacturer, saying on the one hand that there is no severe problem, but on the other hand that security will be improved.

In such a situation of controversy, both proponents and opponents of e-voting often defend their positions in terms of “actual security” versus “perceived security”. It is then said that the machines are actually (in)secure, the facts of which fail to get through to the people on the other side of the controversy. Moreover, such terms are often used in scientific papers analysing the social acceptance of voting technology. It is then argued that the public’s trust should be understood as based on perceived security, as opposed to the actual security of the system.

In this presentation, I sketch both the current e-voting debate in the Netherlands, and the problems that are created by the use of the distinction actual/perceived security in such controversies. I also provide alternative distinctions, which I consider to be more useful. For this purpose, I draw on the work of important thinkers such as Niklas Luhmann and Bruno Latour. I use these distinctions in order to try to explain what happened in the Dutch e- voting history.

More information: http://www.cs.ru.nl/~wolterp http://www.wijvertrouwenstemcomputersniet.nl/English

October 17, 2006 2pm, G21/22 Devonshire Building
Dynamic Binary Translation: The Key to a Flexible World
Martyn Spink

The purpose of this talk is to introduce you to the most amazing software in the world today.

Initially there will be a demonstration of Apples Rosetta solution (http://www.apple.com/rosetta/) which was based on the QuickTransit technology developed by Transitive Limited (http://www.transitive.com/customers/apple.htm).

The presentation will cover a brief history of the technology intertwined with details about the technology itself. It will conclude with a look at some ways in which the technology could be deployed today which should open the door for some interesting discussion.

Martyn Spink VP Engineering Transitive Limited

August 10, 2006 2pm, 701 Claremont Tower
The challanges of network delivered services
Dr Graeme Dixon

There is an industry trend away from packaged applications installed on customer-owned machines to network delivered applications -- the term commonly used to describe this trend is software as a service (or SaS). This talk will discuss the issues around enabling SaS -- issues that range from the mundane (e.g. software packaging) to the complex (e,g, resource optimization and workload management). The context for this work is the development of a service delivery platform for next-generation applications being developed within IBMs service delivery division.

July 25, 2006 2pm, 701 Claremont Tower
The Rely-Guarantee Method in Isabelle/HOL
Leonor Prensa

In this talk I will present my work on the formalization of the rely-guarantee method in the theorem prover Isabelle/HOL. This method consists of a Hoare-like system of rules to verify concurrent imperative programs with shared variables in a compositional way. Syntax, semantics and proof rules are defined in higher-order logic. Soundness of the proof rules w.r.t. the semantics is proven mechanically. Also parameterized programs, where the number of parallel components is a parameter, are included in the programming language and thus can be verified directly in the system. The system is proved to be complete also for parameterized programs. Finally, I will show by an example how the formalization can be used for the verification of concrete programs.

July 18, 2006 2pm, 701 Claremont Tower
Trusting in a convergent world: a promise of Trust Enhancing Technologies
Piotr Cofta

The subject of trust evokes significant emotions as it brings expectations of harmonious society, low-friction economy, and better personal relationship. However, convergent communication over distance has deprived us from our ability to assess trust in face to face communication, making trusting a complicated task. It is not only harder to convey traditional signals of trustworthiness, but it is increasingly considered imprudent to take for granted what has been communicated e.g. over the Internet.

The technology ability to distort and discontinue existing social constructs can be hopefully in a long run matched by our social ability to re-create core relationships by creatively (ab)using such technology. However, instead of waiting for the society to adjust itself to the technology it is of greater benefit to already alter technological properties in such way that they facilitate the development of social virtues.

The talk demonstrates how two dimensions of trust (associated with proper trust and with control-based trust) are combined into a single complexity-driven model of confidence. From there, the concept of Trust Enhancing Technologies (TET) is introduced as a set of technological features that may potentially improve our ability to develop trust and confidence over distances. The proposed set of TET properties and a preliminary group of constructs related to TET is discussed together with a number of examples taken from existing systems.

Piotr Cofta Chief Researcher, Security and Trust BT

Piotr Cofta works for British Telecom as a Chief Researcher, Security and Trust in the Mobility Research Centre. He is responsible for research in convergent security and trust, specifically in identity and privacy. Previously he has been working for many years for Nokia and more recently for Media Lab Europe, concentrating on device security and transactional trust. His research interest includes technical and social aspects of security and trust with special focus on opportunities in convergent environment and mobile commerce. He received his PhD in computer science from the University of Gdansk, Poland. He is a member of IEE and IEEE. Dr Cofta is a contributor to several international standards; he publishes and speaks frequently. You can contact him at piotr.cofta@bt.com or at http://piotr.cofta.co.uk

July 11, 2006 12.30pm, G21/22 Devonshire Building
Improving Model Driven Architecture through Formal Methods
Iman Poernomo

Model Driven Architecture (MDA) is a methodology based on the Meta Object Framework (MOF) to develop software by means of successive refinements from abstract platform-independent models to concrete platform-specific models. The purpose is to promote a clear demarcation of abstract architecture and implementation-specific issues. Central to MDA is the ability to define transformations as mappings between metamodels. Such transformations are powerful, providing a systematic means of model refinement. They are also dangerous: a single error in a transformation mapping can result in the systematic introduction of a range of errors in a resulting model. This talk explores a way of solving this problem through a formalisation of metamodel transformations within logical type theory.

July 3, 2006 2pm, 1.18 Claremont Tower
Belief in Information Flow
Michael Clarkson

Quantitative information-flow security policies, such as at most k bits leak per execution of the program," allow information flows at restricted rates. Such policies are useful when analyzing programs whose nature requires that some---but not too much---information be leaked.

This talk will describe recent work on reasoning about quantitative information flow. A new model is developed that describes how attacker beliefs change due to the attackers observation of the execution of a probabilistic (or deterministic) program. The model enables compositional reasoning about information flow from attacks involving sequences of interactions. The model also supports a new metric for quantitative information flow that measures accuracy of an attackers beliefs. Applying this new metric reveals the inadequacies of traditional information flow metrics, which are based on reduction of uncertainty. The new metric can also be used to reason about misinformation; deterministic programs are shown to be incapable of producing misinformation. In addition, programs in which nondeterministic choices are made by insiders, who collude with attackers, can be handled.

Joint work with Andrew Myers and Fred B. Schneider

May 24, 2006 2pm, 701 Claremont Tower
P3 – a homeostatic environment for persistent and distributed computation on POSIX clusters.
Mark ONeill

P3 is portable cluster computing environment which has been designed to provide a homeostatic environment for coarse grained parallel computations (e.g. databases). P3 borrows many ideas from biological systems. For example, it the P3 environment permits processes to migrate within a clustered environment to those nodes capable of offering them optimal support (in terms of disk, processing speed, specialist devices etc). P3 also supports direct peer-to-peer communication with running processes. An authenticated user or process can request a terminal-like interface to a running process on the fly and then make status enquiries, change parameters or plug new code into the (running) process using this interface. P3 also support shared heaps. These are persistent objects which may be concurrently mapped into the address spaces processes which may be running on different hosts. Lastly, P3 supports and encourages associating processes with names rather than PIDs: this can greatly simplify process management within a network/cluster environment.

The P3 system is implemented in ANSI-C and is POSIX compliant. This means that it is easy to port P3 to almost any modern variant of UNIX or UNIX-like operating system. Currently, ports exist for Linux, FreeBSD, Solaris, Darwin and Cygwin. To date, only Linux and FreeBSD, the primary development environments, are capable of supporting the P3 environment in its entirety. The P3 system facilitates the development of complex multi-process and multi-host computations by emulating colonies of homeostatically regulated organisms. P3 has been used to write applications in the areas of computational neuroscience, neuroinformatics and digital photogrammetry. P3 is an especially useful tool in the implementation of long running persistent distributed computations by providing standardised interfaces and environmental support for:

 Direct communication with running processes.  Attaching (and detaching) dynamic functionality.  Mapping shared objects (shared heaps) into the address spaces of multiple processes.  Delivering network-wide signals within a distributed computing environment.  Process checkpointing and migration (via either the MOSIX-2 or CHPOX packages)  Access authentication to resources on a per-process basis.  Process compute context migration (via the MOSIX-2 environment).  Grid capable (via MOSIX-2).

The central philosophy of P3 is each process is treated as a simple digital lifeform, responsible for maintaining its own environment. The P3 libraries provide routines which allow processes to protect valuable resources such as files areas of shared memory, and their own thread of control from accidental deletion or change and/or termination. For example, P3 processes protect their files by relinking them in response to unexpected deletion events. In P3 almost anything may be protected by a homeostat. In addition to homeostats, the P3 system also employs redundancy. For example important P3 applications may be multithreaded, so if a current process providing critical functionality is damaged or incapacitated, its function can taken over by other processes.

P3 is written in ANSI-C, is POSIX compliant and should run under any POSIX compliant UNIX or UNIX clone with minimal changes. P3 also runs in the Microsoft-NT environment (using the Cygwin libraries) and with coLinux parasites. At the present time P3 has been ported to the following systems:

 BSD 4.4 (FreeBSD)  BSD 4.4 (Darwin)  OSF1 V5.1 (TRU-64 UNIX)  Solaris 5.7 (SVR4)  Linux (including parasitic Linuxes e.g. UML or coLinux)  Cygwin

May 10, 2006 2 pm, 1.18 Claremont Tower
Specification and Verification of Reconfigurable Component Based Systems
Tom Maibaum

The problem of specifying reconfigurable systems in a declarative way is still largely an open one in the software architecture world. Almost all languages for specifying reconfiguration are operational (graph grammars, process algebras, etc) and thus reasoning about reconfiguration must be done in an, often informal, metalanguage. We use temporal logic to specify the behaviours of components and extend the language with a formalisation of connectors. The simplest connector is like an association in OO languages. Using component specifications and connector specifications, we build a coarse grained structural unit called a subsystem, which incorporates reconfiguration operations and their properties. Tom Maibaum McMaster University Department of Computing and Software

May 9, 2006 2pm, 1.18 Claremont Tower
Modelling State, Concurrency and I/O in Functional Languages
Malcolm Dowse

Two important aspects to language design are concurrency/communication and the handling of state, such as array or file system access. However, the semantics of these are traditionally given in altogether different ways - the latter often with stores and state-transformers, the former using process calculi like CCS and CSP. Language semantics is of real interest since it gives a rigorous basis for language modifications, such as new type systems or better compiler optimisations.

This talk presents a novel semantics which describes both stateful and concurrency-based aspects of languages under the same broad framework. We use this to outline a solution to the old problem of structuring side-effects in functional languages, presenting a basic language extension and semantics for deterministic I/O and concurrency in the lazy language Haskell.

April 19, 2006 2pm, 701 Claremont Tower
Internet Background Radiation as seen from the Southern Hemisphere
Ian Welch

Internet Background Radiation (IBR) is composed of unsolicited packets arriving at your network. Typical causes are scans, worms, mapping attempts or misconfiguration of other machines. This seminar looks at work on using a network telescope to collect IBR data from a New Zealand perspective. This work is part of a MSc project by Dean Pemberton who is supervised by me and Peter Komisarczuk. This talk discusses observations based upon a years worth of data (roughly 20G) and initial work on using the collected data to answer questions about the proper placement of network telescopes.

April 5, 2006 2pm, 701 Claremont Tower
Human Interaction and Collaboration in Automated and Autonomous Systems.
Peter Johnson

Current Human Factors and Human Computer Interaction paradigms are challenged by systems with increased levles of automated and autonomous components. The increased levels of agency that occur in automated and autonomous systems raise questions of awareness, intention, and trust. This requires interaction design to support joint action between people and automated and autonomous components. Examples of breakdowns in automated aviation systems are used to show how concepts supporting collaboration through increased awareness of intention lead to particular redesigns and illustrate the direction of paradigm change. The relevance of this to the development of awareness of intention and trust in autonomous systems is considered.

March 20, 2006 3pm, 701 Claremont Tower
Information-flow Security for Interactive Programs
Kevin O Neill

Information flow restrictions are intended to ensure that computer systems do not allow confidential information to leak to public users. Type systems that enforce information-flow security in imperative programs are well-known (Denning, 1976; Volpano, Smith, and Irvine, 1996), but are overly conservative in the sense that they rule out programs that, intuitively, never leak confidential information. It is therefore worthwhile to define semantic security conditions that capture standard intuitions of what information flow means.

A variety of semantic security conditions for imperative programs have been proposed, but these conditions typically restrict information flows from confidential program variables to public program variables. Such conditions are more appropriate for reasoning about "batch-job" programs (which accept inputs, perform some computation, and produce outputs) than about interactive programs that interact with real, unknown users at runtime. Furthermore, existing semantic conditions based on noninteractive models permit insecure information flows in imperative interactive programs.

In this work we formulate new information-flow conditions for a simple imperative programming language. Programs written in the language interact with users at multiple security levels via simple input and output operators. We encapsulate user behavior as "strategies" that determine which input a user provides based on the history of input and output events she has seen, and we use traces of input and output events to model the observations made by users at different security levels. The language includes operators for nondeterministic and probabilistic choice, and we give definitions of noninterference which account for the nondeterministic behavior that programs may exhibit. We illustrate the conditions with simple examples of secure and insecure programs.

Finally, we describe a simple type system for the language based on previous type systems that prevent information-flow in imperative programs. The type system, though conservative, soundly enforces our definitions of noninterference.

(This is joint work with Michael Clarkson and Stephen Chong.) Kevin O Neill is a Ph.D. candidate in the computer science department of Cornell University, where his research focuses on semantic definitions of secrecy and anonymity. He did his undergraduate work in computer science at the University of British Columbia in Vancouver. In his spare time he likes to sail and to play the piano, but he could use more training in both pursuits. He is currently looking for a job.

March 15, 2006 2pm, 1.18 Claremont Tower
Sensible decisions in very large networks
Erol Gelenbe

The network -- wired, wireless, sensor -- that we use is for all practical purposes becoming infinite. In such an environment, it may not possible to count on the accuracy of routing tables. The presentation will first discuss whether finite search times are possible in a large network with imperfect information. We will then suggest sensible local rules that can be used to do better than a random search. Finally we will discuss our Cognitive Packet Routing Protocol which has been implemented to experiment with some of these questions and ideas.

February 28, 2006 2pm, 1.18 Claremont Tower
Pervasive Messaging and Telemetry Integration
Andy Stanford Clark

In many industries, much of the data that companies need to run their day-to-day operations comes from "outside" the business... literally out in the field. Oil pipeline companies need to monitor the flow of liquid through their pipelines, power companies need to monitor generators, distribution grid, and consumer meters. Getting this data into the business applications which make use of it, is a major challenge. This seminar looks at the world of messaging and telemetry, and how IBM is solving the end-to-end data integration problem. Amongst the examples of real-world projects that will be described, are oil/gas pipeline monitoring, electric meter reading, weather monitoring, vehicle tracking, and electronic mouse traps!

February 22, 2006 2pm, G21/22 Devonshire Building
Formal Description Techniques for Interactive Systems Engineering
Philippe Palanque

Except form rare and isolated initiatives, Software Engineering and Human-Computer Interaction have been addressed quite separately. However, the widespread use of innovative interaction techniques, as a way of increasing bandwidth between interactive systems and users, calls for methods, notations, processes and tools to support design, implementation and validation of systems. While research in the field of Software Engineering has provided useful results for many kind of application domains (transactional systems, embedded systems, Information Systems, ...) very few solutions have been provided in the field of interactive systems. In this presentation we intend to discuss the specificities of interactive systems and why these specificities require dedicated support at support at the various stages of the development process. This will lead to a discussion about the difficulties of addressing in a single and coherent framework two fundamental requirements for interactive systems: Usability and Reliability. Lastly, the presentation will give an overview of current trends as well as a research agenda for the integration of research in Human Computer-Interaction and in Software Engineering.

February 13, 2006 2pm, G21/22 Devonshire Building
Themes in True-Concurrency and the Verification of Cryptographic Protocols
Sibylle Froeschle

The talk will proceed in two parts. In the first part I will present highlights of my work on the computational power of true-concurrency.In the second part I will discuss ongoing work on the verification of cryptographic protocols. True-concurrency is often perceived as both difficult to tackle and computationally hard. This is exemplified by hereditary history preserving bisimilarity (hhp-b): whether this notion is decidable was a renowned open problem for many years until it was finally proved undecidable by Jurdzi{'n}ski and Nielsen; only a few positive results could be achieved for restricted classes (Fr{"o}schle 2005). The negative findings are contrasted by a positive trend for true-concurrency in the infinite-state world. In particular, Lasota and I have recently resolved that hhp-b is polynomial-time decidable for the class Basic Parallel Processes. The hope to be able to validate cryptographic protocols automatically seems to have been thwarted by the fact that most security properties such as secrecy have turned out to be undecidable. On the other hand, one could argue that the undecidability proofs exhibited so far do leave room for positive results: most of these proofs exploit properties of the formal models used to represent protocols rather than characteristics possessed by realistic protocols. Based on this insight, one goal of my research is to characterize natural classes of protocols with decidable security properties.

February 9, 2006 2pm, G21/22 Devonshire Building
From Boolean Algebra to Unified Algebra
Eric Hehner

Boolean algebra is simpler than number algebra, with applications in programming, circuit design, law, specifications, mathematical proof, and reasoning in any domain. So why is number algebra taught in primary school and used routinely by scientists, engineers, economists, and the general public, while boolean algebra is not taught until university, and not routinely used by anyone? A large part of the answer may be in the terminology and symbols used, and in the explanations of boolean algebra found in textbooks. This paper points out some of the problems delaying the acceptance and use of boolean algebra, and suggests some solutions. Biography Hehner received his first degrees in mathematics and physics from Carleton University in 1969, and his PhD in computer science from the University of Toronto in 1974. The subject of his thesis was how to match the representation of data and programs to computer architectures. He then joined the faculty, becoming a full professor in 1983, and Bell University Chair in Software Engineering in 2001. His research has been mainly on the subject of formal programming methods, and the mathematics of program construction. He is the first winner of the annual computer science undergraduate teaching award. He has been a Visiting Scientist at Xerox Research Center, Palo Alto, a Visiting Fellow at Oxford University, a Visiting Researcher at the University of Texas, Austin, a Professeur Invité at the Université de Grenoble, a Visiting Professor at UBC, Vancouver, and at the University of Southampton. He is a member of IFIP Working Group 2.1 on Algorithmic Languages and Calculi, and IFIP Working Group 2.3 on Programming Methodology. He is an editor of Acta Informatica and of Formal Aspects of Computing. He has written two books (the Logic of Programming, Prentice-Hall, 1984, and a Practical Theory of Programming, first edition Springer-Verlag 1993, current edition online) and over fifty journal and conference papers. He has given over a hundred invited lectures at institutions around the world. He has taught short courses in Marktoberdorf Germany, Macau China, Turku Finland, and Tandil Argentina. His former students have gone on to head major corporations and departments of computer science.

February 8, 2006 1pm, Devonshire G21/G22 Conference Room
GRIDS, Databases and Information Systems Engineering Research
Keith Jeffery

GRID technology, emerging in the late nineties, has evolved from a metacomputing architecture towards a pervasive computation and information utility. However, the architectural developments echo strongly the computational origins and information systems engineering aspects have received scant attention. The development within the GRID community of the W3C-inspired OGSA indicates a willingness to move in a direction more suited to the wider end user requirements. In particular the OGSA/DAI initiative provides a web-services level interface to databases. In contrast to this stream of development, early architectural ideas for a more general GRIDs environment articulated in UK in 1999 have recently been more widely accepted, modified, evolved and enhanced by a group of experts working under the auspices of the new EC DGINFSO F2 (GRIDs) Unit. The resulting reports on ‘Next Generation GRIDs’ have been published with the third due in January 2006. They are used by the EC as an adjunct to the Framework Call for Proposals Documentation. The reports proposes the need for a wealth of research in all aspects of information systems engineering, within which the topics of advanced distributed parallel multimedia heterogeneous database systems with greater representativity and expressivity have some prominence. The need for novel operating systems and a new architecture for middleware based on SOKUs (service oriented knowledge utilities) has been articulated. Topics such as metadata, security, trust, persistence, performance, scalability are all included. This represents a huge opportunity for the database and information systems engineering community, particularly in Europe.

January 26, 2006 2pm, 701 Claremont Tower
Samoa: Formal Tools for Securing Web Services
Andy Gordon

Based on joint work with K. Bhargavan and C. Fournet Microsoft Research, Cambridge.

Securing.WS

An XML web service is, to a first approximation, a wide-area RPC service in which requests and responses are encoded in XML as SOAP envelopes, and transported over HTTP. Applications exist on the internet (for programmatic access to search engines and retail), on intranets (for enterprise systems integration), and are emerging between intranets (for the e-science Grid and for e-business). Specifications (such as WS-Security, now standardized at OASIS) and toolkits (such as the Microsoft WSE product) exist for securing web services by applying cryptographic transforms to SOAP envelopes.

The underlying principles, and indeed the difficulties, of using cryptography to secure RPC protocols have been known for many years, and there has been a sustained and successful effort to devise formal methods for specifying and verifying the security goals of such protocols. One line of work, embodied in the spi calculus of Abadi and Gordon and the applied pi calculus of Abadi and Fournet, has been to represent protocols as symbolic processes, and to apply techniques from the theory of the pi calculus, including equational reasoning, type-checking, and resolution theorem-proving, to attempt to verify security properties such as confidentiality and authenticity, or to uncover bugs.

The goal of the Samoa Project is to exploit these recent theoretical advances in the analysis of security protocols in the practical setting of XML web services. This talk will present some of the outcomes of our research, including: automatic analysis of hand-written pi-calculus descriptions of WS-Security protocols; automatic generation of pi-calculus descriptions from WSE config and policy files; and tools to help review the security of WSE installations.

January 11, 2006 2pm, Devonshire G21/G22 Conference Room
Understanding and modelling human error for interactive system design
Ann Blandford

Most work on human error is based around incident reports or other forms of retrospective reporting. This has led to important insights into causes of error – e.g. on the roles of context, feedback and policies in provoking human error. However, this approach cannot give insights into many of the underlying cognitive causes of error – what Hollnagel calls the ‘genotypes’ of error. One of the great challenges of conducting controlled studies of error is that they are difficult to provoke systematically in a controlled laboratory setting. In this talk I will present our ongoing work on developing methods for studying error in controlled settings that enable the manipulation of variables such as interruption point, task structure and visual cueing to determine their influence on certain types of error. In particular, we have been studying the roles of memory and attention in omissions such as post-completion errors. This work is informing parallel studies on formal modelling of users for systems verification, and less formal work on error evaluation methods.

December 19, 2005 2pm, 701 Claremont Tower
The Rules of Modelling: Automatic Generation of Constraint Programs
Alan M. Frisch

Many and diverse search problems have been solved with great success using constraint programming. However, to employ constraint programming technology to solve a problem, the problem first must be characterised, or modelled, by a set of constraints that its solutions must satisfy. Generating a correct model can be difficult; generating one that is easier to solve than its alternatives is even more difficult, often requiring considerable expertise. This so-called "modelling bottleneck" has inhibited the wider use of constraint programming technology. This talk describes CONJURE, a rule-based system that automatically generates constraint programs by refining an abstract problem specification. Since the high-level specification language is significantly closer than a constraint program to the way in which problems are commonly conceived, the modelling bottleneck is substantially reduced. A particular focus of this talk is showing why the refinement rules must be recursive, why this is difficult to achieve and how we ultimately solved solved this problem. This talk assumes no background in constraint programming.

November 29, 2005 4pm, Devonshire G21/G22 Conference Room
Modelling and Analysis of Quantum Cryptographic Protocols
Simon Gay

Most current cryptographic techniques rely on unproven assumptions about the computational intractability of tasks such as prime factorisation. These assumptions are directly threatened by theoretical developments in quantum computing, which could become practical in the medium term. Quantum cryptography is therefore of great interest as it is provably secure even in the presence of quantum computers. After introducing the basic concepts of quantum computing and quantum cryptography, I will argue that there is a need for formal modelling and analysis of quantum cryptographic protocols (as distinct from primitives) if we are to be confident of the security of real implemented systems. I will present recent work in this direction, including the design of a process calculus for modelling quantum systems, and preliminary results on model-checking quantum systems.

November 23, 2005 2pm, Devonshire G21/G22 Conference Room
Adding Conflict and Confusion to CSP
Christie Marr (nee Bolton)

In this talk we explore the truly concurrent notions of conflict,whereby transitions can occur individually but not together from a given state, and confusion, whereby the conflict set of a given transition is altered by the occurence of another transition with which it does not interfere. Having provided a translation from Petri nets, a truly concurrent formalism, to CSP, an interleaving formalism, we demonstate how the CSP model-checker FDR can be used to detect the presence of both conflict and confusion in Petri nets.

October 31, 2005 1pm, Devonshire G21/G22 Conference Room
A Hierarchical Analysis of Propositional Temporal Logic based on Intervals
Ben Moszkowski

We present a hierarchical framework for analysing propositional linear-time temporal logic (PTL) to obtain standard results such as a small model property, decision procedures and axiomatic completeness. Both finite time and infinite time are considered. The treatment of PTL with both the operator Until and past time is readily reduced to that for a version of PTL without either one. Our method is based on a low-level normal form for PTL called a transition configuration. In addition, we employ reasoning about intervals of time. Besides being hierarchical and interval-based, the approach differs from other analyses of PTL which in general utilise sets of formulas and sequences of such sets. Models are instead described by means of time intervals represented as finite and countably infinite sequences of states. The analysis naturally relates larger intervals with smaller ones. The steps involved are expressed in a propositional version of Interval Temporal Logic (ITL) since it is better suited than PTL for sequentially combining and decomposing formulas. Consequently, we can articulate various issues in PTL model construction which are equally relevant within a more conventional analysis but normally only considered at the metalevel. We also briefly describe a prototype implementation of a decision procedure based on Binary Decision Diagrams. Beyond the specific issues involving PTL, the research can be viewed as a significant application of ITL and interval-based reasoning and also illustrates a general approach to formally reasoning about a number of issues involving discrete linear time. For example, it makes use of various techniques for performing sequential and parallel composition. The formal notational framework for a hierarchical reduction of infinite-time reasoning to simpler finite-time reasoning could also be used in model checking. The work includes some interesting representation theorems and exploits properties of fixpoints of a certain interval-oriented temporal operator. In addition, it has relevance to hardware description and verification since the property specification languages PSL/Sugar (just made IEEE standard 1850) and "temporal e" (part of IEEE candidate standard 1647) both contain temporal constructs concerning intervals of time.

September 16, 2005 2pm, Devonshire G21/G22 Conference Room
Software Components -- A Step towards an Engineering Approach to Software?
Ralf Reussner

This talk discusses the role of software components for an engineering approach to software construction. In particular, this talk concentrates on predicting functional and extra-functional properties of layered component-based software architectures. The approach presented is based on parametric contracts, a generalisation of design-by-contract for the contractual definition of components.

August 24, 2005 2pm, Devonshire G21/G22 Conference Room
Dependability in a digitally integrated world - the challenge of moving from physical to logical boundaries
Stephan Engberg

When we move towards a fully integrated world where even physical artifacts are integrated with the electronic network through RFID and sensors, we are faced with the problem that systems and even databases might be provable dependable with automatic error and fault recovery. But this cannot be extended to the broader system incorporating the human factor. How do we protect systems and data when attackers initiate an identity theft attack on security cleared personel? We are faced with challanges requring us to question the basic definitions of security and dependability. This talk is addressing the needs and issues involved in moving to a context-centered security model focussing on empowerment to break the trade-off between integration and risk accumulation. We will address issues of mobile Identity and new solutions to RFID security to illustrate how multi-level fallback can be designed for success even with seriously limited ressources and groing resistance due to surveillance and privacy concerns. One key aspect of context understanding is that serverside global identification of people and devices is likely a design mistake. The main strenght of IPv6 is likely not that each device can have a persistent unique id but that devices can have a new unique id every time as this makes devices more difficult to target and only available in context. When we design with the assumption that perimeter security fails, not only do we design more dependable systems where one failure such as identity theft doesnt lead to cascading security failures, we also make more trustworthy systems focussing on the fundamentals of a democracy by alligning the issues of privacy and security.

July 27, 2005 2pm, Devonshire G21/G22 Conference Room
Failure Propagation and Transformation - a Safety Analysis
Malcolm Wallace

High integrity real-time software systems (HIRTS), as the name implies, have substantial requirements for reliability and safety. Traditional software analysis techniques tend towards determining a product's correctness, whether through proof, model-checking, abstract interpretation, or some other formal method. However, in the safety domain, it is of equal interest to know how a system behaves in the presence of failure, regardless of whether that failure is in the external environment, or caused by an internal software error. A demonstrable ability to continue to function in the presence of failures is good, and methods to mitigate potential hazards are important too. This talk will describe a modular representation and compositional analysis of a system's hardware and software components, called Fault Propagation and Transformation Calculus (FPTC). We show how, given an architectural description of components and their combination into a whole system, together with an FPTC expression of each component's failure behaviour, the failure properties of the whole system can be computed automatically from the individual FPTC expressions. From a safety point of view, this provides some idea of robustness: the system's capability to withstand certain types of failures in individual components. It also provides a way to understand how and where to develop fault accommodation within an architecture.

July 6, 2005 2pm, Devonshire G21/G22 Conference Room
Nonparametric inference in machine learning
Lehel Csato

Machine learning collects algorithms applicable for various data-sets and various problem types. One problem often encountered in machine learning methods is the issue of selecting the number of parameters, implying in some form the complexity of the model. Let us take the regression example. The generalised linear models are function approximators using a linear combination of functions. In the limit of infinitely many primitives the generalised linear models are universal approximators. The number of functions is usually fixed before applying the parameter inference and one has to make several runs with different number of parameters to obtain a good algorithms. Nonparametric methods are flexible inference procedures that sidestep the specification of model complexity by using a more flexible "parametrisation" of the functions used for approximation. The presentation will detail the application of Gaussian processes to various machine learning problems,like classification, regression or robust regression. Problems with the non-parametric setup, possible solutions, applications and programs will be presented.

June 8, 2005 3pm, Devonshire G21/G22 Conference Room
Some Recent Results and Research Problems in Timed Systems
Joel Ouaknine

The theory of automated verification in the untimed world has by now achieved a respectable maturity: we have a fairly good understanding of what is decidable and what isn't, and what complexity the algorithms involved have. The situation is much less clear in the timed world, where open questions abound. I will describe some very simple and natural problems that have recently -- and quite surprisingly -- been shown to be decidable, with nonetheless astonishingly high (non-primitive recursive) complexity. I will then discuss a number of related open problems, both theoretical and practical. No previous knowledge of timed systems will be assumed.

June 8, 2005 1pm, Devonshire G21/G22 Conference Room
SDSS and NVO, bringing Astronomical data to the masses
Wil O'Mullane

The Sloan Digital Sky Survey (SDSS) is in its 5th year and will hopefully be extended for 3 more years. The SkyServer is a comprehensive website allowing access to the 1.6TB science database which describes over 230 million astronomical objects. An extensive outreach and education section guides students through some of the data and tools. Traffic has been steadily increasing on the site requiring new developments such as the CasJobs Batch system. The National Virtual Observatory (NVO) concerns itself with the accessibility of datasets such as that produced by SDSS, it is in its 4th year. NVO is involved in international standards for the accessing of such data. This allows the construction of tools which are less specific to a single data set and allow correlations between them to be studied. Both projects faced and continue to face interesting technical challenges. This talk will present some of the highlights and discuss the underlying technologies.

June 1, 2005 3pm, To follow
The righteous and the wicked: efficient high-level methods for performance analysis
Stephen Gilmore

I'll present a novel method of modelling program execution on compute clusters. As previously, we use Performance Evaluation Process Algebra (PEPA) as the high-level modelling language, capturing both workload and computing fabric. The novel feature is that we make a continuous approximation of the state space underlying the PEPA model and represent it as a set of ordinary differential equations (ODEs) for solution, rather than a continuous time, but discrete state space, Markov chain.

Joint work with Anne Benoit, Murray Cole and Jane Hillston

May 18, 2005 2pm, Devonshire G21/G22 Conference Room
The BBC Domesday Rescue Project
Jeffrey Darlington

A collaborative project managed by The National Archives has rescued the unique data resource created by the BBC Domesday Project of 1986 from its obsolete videodisc storage medium, and its dependence on the obsolete BBC Micro computer. As this is an interactive multi-media data resource, the issues raised and problems solved are of great interest to all those concerned with preserving digital objects and tracking the history of the computer age. The talk compares several parallel rescue projects, each taking a different approach. After graduating from Cambridge, Mr Darlington worked in the UK computing industry for 30 years, designing business applications and databases. He lectures in Information Systems at the University of West of England and was a consultant to the Open University course ‘Relational Databases’

Mr Darlington joined the National Archives in 1998 and helped to set up and run the Digital Preservation Department from 2001 until his retirement last year. He was the Contract Manager for the UK National Digital Archive of Datasets and Project Manager for the BBC Domesday Rescue Project.

May 4, 2005 2pm, Room 519 Claremont Tower
An Algorithm for Polynomial Matrix Eigenvalue Decomposition
John McWhirter

Space time adaptive processing is an important topic which arises in broadband sensor array signal processing. The space time correlation matrix requires (at least) three dimensions but may be represented very effectively as a para Hermitian symmetric (Laurent) polynomial matrix. A stable technique for computing the eigenvalue decomposition (EVD) of such a matrix is important for many applications including; broadband subspace identification; independent component analysis (ICA) applied to convolutive mixtures; space time coding for multiple antenna (MIMO) communicaton channels. This paper presents a novel algorithm for computing the polynomial matrix EVD. It involves diagonalising the polynomial space-time correlation matrix by means of a paraunitary "similarity" transformation. It makes use of "elementary paraunitary transformations" and constitutes a generalisation of the classical Jacobi algorithm. A proof of convergence has been obtained. Impressive results have been obtained for a range of practical applications using both simulated experimental data. Some of these will be presented.

April 25, 2005 2pm, Room 519 Claremont Tower
Self Assembley Processes In Nanoscience
Ed Coffman

Advances in chemical synthesis have laid the groundwork for computation at nanoscale, where self assembly becomes the core process, either as a computation itself, or as a mechanism for fabricating nanodevices. By such processes, elementary particles, such as DNA molecules, combine into large complexes following built-in bonding rules. We study self assembly viewed as a random growth process, addressing such as questions as:``How long does a given structure take to self-assemble?'' ``How does one optimize the yield of a particular self-assembly process?'' ``What are the trade-offs between the reliability (error tolerance) and speed of self assembly?'' Answers to these questions bring out unexpected connections with well studied problems in physics, chemistry, and computer science.

April 20, 2005 2pm, Room 519, Claremont Tower
Collaborative Visualization in Grid Computing Environments
David Duce

This talk will give an overview of distributed and collaborative visualization and then describe some recent developments. We have devised a model for dataflow visualization at three levels: an abstract specification of the intent of a visualization, a binding of these abstract modules to a specific software system; and then a binding of software to processing and other resources. We have an XML application (language), called skML, capable of describing visualization at the three levels. A feature of the approach is that a visualization can first be described using modules from a generic collection and then translated into a concrete collection of modules in a specific visualization system, drawing on a variety of Web technologies to do so.

We are currently developing an application scenario based on wildfire management. We are developing a new collaborative visualization tool (using Web technology) within the context of an architectural framework for Grid middleware being developed at the University of Lancaster. The talk will outline the approach we are taking and the thinking behind it.

Through this work we have found the need for an ontology of visualization. The talk will conclude with some thoughts about this.

The talk is based on joint work with the University of Leeds in the gViz project (under the e-Science Core Programme) and the University of Lancaster in the Open Overlays project (under the e-Science Fundamental Computer Science for e-Science Programme).

----------
Professor David Duce
Department of Computing
School of Technology
Oxford Brookes University

March 16, 2005 2.30pm, G21 & G22 Devonshire Building
In Vivo - In Silico: finding out how nature grows complex systems
Ronan Sleep

We routinely use massively powerful computer simulations and visualisations to design aeroplanes, build bridges and to predict weather. With computer power and biological knowledge increasing daily, perhaps we can apply advanced computer simulation techniques to realise computer embodiments of living systems. This is the thinking behind iViS (in Vivo -- in Silico), a 15 year+ grand challenge project which aims to realise fully detailed, accurate and predictive computer embodiments of plants, animals and unicellular organisms. Possible benefits of iViS include an understanding of regeneration processes in plants and animals, with potentially dramatic implications for disease and accident victims. iViS may also lead to revolutionary ways of realising complex systems: instead of designing and programming such systems in excruciating detail, perhaps we can just grow them from compact initial descriptions in a suitable medium. We know it's possible, because that's exactly what nature does when it grows a plant or animal from a single cell. During the talk I will introduce the challenge, show some of the things it needs to model, outline some current approaches, and talk about some of the early work we have done towards the challenge at UEA.

February 16, 2005 2pm, Room 519, Claremont Tower
Temporal Information Maximization and Cortical Processing
Thomas Wennekers

Brains are information processing systems. From that point of view it seems plausible, that their self-organization follows some information theoretic optimization principles. In the early visual system mutual information maximization is one such widely acknowledged principle which minimizes redundancy in feedforward pathways. Independent information channels might be useful for early coding under a bottleneck constraint, but brain dynamics is more complex. Neurons interact dynamically in order to integrate distributed information into functional ensembles expressed by correlated activity. Synchronized oscillations and synfire chain like spatio-temporal firing patterns are the two most simple and best know correlation patterns that may serve cortical integration.

We have studied two measures called spatial and temporal stochastic interaction which extend mutual information (MI) from static feedforward mappings to recurrent systems and spatio-temporal correlations, respectively. Maximization of the temporal interaction measure (TIMax) in Markov chains leads to activation patterns similar to synfire chains, i.e., globally ordered state transitions, where single units nonetheless fire virtually randomly. If some units receive input defined by a prescribed Markov process, the optimized systems turn out to be almost deterministic finite state automata. Thereby TIMax provides a link between information theoretic optimization principles and computational processes. It is further shown that a simple temporal learning rule approximately maximizes TI, and that TIMax leads to a high information flow into the studied systems (as MI-maximization does naturally). Auto- and hetero-associative spiking neuron networks are shown to reveal high interaction values. These networks are common models for attractor- and synfire chain-like processing in higher areas. From these results we propose that TIMax might guide cortical self-organization supported by a temporal synaptic learning rules.

----
Thomas Wennekers
Center for Theoretical and Computational Neuroscience
University of Plymouth

January 26, 2005 2pm, Room 519, Claremont Tower
Distributed language models of online interaction
Ata Kaban

Online communication is considered an intellectual amplifier. Yet, this growing interest inevitbly results in a growing information overload, and this continues to challenge existing technology. Novel tools and techniques are needed that are able to enhance our understanding of human behaviour on the web and large-scale observational data is available to use for that purpose. Indeed, online communication is genuinely dynamic and most often produces highly entropic action sequences. Neither a global model nor user-specific models can help us detail and understand common trends and interests at various levels of groups and groupings. In this talk I will present ongoing work on approaches built of novel combinations of statistical language models, that are designed to scale to large masses of recordings, and are aimed to produce both accurate predictions and interpretable summary mappings of sets of logged activity sequences. Such models could be used for better understanding and predicting users' information needs and further enhancing the online technology.

-----
Ata Kabán
School of Computer Science
University of Birmingham

January 12, 2005 2pm, Room 518/519, Claremont Tower
Politics and IT: ­ experiences of making them fit together
Lesley Beddie

For more than 4 years, after being the Head of an academic Computing Department, I was the Director of Communications Technologies (ie IT and Broadcasting) at the Scottish Parliament. It was an immensely challenging and satisfying job but politics and computing/IT wouldn’t be many a person’s idea of an ideal partnership. Here are some examples of what we achieved at the Scottish Parliament and how we made the partnership work.

----------
Lesley Beddie (Director)
Information Technology Service
University of Durham

December 1, 2004 2pm, Room 519, Claremont Tower
A Functional Language for Hardware Modelling and Verification with Metaprogramming and Reflection
Tom Melham

Forte is a formal verification system developed by Intel's Strategic CAD Labs for applications in hardware design and verification. Forte integrates model checking and theorem proving within a functional programming language, which both serves as an extensible specification language and allows the system to be scripted and customized. Forte's functional programming language is also the underlying term language for the higher order logic of its theorem prover.

The latest version of this language, called reFLect, has quotation and antiquotation constructs similar to those in LISP, but typed. These build and decompose expressions in the language itself and provide a combination of pattern-matching and metaprogramming features tailored especially for the Forte applications. The addition of some reflection principles in the higher order logic based on reFLect also provides a framework for making a logically principled connection between theorems in higher-order logic, program execution in the reFLect language, and the results of model checking verifications.

This talk will describe the design philosophy and architecture of the Forte system and give an account of the reFLect functional language and its role in Forte.

This is joint work with Jim Grundy and John O'Leary of Intel Corporation.

------
Tom Melham
Professor of Computer Science
Tutorial Fellow at Balliol College
Oxford University Computing Laboratory

November 24, 2004 2pm, Room 519, Claremont Tower
Resources, Concurrency and Local Reasoning
Peter O'Hearn

Resource has always been a central concern in concurrent programming. Often, a number of processes share access to system resources such as memory, processor time, or network bandwidth, and correct resource usage is essential for the overall working of a system. In the 1960s and 1970s Dijkstra, Hoare and Brinch Hansen attacked the problem of resource control in their basic works on concurrent programming. In addition to the use of synchronization mechanisms to provide protection from inconsistent use, they stressed the importance of {\em resource separation}\/ as a means of controlling the complexity of process interactions and reducing the possibility of time-dependent errors.

In this talk we show how a resource-oriented logic, separation logic, can be used to reason about the usage of resources in concurrent programs.

----------
Peter O'Hearn
Department of Computer Science
Queen Mary, University of London

October 27, 2004 2pm, Room 519, Claremont Tower
Model Checking Polymorphic Systems with Arrays
Ranko Lazic

Polymorphic systems with arrays (PSAs) is a general class of nondeterministic reactive systems. A PSA is polymorphic in the sense that it depends on a signature, which consists of a number of type variables, and a number of symbols whose types can be built from the type variables. Some of the state variables of a PSA can be arrays, which are functions from one type to another. We present a complete classification of parameterised reachability problems on subclasses of PSAs into decidable or undecidable.

-------
Ranko Lazic
Department of Computer Science
University of Warwick

October 15, 2004 2pm, Room 518/519, Claremont Tower
The Technical and Societal Implications of Networking: A Personal Perspective
Dave Farber

Prof Farber has been involved with networking for over 45 years. Starting at Bell Labs and continuing in academia, he has been a key player in many of the US networking activities. He is called by many the Grandfather of the Internet due to his academic children who were among the Fathers of the Internet.

With that background, Prof Farber will examine the impact that networking has had on the world and its citizens -- not all positive. He will comment on the current chaos -- spam and other nasties and what if anything can be done.

The Moore's Law growth of network speeds has challenged the technical field to better understand how the future directions in computer hardware and increases in bandwidth due to all optical networking will impact future systems and applications. Prof Farber will give his thoughts on the directions with a hope of challenging the listeners to explore this area.

-----
Prof. David J. Farber
Distinguished Career Professor of Computer Science and Public Policy
Carnegie Mellon University
USA

September 29, 2004 2pm, Room 518/519, Claremont Tower
Data Base Technology for Sensor Based Computing
Dieter Gawlick

Sensor Based Computing has become a very hot topic, the RFID technology being its most prominent driver. Companies, governments, and service providers are eager to explore their options since they expect significant process improvements and cost savings. The research community is actively involved.

Sensor Based Computing has been based on three major components: Sensors, Edges Servers, and resources (applications, services, and actors). More recently, it has been recognized that there is a need for a Sensor Data Archive acting as a bridge between Edge Servers and resources. Sensor Based Computing needs to activate resources based on sensor readings, i.e., ‘sensor events’ activate the resources. Experience shows that Sensor Data Archives are often needed to understand sensor readings and are essential for the specification and creation of ‘business events.’ Business Events are more meaningful to resources than sensor events.

The presentation describes the elements of Sensor Based Computing with special focus on Sensor Data Archives, which contain the archived data and a description of sensor environments and resources. Furthermore, the presentation describes methodologies to specify business events and the technologies to identify these business events as soon as they become visible. The presentation will end with a set of challenges posed by Sensor Data Archives.

The presentation will show that the database technology is arguably the best basis for Sensor Data Archives.

-----
Dieter Gawlick
Oracle -- USA

As member of IBM's IMS development team Dieter proposed, architected, and implemented products that enabled high-end transaction processing technology. This work introduced many of the core concepts of the database/transaction technologies. While working for Ahmdahl (Fujitsu), Dieter worked on I/O optimization (Electronic data store, RAID5 technology). While at Digital (HP), Dieter led the development of the first database based workflow system. After joining Oracle, Dieter architected the first message queuing system that is fully integrated into and leverages the functionality of a commercial database - Oracle/AQ (Advanced Queuing). The development of ''Expressions as Data'' is a more recent achievement. He is currently focused on making databases the primary event source in the context of sensor based computing. Dieter has the MS equivalent from the University Muenster (Germany). He has published a series of articles, holds various patents, and served on many conference and workshop program committees.

September 22, 2004 2pm, Devonshire G21/G22 Conference Room
Alternative Reality, a new approach to VR
Marc Cavazza

Most research work in Virtual Reality (VR) endeavours to match the highest possible standards of physical realism, whether in visual appearance, physical behaviour of objects, or user interaction. However, early ideas in VR were advocating a psychedelic departure from our everyday experience. The VR pioneers were in pursuit of original experiences and fantasy worlds, far from our common sense laws of Physics. Our research in Alternative Reality investigates the behavioural mechanisms by which it is possible to create immersive virtual worlds, in which laws of Physics could be redefined on a principled basis, so as to induce new experiences. From a technical perspective, this approach substitutes itself to traditional “Physics engines”, taking advantage of the fact that these operate on a discretisation of virtual world events. This discretisation makes it possible to integrate AI-based simulation mechanisms. We have targeted two elements of reality. The first consists of process-based mechanisms (such as fluid flows, heat exchange, etc.) which we have modelled using Qualitative Physics. The second one, causal perception, lies at the interface between perception and cognition, and plays an important role in our mechanistic explanation of the world. We will show how the artificial creation of co-occurrences between events can induce causal perception in subjects. We have developed a complete environment using a game engine for visualisation (because of its sophisticated event system) which has been adapted to immersive VR using a CAVE™-like hardware (the SAS Cube™) and the CaveUT™ software. In this talk, we will give various examples of such behaviours in different contexts, from fantasy worlds created as part of artistic briefs to everyday settings which can be used to explore subjects’ perception. This work, which was originally developed in the context of VR Arts, is also opening new research directions, such as the development of virtual environments supporting cognitive experiments, or new techniques to optimise objects’ behaviour in VR.

September 13, 2004 2pm, Devonshire G21/G22 Conference Room
An architecture and a language for contract monitoring in cross-organisational systems
Zoran Milosevic

In this talk we will present our solution for business contract monitoring as part of an overall enterprise contract management system. This solution consists of business contract architecture (BCA) and business contract language (BCL). BCA is designed to support contract management in cross-organisational environment and can be configured to reflect specific business and IT deployment requirements. BCL is developed to express various contract conditions pertinent to the execution of activities and processes needed for the fulfillment of obligations and other policies stated in contract. Its primary aim is to support the expression of contract monitoring conditions. The BCL is declarative, event-based language and can be used to parameterize generic BCA for specific business contracts and for specific enterprise contract management activities. We will conclude with an overview of our other current and future e-contracts research topics. Speaker Bio: Dr Zoran Milosevic is a Principal Scientist at Cooperative Research Centre for Enterprise Distributed Systems Technology (EDST). His areas of interest include enterprise modelling and enterprise architectures of open distributed systems, cross-organisational business processes and business contract architectures and languages. Zoran has over 18 years of ICT experience including various roles in consulting, research, standardization (e.g. ISO, OMG, OASIS and W3C standards) and in commercial software development. He has published over 50 conference and journal papers. He is the founder of IEEE's EDOC conference, PC member of several other research conferences and a frequent speaker at many international events. He holds a PhD in Computer Science (The University of Queensland).

July 16, 2004 2pm, 519
Recent Work on WebSphere Application Server
Graeme Dixon

To follow

July 5, 2004 2pm, Room 519, Claremont Tower
Two Conceptions of Security Online
Helen Nissenbaum

The mandate of computer security has grown in complexity and seriousness as computer technologies have saturated society and, simultaneously, the threats have multiplied in number and sophistication. Although well-publicized attacks by viruses, worms, and unauthorized break-ins make the work of computer security specialists seem clear-cut, the broader purposes of computer security are, in fact, ambiguous. Or, so this paper argues. It proposes that at least two conceptions of security are vying for the attention and resources of the wide-ranging activity of computer security: one that has evolved within the computer science and engineering community focused on individual systems, the other that has been carried over from the political arena of national security focused on collective and institutional systems. The paper argues that because these two conceptions envision divergent understandings of what it means for a computer environment to be "safe" they will have divergent implications for design and ultimately for the utility of computerized information and communications networks. It is important that we see these differences clearly so we may set our course with purpose and deliberation.

_________________________________
Helen Nissenbaum
Department of Culture and Communication, NYU
USA

June 30, 2004 2pm, Room 519, Claremont Tower
Scalable Ubiquitous Computing Systems
Jon Crowcroft

We are all acquainted with the Personal Computer. We are less aware of the burgeoning numbers of invisible, embedded computers around us in the fabric of our homes, shops, vehicles and even farms. They help us command, control, communicate, entertain, and commerce, and these invisible computers are far, far more numerous than their desktop cousins. The visible face of computing, the ubiquitous PC, is nowadays generally networked. To date, embedded computing systems have been largely used to replace analog control systems (for reasons of price, performance and reliability). Increasingly, however, we will find systems are integrated into a whole. This will lead to a challenge for Computer Science in the form of system complexity. Complexity is at the core of the skill-set of computer science and engineering, but it is also becoming a key piece of the formalisms used to understand other systems in the natural world, in ecology and biology and in physics. With the Internet as large and organic as it already is, we see a complex set of interactions with graph theory, control theory, economics and game theory, and a number of other disciplines being bought to bear and even extended to understand its behaviour. We also see a set of engineering rules of thumb maturing into design principles, which can be applied to other systems. Some principles already established in the world of Internet-scale engineering give us hope that we can build systems early (and there are many Ubiquitous Computing projects underway in the UK, EU and world today), with some hope that they will work. However, as systems grow, new problems for performance (stability, availability, etc) will emerge. Critical new areas for concern are the control of multiple resources (scheduling for battery life, randomising timing of events to avoid correlated overload, statistical failure tolerance in very large scale sensor systems). Within the timescales of this challenge, components will even start to draw resources (power) directly from their environment (ambient heat, RF etc), and this has hidden consequences (radio opacity in unusual places for example). The more we look at how such systems will be built, the more we see them vanish into the substance (and ether) around us! The core of this challenge then, is to abstract out these engineering design principles, and this will be achieved largely through a process of ``build and learn''. This is a natural complement and sister to the challenge to uncover the Science for Global Ubiquitous Computing, which will have descriptive power. We will have prescriptive solutions (patterns) for the mixed reality environment that will form the next phase of development of cyberspace.

May 28, 2004 2pm, Room 518; Claremont Tower
The Economics of Software Dependability
Barry Boehm

In most software applications, investments in software dependability compete with investments in such alternate capabilities as functionality, response time, adaptability, and speed of development. Investigating the tradeoffs among these sources of investment raises a number of significant questions about the nature of software dependability and its interactions with other desired software capabilities. These questions include:

• What software capabilities are your various stakeholders really depending on (liveness, responsiveness, quality of service)? What happens when these aspects of "dependability" conflict?
• Is success in the marketplace a monotone function of achieved dependability?
• Is quality really free in all situations? How can one determine how much investment in dependability is enough in a given situation?
• Are there ways to quantify the tradeoffs among schedule, cost, and dependability? Is "faster, cheaper, better" really achievable?
• Many current software dependability-related techniques assume that every requirement, use case, test case, and defect is equally important. How cost-effective are such value-neutral methods?
• What are the strengths and weaknesses of emerging "agile methods" in coping with dependability-related investments?

This talk will explore these and related questions from the perspective of the emerging discipline of Value-Based Software Engineering. It will show that, at least in many cases, reasoning about the economics of software dependability can lead to more satisfactory outcomes than will the application of value-neutral techniques.

------------
Professor Barry Boehm
TRW Professor of Software Engineering
Computer Science Department
Director, USC Center for Software Engineering
University of Southern California

May 21, 2004 2:30pm, Room 518, Claremont Tower
From Objects to Agents: An Aspect-Oriented Approach
Alessandro Fabricio Garcia

Software engineers of Multi-Agent Systems (MASs) are faced with different concerns (properties), such as autonomy, adaptation, interaction, collaboration, learning, and mobility. Many of these agent concerns cannot be modularized based only on object-oriented abstractions. MAS developers however have relied mostly on object-oriented design techniques and on object-oriented programming languages, such as Java. As the agent complexity increases, the agent concerns tend to spread across several system components at the architectural, design and implementation levels. It often leads to a poor separation of agent concerns in the software system, and in turn to the production of MASs that are difficult to maintain and reuse.

This talk will present an innovative aspect-oriented approach for the seamless integration of agents into object-oriented software engineering from the architectural stage to the implementation stage. Aspect is the abstraction used to modularize agent concerns that crosscut several system components. The proposed approach encourages the separate handling of agent properties, and provides a disciplined scheme for their composition. The approach is composed of an architectural method, a pattern language, and an assessment framework. The architectural method and the pattern language provide aspect-oriented solutions for modularizing the agent concerns at different stages of design and implementation. The purpose of the assessment framework is to support the evaluation of the reusability and maintainability of aspect-oriented solutions based on a metrics suite and a quality model. Experimental studies in different application domains have been conducted to assess the proposed approach based on qualitative and quantitative criteria. The use of the aspect-oriented solutions resulted in fewer lines of code, fewer design and implementation components, lower internal complexity of system components, and lower coupling.

May 20, 2004 2.30 pm, Room 519 Claremont Tower
Advances in Logic Verification and Boolean Satisfiability
Dhiraj Pradhan

Logic Varification continues to be considered one of computer aioded design's (CAD) most difficult problems. This is highlighted with the recent discovery of the Pentium bug dilemma which had a large financial and time-to-market consequences. This talk reviews certain current innovations addressing the problem of logic verification. A new method will be discussed, based on what has become known as Recursive Learning developed by the author. This proposed techinue has its conerstone in Boolean implication techniques and it has been proven most powerful when traditional approaches as Ordered Binary Decision Diagrams fail.

May 19, 2004 2pm, Room 519, Claremont Tower
Last dance on the Titanic: Why we need to re-invent computer security
Angela Sasse

Over the past few years, the security researchers and practioners have come to realise that lack of usability can undermine security systems. Most of the recent attempts to address this problem treat usability of security as a user interface (UI) problem. It is no co-incidence that the most widely known and cited paper on usability and security is Whitten & Tygar's "Why Johnny Can't Encrypt", a study of the user interface to PGP 5.0.

Whilst the UIs of many security tools are difficult to use, the talk argues that these immediate user-system interaction problems are only the tip of the "security problem iceberg", and we need to address more fundamental issues. In conclusion, I will argue the case for designing security as a socio-technical system, and outline how the roles and responsibilities of different stakeholders ought to be re-defined.

-----------

Biography

M. Angela Sasse is the Professor of Human-Centred Technology in the Department of Computer Science at University College London, UK. She holds an MSc in Psychology from the University of Sheffield, UK, and a PhD in Computer Science from the University of Birmingham, UK. Prior to joining UCL, she worked as a She has been researching usability issues in security since 1997, and co-authored a more than a dozen publications on human-centred approaches to security, trust and privacy (see http://www.getrealsecurity.com/publications.htm).

May 5, 2004 3pm, L401, The Seminar room, Merz Court
Quantum Theory and Global Optimisation
Koenraad Audenaert

We consider a problem in quantum theory that can be formulated as an optimisation problem and present a global optimisation algorithm for solving it, the foundation of which relies in turn on a theorem from quantum theory. To wit, we consider the maximal output purity $\nu_q$ of a quantum channel as measured by Schatten $q$-norms, for integer $q$. This quantity is of fundamental importance in the study of quantum channel capacities in quantum information theory. To calculate $\nu_q$ one has to solve a non-convex optimisation problem that typically exhibits local optima. We show that this particular problem can be approximated to arbitrary precision by an eigenvalue problem over a larger matrix space, thereby circumventing the problem of local optima. The mathematical proof behind this algorithm relies on the Quantum de Finetti theorem, which is a theorem used in the study of the foundations of quantum theory.

We expect that the approach presented here can be generalised and will turn out to be applicable to a larger class of global optimisation problems. We also present some preliminary numerical results, showing that, at least for small problem sizes, the present approach is practically realisable.

------------
Koenraad M.R. Audenaert
School of Informatics
University of Wales (Bangor)

------------
Joint event with the Department of Mathematics
http://www.mas.ncl.ac.uk/~najd2/colloquium/colloq_03,4_2.html

April 29, 2004 2:30pm, Room 518; Claremont Tower
Software Evolution and the Future for Flexible Software
Keith Bennett

Most successful software evolves over its lifetime, often in ways in which the original designers cannot conceive. I’ll start by presenting a brief overview of the state of the art, and summarise how we currently cope with such evolution, drawing on industrial case studies.

The “holy grail” for evolution is to build software which is intrinsically flexible – it is easy to change without compromising dependability (in broad terms, the cost of making a change is proportional to the size of the change, not the system). Software engineers have not been very successful in understanding how to do this, yet the demands to change software in internet time are increasing, particularly in so-called “emergent” organisations. This problem is being taken up as part of a proposed grand challenge in computer science.

I’ll present the results of research being undertaken by the Pennine Group on a project called IBHIS which is exploring radical solutions, with a more demand-centric view leading to software which will be delivered as a service within the framework of an open marketplace. Based on this foundation, I'll then describe recent work, which has resulted in an innovative demand-side model for the future of software evolution. Components may be bound just at the time they are needed, executed, and then the binding may be discarded.

----------

Prof. Keith Bennett
University of Durham

Pennine Research Group **

** The Pennine Research Group is the name of a group of software engineering researchers at Keele, UMIST, Durham and Leeds who have been collaborating for the past 8 years on service-based software engineering. See www.service-oriented.com.

April 20, 2004 2pm, Room 519, Claremont Tower
Securing Spontaneous Interactions in Mobile/Ubiquitous Computing
Tim Kindberg

A key problem in mobile and ubiquitous computing is that of setting up associations between pairs (or larger groups) of devices so that they may communicate securely over a wireless network. For example, suppose I send a photograph over a local wireless connection from my phone or PDA to a printer when visiting my friend's house. How can I conveniently ensure that the neighbours cannot access it? It is particularly important to be able to solve this general problem for associations in spontaneous circumstances. The interaction should not depend on preexisting security values such as certificates; moreover, the user establishes trust dynamically in some parts of their environment but not others, and the main reliable means of identifying the (trusted) target device is physical. This talk concerns protocols for constructing and validating secure spontaneous associations based on physical evidence. I shall present our first protocols, which were predicated on special hardware, and more recent work to eliminate that requirement. The problem description and much of the techniques should be broadly understandable by a general audience, but the talk will contain technical material. Speaker Bio: Tim Kindberg has been a senior researcher at HP Labs for four years, initially in Palo Alto and since September 2003 in Bristol. His research interests include ubiquitous computing systems, distributed systems, and human factors. Recent research addresses support for users to navigate between physical and virtual artefacts -- in particular, the Pulp Computing project investigates the integration of paper artefacts into personal and inter-personal computing environments. He is also investigating use-models and protocols for secure content exchange between ubiquitous devices. He was formerly a senior lecturer in Computer Science at Queen Mary, University of London. Before that, his PhD research led to start-up Zebra Parallel, which marketed an operating system for adaptively parallel programs. He holds a PhD in Computer Science from the University of Westminster and a BA in Mathematics from the University of Cambridge. He is co-author of the textbook 'Distributed Systems -- Concepts & Design'.

April 14, 2004 2pm, Room 519, Claremont Tower
Interoperation between a PKI and an ID-based infrastructure
Chris Mitchell

Suppose that members of two separate security domains wish to intercommunicate in a secure way. Suppose also that domain A uses a 'conventional' PKI, with one or more CAs, whereas domain B operates an ID-based public key infrastructure, with one or more trusted key generation entities (trusted authorities). Given that the members of the two domains wish to inter-operate, i.e. verify signatures generated by each other and/or send each other encrypted messages, there needs to be a means for members of domain to obtain trusted copies of public keys for members of domain B, and vice versa.

In this talk we will explore some aspects of this problem, and consider possible solutions. The work described is joint research with Geraint Price.

-----------
Professor Chris Mitchell
Information Security Group
Royal Holloway, University of London

March 24, 2004 2:30pm, Room 519, Claremont Tower
The impact of new technologies upon Cyber Trust & Crime Prevention - emerging findings of a Foresight project
Miles Yarrington

The Cyber Trust & Crime Prevention project is looking at the application and implications of future generation information technologies in areas such as identity and authenticity, surveillance, system robustness, security and information assurance and the basis for effective interaction and trust between people and machines. This has involved bringing together experts from a broad range of subjects, covering technology and its uses, to develop a number of visions for the future that allow us to explore potential key decision points over the next 10 to 15 years. One of the assumptions made is that ICT will become increasingly pervasive during that period, but there are question marks around the emergent behaviours of complex systems and how that may affect peoples perceptions of risk and the development of on-line trust.

---

Miles Yarrington
Project leader for the Cyber Trust & Crime Prevention project
DTI - Foresight

March 17, 2004 2pm, Room 519, Claremont Tower
Relational-based Calculus for Trust Management in Networked Services
Noureddine Boudriga

This talk considers the use of local policy enforcement in communication networks. Compliance with the security policy is important, especially if the system is based on the concept of Public Key Certificate (PKC). Our approach discusses the design of a trust management scheme that integrates a model for the specification of entities and actions, a mechanism for identifying users, authorizations, and delegations, and a compliance engine. The model is based on the use of an axiomatic representation of security requirements. The compliance engine integrates a relational calculus that allows proof and verification. Three cases are addressed to validate the model: the anonymous payment system, clinical information system, and distributed firewall systems.

------------
Prof. Noureddine Boudriga
Prof. of Telecommunications at "Ecole Supe'rieure des Communications de Tunis (SUP'COM)", Tunisia

March 16, 2004 2:30pm, Room 519, Claremont Tower
Engineering Webs of Knowledge
Nigel Shadbolt

We face a dilemma. The exponential growth of content on the web provides unparalleled opportunities for harnessing knowledge on a massive scale. At the same time we are suffering from a new kind of technological pollution ­ infosmog ­ so much information it is hard to make timely or effective decisions.

The Advanced Knowledge Technologies IRC has the principles aim of getting the right content to the right place, at the right time and in the right form. Content managed in this way is practical knowledge. AKT is about making this vision of knowledge management a reality. It is about understanding why this is hard.

AKT is using the World Wide Web as its principle source of content. Tim Berneers-Lee's vision for a Semantic Web is very close to AKT’s original aspirations. My talk will articulate the assumptions behind the Semantic Web and explain how AKT is attempting to build many of the required components. It will discuss applications under construction and also identify a number of substantial computer science research challenges confronting research in this area.

----------
Professor Nigel Shadbolt FBCS
Intelligence, Agents, Multimedia Group
Electronics and Computer Science
University of Southampton

March 3, 2004 2:30pm, Room 519, Claremont Tower
Relating Models for Consistent Diagrams of Critical Systems
Juan Bicarregui

In the design of critical systems, a variety of diagrammatic forms are commonly used for representing different aspects of the design. Safety analyses, using further diagrammatic conventions, requires an inter-disciplinary collaboration between designers who, whilst expert in some domains, may be less familiar with others. Understanding the full significance of such analyses, therefore, requires accurate correlations to be drawn between information represented in the various diagrams. Interpreting the word 'diagram' broadly to include tables and structured lists, we offer a framework which enables the display of consistent, diverse, diagrammatic views of a system.

In this seminar I will outline the framework and present a small case study using an engineering schematic, a HAZOPS table, a fault tree, a plant procedure description and a controller state chart. I will illustrate some consistency relations between these diagrams and discuss an approach to enhance the visual presentation of these diagrams. Finally I will discuss issues related to the implementation of the approach using SQL and XML.

The work presented is joint with David Clark, Julian Gallop and Stephen Morris.

February 26, 2004 2:00pm, Room 118, Claremont Tower
'Bruce Willis is Braver than You Think': New Techniques for Analysing Software Failures in NASA's Space Missions
Chris Johnson

I'll talk about a joint project with NASA Langley to develop analysis techniques that can be used to identify the causes of failures involving complex programmable systems. In particular, I will look at a joint analysis of the Mars Surveyor `mishaps' and the SOHO observatory mission interruption. I can also briefly discuss more recent initiatives such as the new NASA safety centre being set up after the Columbia accident report.

Chris Johnson,
Department of Computing Science,
Univ. of Glasgow.

February 19, 2004 1pm, Room 519 Claremont Tower
How to Live Beyond Your Means: Extracting Response Time Densities and Quantiles from Stochastic Models
Will Knottenbelt

Response time quantiles are important performance and quality of service metrics increasingly specified in contracts and Service Level Agreements (e.g. 95% of text messages must be delivered in under three seconds). This talk considers analytical methods for calculating response time densities and quantiles in Markov and semi-Markov chains derived from Stochastic Petri net models using numerical Laplace Transform inversion. We also consider efficient parallel implementation using hypergraph partitioning. Results are presented for very large Markov and semi-Markov models with over 15 million states and validated against simulation.

February 12, 2004 1pm, Room 519 Claremont Tower
Towards an Internet-wide Distributed System for Media Stream Processing and Delivery
Richard West

This talk focuses on the construction of an Internet-wide distributed system for media stream processing and delivery. Applications targeted by this system include live webcasts, tele-medicine and interactive distance learning. The aim is to support numerous channels of real-time data streams, generated by a number of publishing nodes and delivered to hundreds of thousands of clients with specific QoS constraints. The novelty of our approach concerns the use of overlay topologies (now popular with peer-to-peer systems) to deliver QoS-constrained streams between publishers and potentially thousands of subscribers. Consequently, I will discuss preliminary results from the study of k-ary n-cubes for data delivery, given that membership of the system, publishers, subscribers and QoS constraints may change at run-time. Additionally, I will describe work we are doing on the construction of an efficient end-host architecture, as part of this Internet-wide system. This includes a user-level sandboxing mechanism, to predictably, efficiently and safely execute stream processing agents (SPAs), as data is transported along its path from source to destination. Techniques that support the safe execution of application-specific service extensions, while avoiding unnecessary data copying and heavyweight context-switching will be discussed.

February 5, 2004 2:30pm, Room 518, Claremont Tower
Web Services Management Framework and Related Topics
Aad van Moorsel

This presentation discusses the motivation and technology behind HP's WSMF standard proposal. The objective of this standard proposal is to agree on manageability interfaces for web services as well as other types of applications and resources. We will discuss the design objectives and choices, which will not be unfamiliar to grid and web services engineers, as well as some implementation aspects. I will dress it all up with some related topics, to be determined.

-----

Aad van Moorsel's topic of main interest is managing large-scale systems.

Previously, Aad worked as researcher and research manager for Hewlett-Packard Laboratories in Palo Alto, California, and for Lucent Bell Labs Research in Murray Hill, New Jersey, both in the United States.

Aad was a postdoctoral researcher for two years at the University of Illinois at Urbana-Champaign, USA, after he got his PhD from University of Twente in The Netherlands in 1993.

January 29, 2004 2:30pm, Room 519 Claremont Tower
Security is a dirty word
Mike Ellison

Computer Security is seen as one of the ideals every computer user pays heed to and tries to follow, except when it gets in the way from what is perceived as the "normal course of work". However there are reasons why it is there - any computer is a popular target for intruders. Why? Because intruders want what you've stored there. They look for credit card numbers, bank account information, and anything else they can find. By stealing that information, intruders can use your money to buy themselves goods and services.

But it's not just money-related information they're after. Intruders also want your computer's resources, meaning your hard disk space, your fast processor, and your Internet connection. They use these resources to attack other computers on the Internet. In fact, the more computers an intruder uses, the harder it is for law enforcement to figure out where the attack is really coming from. If intruders can't be found, they can't be stopped, and they can't be prosecuted.

The talk will cover the some of the major attacks that have affected computer systems on campus (both globally [e.g. Nimda and Blaster] and locally) as well as discussing some of the threats and reasons behind these attacks

Michael Ellison
IT Security Coordinator
Information Systems and Services,
University of Newcastle Upon Tyne

January 21, 2004 3pm, Room 519 Claremont Tower
CommUnity on the Move: Coordination in Distributed and Mobile Systems
José Luiz Fiadeiro

We present an extension of CommUnity, a language for parallel program design, that is being developed in order to represent distribution and mobility explicitly in system architectures that are structured in terms of components and coordination connectors. In the developed extension, patterns of distribution and mobility of components (or groups of components) can be explicitly represented in architectures through a primitive that we have called distribution connectors. Furthermore, new abstractions for component interaction that have been proposed in order to facilitate the design of mobile systems can be modelled as coordination connectors and used in systems architectures together with the connectors that model traditional coordination primitives. These new abstractions include coordination patterns that are location-dependent or even involve the management of the location of the coordinated parties.

January 14, 2004 2:00pm, Room 519 Claremont Tower
Nature Inspired Cryptography and Security
John Clark

In this talk I will outline how nature-based search techniques have recently been applied to problems in modern cryptography and cryptographic applications. Much work has concentrated on the development of building blocks (such as the synthesis of Boolean functions satisfying particular cryptographic criteria) but there have been higher level applications (such as the automated refinement of security protocols). I will describe work on building blocks, protocols, and outline some rather non-standard approaches to cryptanalysis. I will also hint at possibilities for downright skullduggery (e.g. planting trapdoors in cryptographic designs). I wouldn't want to give a full seminar on "achievements", and so will end by engaging in gross speculation regarding the future of nature-inspired techniques in cryptology and security more generally.

The talk will be aimed at a general computer science audience.

Dr John A Clark
Senior Lecturer in Critical Systems
Department of Computer Science
University of York

December 4, 2003 1pm, Room 519 Claremont Tower
Lost Horizons
Neale Smith

Current industry and academic research is going down an inappropriate path. We will give examples of alternative ways of looking at problems and how conventional thinking can stifle development. The examples will be generic, drawn from various disciplines as well as computing. The intention is to try to encourage people to consider using lateral thinking to solve various "insurmountable" problems and avoid "physical barriers" when developing new technologies

December 2, 2003 14:30, Room 519 Claremont Tower
Why politics needs computer scientists
Ian Brown

Nobody would question that lawyers or economists can make a valuable contribution to the development of public policy. Yet curiously for our "information society", very few computer scientists are involved at a senior level in politics or the civil service. The result is often policy that is ignorant of the most fundamental technical realities.

The Foundation for Information Policy Research was founded in 1998 to attempt to redress this problem. Initially it focused on legislation that would have required private cryptographic keys in the UK to be lodged with "Trusted Third Parties". This eventually became the Regulation of Investigatory Powers Act, which FIPR had a major impact in improving. Since then FIPR has continued to work on surveillance issues, and has also had successes in the fields of intellectual property, e-voting, medical privacy and ID cards.

In this seminar, Ian Brown will describe some of these policy battles in more detail, and attempt to demonstrate that the introduction of a little computer science into politics goes a long way!

----

Ian Brown is director of the Foundation for Information Policy Research. He has spoken and written extensively on communications and medical privacy, copyright and e-voting. Dr Brown is an honorary research fellow at University College London, from where he received a computer science PhD in the field of communications security. He is advising the US government on the security of their next-generation emergency communications systems, and is the co-author of a recent Kluwer book on this subject. Brown has consulted for other large organisations such as the BBC, JP Morgan and Credit Suisse. He is also a trustee of Privacy International.

November 4, 2003 14:30, Room 519 Claremont Tower
Quantum Software Engineering?
Jeff W Sanders

Is there a discipline of quantum software engineering?

Quantum algorithms provide a test for software engineers: can they be specified and reasoned about as successfully as can standard software? This seminar will investigate the specification and derivation of a distributed quantum algorithm - Brassard and Bennett's quantum protocol for secure key distribution. The case study is of some interest because a quantum algorithm is a probabilistic algorithm, and for probabilistic algorithms the standard theory of data refinement, by which implementations are verified against their specifications, fails.

However it will be argued that in spite of the success of this study, anticipation of a discipline of software engineering is at present misplaced. It will be argued that the likely scenario is use of hybrid systems in which embedded quantum processors are exploited for executing specific procedures.

No familiarity of quantum computation will be assumed.

(This work was not supported by EPSRC.)

October 29, 2003 3pm, Room 519 Claremont Tower
Collaborative Working in Requirements Management for a System of Systems
Amer Saeed

The development of a fifth terminal (T5) at Heathrow is part of BAA's strategy for modernising and improving the airport to meet aviation demand and customer needs whilst minimising impact on the environment. The development of systems to support Baggage Handling, CCTV, Lifts, Energy Services etc and their integration to a system of systems will be essential to the efficient operation of T5.

Traditionally suppliers of the individual systems have worked at their own sites in accordance with company practices. However, for the T5 project, suppliers are co-located and collaboration is facilitated through a common IT infrastructure and project procedures. T5 Suppliers have been recruited at the project definition stage, with a general scope of work and fixed budget, with the objective to precisely define their supply and its interfaces to the T5 Environment. For Project Definition, T5 suppliers use a systematic approach to requirements development and management supported by DOORS. The approach:

• allows flexibility in the production of requirements documents,
• leads to a standard set of requirements documents, through the use of common document templates and statement level templates,
• supports collaboration during requirements elicitation through viewpoint documents,
• checks the quality of the actual requirements process followed by the suppliers and the requirements documents produced using an evidence-based assurance approach.

This presentation will overview the systematic approach, the support role of DOORS and report on experience to date.

October 23, 2003 13:30, Claremont Tower Room 118
Determining the specification of a control system from that of its environment
Ian J. Hayes

Well understood methods exist for developing programs from given specifications. A formal method identifies proof obligations at each development step: if all such proof obligations are discharged, a precisely defined class of errors can be excluded from the final program. For a class of ``closed'' systems such methods offer a gold standard against which less formal approaches can be measured.

For ``open'' systems --those which interact with the physical world-- the task of obtaining the program specification can be as challenging as the task of deriving the program. And, when a system of this class must tolerate certain kinds of unreliability in the physical world, it is still more challenging to reach confidence that the specification obtained is adequate. We argue that widening the notion of software development to include specifying the behaviour of the relevant parts of the physical world gives a way to derive the specification of a control system and also to record precisely the assumptions being made about the world outside the computer.

October 16, 2003 1.00 pm, Room 519 Claremont Tower
A Decentralized Mechanism for Distributed Coordination & Control
Naftaly Minsky

It is my thesis that for a group of autonomous agents to interoperate effectively, they must be able to trust each other to comply with some common rules-of-engagement, or a policy. Moreover, it stands to reason that if the members of the group in question are heterogeneous, with little or no trust in each other, then their interaction-policy needs to be enforced; and that this enforcement needs to be de-centralized, if the group might be large.

Guided by this thesis we have developed a coordination mechanism called Law-Governed Interaction (LGI), that enables a community C of distributed agents to interact under an explicit and strictly enforced policy, called the ``law'' of this community.

This mechanism, which is currently prototyped by the Moses toolkit, has the following characteristics: (a) The membership of C can change dynamically, and can be very large. (b) LGI makes no assumptions about the structure and behavior of members of C, which can, therefore, be heterogeneous. (c) The deployment of a community under a specified law is easy, incremental, and can be done dynamically. (d) The enforcement of laws under LGI is strictly decentralized---for scalability. (e) LGI provides for flexible interoperability between policies.

In the talk, I will attempt to motivate this mechanism, describe its nature, and outline some of its applications.

October 8, 2003 3.00pm, Room 519 Claremont Tower
Trade Secrets, Dongles, and Patents: A History of Software Protection
Martin Campbell-Kelly

The European Parliament will shortly be voting on whether or not to allow software patents in Europe. Since software patents were officially permitted in the United States in 1982 tens of thousands have been granted. Software patents are deeply controversial: in particular it is argued that patent “thickets” threaten the existence of the software industry and the open source movement.

This seminar traces the evolution of software protection, from trade secrets in the 1960s, through copyright protection in the 1970s, to software patents in the 1980s. The perceived threats to the future of software construction are set in the historical context of information technology patents over the last 100 years.

October 2, 2003 2pm, Room 118 Claremont Tower
Software Concerns: Separation and Composition
Michael Jackson

Separation of concerns is a well-recognised principle. But it is not always easy to say exactly what is, and what is not, a concern. In this talk a notion of concern is presented based on the decomposition of realistic problems into simple subproblems. The composition of these subproblems to obtain a full solution to the original problem raises further concerns of a different nature.

September 23, 2003 2pm, Room 519 Claremont Tower
Situated Formalisms: Combining Software Function and Context
John Knight

In systems requiring ultra-high dependability, the majority of software defects that are found during testing or after deployment are the result of requirements errors. Of those requirements errors, a significant number occur because of misunderstandings about the system context. Essential details of the application domain are either unknown or misunderstood by developers because of poor communication of application domain knowledge. Current software development practices focus on the formal aspects of software. While formalisms are the only structures required to communicate with a machine, contextual information is required for developers to communicate with one another and establish software validity. The pervasive medium for this communication, natural language, is understood to be problematic for high-precision communication because of its characteristic ambiguity and informality. However, natural language possesses its own body of research results and is amenable to rigorous inspection. We have analyzed the domain knowledge communication problem as it arises in software engineering from the perspective of current cognitive linguistic theory, and this analysis has yielded a model that helps to explain sources of ambiguity and other problems with the use of natural language. Using this model we have developed a new artifact that combines software function and essential context information in a rigorous entity that we refer to as a situated formalism. In this presentation, I briefly summarize the linguistic model and insights derived from it, e.g., that the considered use of natural language performs a function unachievable by formal means. I will explain how these insights are exploited to motivate the structure of the situated formalism and discuss a preliminary practical representation. Finally, I will present some details of our applications of the concepts discussed.

July 9, 2003 2.30 pm, Room 519 Claremont Tower
Social Informatics @ Newcastle: The first three years.
Mike Martin

The Social Informatics Group has been in informal operation for about three years now. It represents a grouping from Computer Science, the Centre for Urban and Regional Development Studies and the School of Management and the Centre for Health Services Research. Its attention has been focussed on the large scale complex socio-technical problems associated with the transformation of Public Services and we have been undertaking significant action research and development projects with the NHS, in Local Authorities, in Social Services Departments and with development agencies in the Region and in Europe. Some significant results are beginning to emerge about the nature of the space in which Social Scientific, Management and Architectural Discourses interact and this seminar will explore some of them. In particular, we will question what it means to be systematic in the face of complex and contested socio-political contexts such as social, health and education service. We will also explore the processes of sensemaking and organisational change in which technical systems and infrastructures are deeply and problematically implicated.

May 28, 2003 3pm, Room 519 Claremont Tower
Real-Time Networks - Rationale and Practice
Hugo Simpson

System architecture is arguably the most important factor in determining whether a computing system can be economically developed, and then be relied upon to meet its specified requirements. The real-time network architecture is specially formulated to cope with the development of large, embedded, distributed, and dependable real-time systems. In this context, a large system is one requiring 100s of man years for its development. The principal features of the architecture will be described, together with the history of its evolution over some 35 years of practical application. Special attention will be given to the intercommunication data area (ida) concept. An ida is a multi-threaded component for process interaction which distinguishes the real-time network approach from other methods. A family of protocols for defining the dynamic properties of an important class of ida types will be described. The talk will conclude with an account of some recent and current applications, and opportunities for further research and development will be identified.

May 21, 2003 11am, Room 519 Claremont Tower
The Inferno Distributed Operating System
Michael Jeffrey

The construction of distributed systems has been hampered by the lack of a clean, perspicuous model for its components. Researchers at Bell Labs Computer Science Centre (headed by Dennis Ritchie) advocated and pushed to the limit the idea of representing all resources (physical devices, services, control points and dynamic data structures) as files. They noted that all systems (well almost) use files to represent data, arranged in a hierarchical naming scheme. Extending this scheme to encompass all resources (local and remote) makes use of a naming and classification scheme that is well understood not just by programmers but lay people as well. This seminar provides an introduction to the Inferno operating system which makes use of this idea and demonstrates how it can be used in the construction of distributed (Grid) systems. During the course of the seminar there will be a demonstration of a distributed system encompassing a range of computing devices, large and small.

May 8, 2003 2.30pm, Room 120 Claremont Tower
APSS: Asynchronous Proactive Secret Sharing
Fred Schneider

A proactive secret sharing protocol enables a set of secret shares to be periodically refreshed with a new, independent set, thereby thwarting so-called mobile adversary attacks. This talk discusses APSS, a proactive secret sharing protocol for asynchronous systems. APSS resists denial of service attacks, which slow processor execution or impede message delivery and thus violate the defining assumptions of a synchronous system. An informal derivation of the APSS protocol will be given along with protocol transformations that have general applicability in the construction of secure and fault-tolerant distributed computations.

April 3, 2003 3pm, Room 519 Claremont Tower
Capturing Rationale using Rich Traceability
Jeremy Dick

Requirements traceability is now widely recognised as a vehicle for improving many system engineering processes, particularly in assessing completeness through coverage of requirements, and in understanding the impact of change. Most system engineering organisations are at the level of using "elementary" traceability, in which requirements statements are linked to specifications and designs to document the impact relationship. However, the rationale of the links is typically not captured, and stays in the minds of the engineers. "Rich" traceability provides a means of capturing the rationale for the presence of links. This rationale may represent vital design information, sometimes called a "satisfaction argument", explaining how particular requirements are met, and can help a great deal in the understanding of impact. Without a record of such rationale, the design information has to be recovered or reengineered every time a possible change is assessed. Rich traceability can similarly be used for capturing rationale associated with testing, the "validation argument", explaining why a particular set of tests is believed to be sufficient. The seminar presents the concept of rich traceability, and shows some case studies in it use in industry, including in the Railtrack West Coast Main Line modernisation programme. BIOGRAPHY: Dr. Jeremy Dick has worked as a requirements consultant for Telelogic (once QSS) for the last 8 years, and has accumulated considerable experience in helping organisations devise and implement requirements engineering processes. Previous work has included designing formal methods tools, and using them in industry. He is co-author of the most recent Springer book on requirements engineering, "Requirements Engineering",

February 13, 2003 3pm, Room 519 Claremont Tower
Dependable Dynamite - Formal modelling in the commercial development of an optimising dynamic binary translator
John Fitzgerald

Dynamite is an optimising binary translator developed from research prototype to commercial product over the last two years. It allows programs written for one CPU to be executed on another while run-time optimisations are applied to blocks of code in order to recover translation overhead. Dynamite's translation kernel is configured with a variety of front- and back-ends for different instruction sets. For example, translators have been developed for x86-MIPS, Arm-MIPS and PPC-x86 combinations.

Assuring the dependability of Dynamite poses particular challenges. The product is small but intricate, and faces demanding performance and reliability requirements. This seminar will examine the use of model-oriented specification alongside more conventional technology as part of the defect avoidance strategy for Dynamite's software. Formal modelling techniques aim to help designers master system complexity by encouraging abstraction and providing tools to exploit the formal semantics of the model through validation. Modelling technology has advanced considerably in recent years, but what happens when it is faced with the realities of industrial software development for a demanding product in a volatile development environment?

The main features of Dynamite and its development environment will be introduced. The use of formal modelling will be illustrated with examples drawn from the VDM model of the product kernel. The successes and failures of formal modelling in this environment will be identified and form a basis for identifying challenges for formal methods in the future.

February 6, 2003 3pm, Room 519 Claremont Tower
Visualising Information Structures
Keith Andrews

Information visualisation involves the visual presentation of abstract information spaces and structures to facilitate their rapid assimilation and understanding. Information structures include hierarchies, networks, multidimensional tables, and collections of text documents. Techniques from information visualisation are finding increasing application in areas such as information and knowledge management and biotechnology. This talk presents some of the work in information visualisation done at the IICM over the past 10 years, embedded in the context of related work from the field as a whole. Biography Keith Andrews is an associate professor at the Institute for Information Processing and Computer Supported New Media (IICM) at Graz University of Technology, in Austria. His research interests include hypermedia, human-computer interaction, computer graphics, and the web. He is currently pursuing research in the emerging field of information visualisation and was co-chair of the IEEE Symposium on Information Visualization in 2001 and 2002.

November 30, 1999 1pm, Room 701 Coffee & Biscuits at 2pm in the Common Room
Real-time Program Algebra
Ian Hayes

We start from the algebra of regular expressions (Kleene algebra) and look at extensions to give one an algebra for programs. This involves using primitives of assignments, tests and assertions, as well as adding operators to handle infinite iteration. We look at ways to represent important concepts like loop invariants and variants (although we treat the later via well founded relations). The algebra allows one to prove properties like Hoare's "axiom" for loops straightforwardly. For real-time programs infinite iteration becomes much more interesting: we want control programs that (conceptually at least) execute forever. We look at rules for reasoning about possibly infinite iterations, and concepts like non-Zeno behaviour of programs.

November 30, 1999 11am, Room 922 Claremont Tower
*A multi-threaded architecture for cognitive robotics*
Prof. Keith Clark is from Imperial College, London.

We describe a multi-threaded architecture combining elements of Belief, Desires, Intentions (BDI) agent architectures with the goal directed reactive control of Nilsson's Teleo Reactive(TR) programs. TR programs are a rule based programming notation influenced by process control concepts of continuous monitoring and action, but they have parameterized procedures and actions can be TR procedure calls, even recursive calls. A TR procedure is also typically goal directed, the actions of its rules being oriented towards achieving a state of the environment that can be determined by some test of sensor readings. They are thus well suited to implementing robotic control where action routines are selected on the basis of the computational analysis of sensor readings . TR computation comprises nested threads of execution, each thread being the execution of a TR procedure called from its parent thread. The TR procedures of the higher threads can be programmed to monitor beliefs, inferred from sensor readings and a model of the environment, rather than percepts. But to retain reactivity, the lower level threads can still directly test percepts computed from sensor readings. This makes it also suitable for programming hybrid deliberative/reactive robots.Finally, a topmost control thread, which decides which high level TR procedure to invoke based on significant events, such as belief updates or new goals, can be added borrowing from BDI agent architectures. This allows the robot to switch tasks based on message events or sensor reading events that leading to significant changes in the robots higher level beliefs. This is the control architecture currently being used at Imperial both for Multi-agent systems and co-operative robotics applications.

November 30, 1999 ,

• Colloquia
• Systems Research Groups
• ASL
• Security
• University Events
• Events RSS
• Events Atom
• Twitter