keynote speakers

   Ian Hayes:               U of Queensland, Australia

Keynote 1

 9:00 - 10:00, Wednesday, 5 November 2003

Speaker:

Prof. Ian Haye

Title:

Programs as Paths

Abstract:

We show how a program can be decomposed into a set of possible execution paths. These can be described in terms of primitives such as assignments, assumptions, guards, (finite or infinite iterated) sequential composition and nondeterministic choice. Some of these cannot possibly be followed (they are dead or infeasible), some may be terminating, and some nonterminating.
Decomposing programs into paths provides a foundation for analysing properties of programs. Our motivation is timing constraint analysis of real-time programs, but the same techniques can be of use for program testing. In general the set of execution paths for a program is infinite. For timing analysis we would like to decompose a program into a finite set of subpaths that covers all possible execution paths, in the sense that we only have to analyse the subpaths in order to determine suitable timing constraints that cover all execution paths.
 

Bio:

Dr. Ian Hayes is a Professor in the School of Information Technology and Electrical Engineering at The University of Queensland. His research interests include formal methods for the specification and development of computer systems, especially for safety-critical systems. His research includes both theoretical work to develop better methods of system construction, and the practical application of the theory to industrially-relevant case studies. In 80s Professor Hayes took part in a collaborative project between Oxford University and IBM (UK) Laboratories. This was one of the first projects to apply the formal specification language Z in industry. He also edited of a volume of Z specification case studies. His recent work has concentrated on formal methods for specifying and developing real-time systems, the role of modularity in formal methods, and computer-based support for formal methods. He is on the editorial board of Formal Aspects of Computing.

Keynote 2

9:00 - 10:00 Thursday, 6 November 2003

Speaker:

Dr. Colin O'Halloran

Title:

Model Based Formal Code Verification

Abstract:

Model based development languages, such as Simulink and UML, are increasing in popularity. Simulink is a de-facto standard in control systems engineering and UML is the subject of a significant standardisation effort. These "standardised" model based languages have commercial tool support, which primarily address the customer's immediate demands. In this paper I shall discuss the trends that are leading to an opportunity for formal methods to deliver significant benefits to industrial software development. Insights from an industrial application of formal methods and an experiment that compares a formal and a conventional development are drawn from.
กก

Bio:

Dr. Colin O'Halloran has a BSc. in mathematics from Warwick University and a DPhil. from Oxford University. He carries out research into mathematically based assurance techniques and leads the Systems Assurance Group within QinetiQ, which applies research results to industrial projects. He was a member of the board of inquiry into the first flight failure of Ariane 5 in 1996. He is a Visiting Fellow of Kellog College Oxford and has recently been appointed to a Visiting Chair at York University.

Keynote 3

9:00 - 10:00 Friday, 7 November 2003

Speaker:

Dr. Mathai Joseph

Title:

Adding Formalism to Methods or
Where and When Will Industry Use Formal Reasoning?

Abstract:

In this talk, I argue that there is a great deal more that formal reasoning can do for software development. There are many problems in large-scale software development where the existing methods are quite inadequate and any contribution from formal reasoning would result in great improvement. Some of these methods will benefit from the systematic use of lightweight formalisms, others from the insights that can come from the kind of analysis that formal reasoning makes possible (e.g. discovering "missing
scenarios"). There may be no obvious method to the use of formal reasoning itself in these cases, i.e. no "formal method", but instead there can be the addition of formal analysis to some existing method.

I will first describe two systems built in the last few years. System One is a cross-border trading system of considerable size and complexity which was built using modern software development techniques and tools. System Two is a safety critical system built
for a highly automated freight railway network using formal specification and an automated tool to develop the final software system. I will then describe where formal reasoning could have played a role in the development of the first system and how "standard" software development methods were used along with formal reasoning in the second.
 

Bio:

Mathai Joseph is Executive Director of Tata Research Development and Design Centre in Pune, India. This is the research centre for Tata Consultancy Services. Among other things, he is responsible for bringing the TRDDC software tools into the market.

He was formerly Professor of Computer Science, University of Warwick, for 12 years and worked on formal aspects of real-time and fault-tolerant systems. While at Warwick, he started the conference series, Formal Techniques in Real-time and Fault-tolerant Systems. Before Warwick, he was at the Tata Institute of Fundamental Research in Mumbai for many years.