|
|
|
Time and place
Friday, 20 September 2002, 13:00 and 15:00
Room: ETH, RZ F21
Program
Jean-Guy Schneider, Swinburne University of Technology
Towards a formal foundation for component technology
13:00-13:45
Bernhard Beckert, Universität Karlsruhe
Object-Oriented design and formal verification of software
15:00-15:45
Refreshments will be served at 14:30 outside of RZ-F21.
Abstracts and biographiesDr. Jean-Guy Schneider, Swinburne University of Technology
The last decade has shown that object technology alone is not enough to cope with the rapidly changing requirements of present-day applications. Component-based systems, on the other hand, achieve the required flexibility and reusability by clearly separating the stable parts of systems (i.e. the components) from the specification of their composition.
However, component technology has suffered from the inherent problem that reusability and extensibility is limited due to position-dependent inter-component communication. To address this problem, we propose to replace position-dependent communication by the communication of forms, a special notion of extensible records.
In this talk, we will introduce the basic concepts of forms, the corresponding form composition operations, and illustrate how the combination of forms and form operations facilitates the specification of flexible and reusable programming abstractions.
We will also discuss benefits of using forms to specify component interfaces and motivate the definition of a form-based process calculus as a formal foundation for software composition in a concurrent and distributed setting.
Jean-Guy Schneider is a lecturer in Software Engineering at the School of Information Technology of Swinburne University of Technology, Melbourne, Australia. His main research interests are in object-oriented programming, scripting and composition languages, and the definition of formal approaches for component-based software engineering. Furthermore, he is interested in agile software development processes (especially focused on component-based development), methodologies and tools for collaborative work environments, as well as the influence and applicability of software development processes in tertiary education. He completed both his M.Sc. in Computer Science in 1992 and his Ph.D. in 1999 at the University of Berne, Switzerland.
Dr. Bernhard Beckert, Universität Karlsruhe
The importance of software verification is increasing as more and more safety and security critical applications emerge, and there is greater demand for high-quality software. Currently, however, tools and methods for software verification do not adequately support the design formalisms (such as UML) and programming languages (such as Java) that are used in practice.
In my talk, I give an overview of the KeY project, which aims to overcome this problem and to facilitate and promote the use of formal verification in an industrial context. The central idea of KeY is to enhance a commercial CASE tool with functionality for formal specification and deductive verification. This allows a gradual integration of formal methods into the software development process without changing the user's familiar modelling environment.
Bernhard Beckert is a scientific assistant at the University of Karlsruhe and a member of the KeY project jointly operated with Chalmers University of Technology, intended to integrate formal software specification and verification into the industrial software engineering processes. He holds a PhD in computer science from the University of Karlsruhe, on tableau methods for theorem proving, and has held a visiting appointment at Imperial College in London. His interests are in theorem proving, logic and deductive software development.
|
|