The Requirements Engineering Specialist Group
of the British Computer Society
:
About
Join the RESG
Mailing List
Events
RQ Newsletter
RE Sources
Search & Map
Home
Contact Us
Past RESG Event
Formal-Lite RE
Slides from each speaker are available below before the respective abstract.
Date
Wednesday, 19 September 2007
Venue
King’s Manor, Huntingdon Room, University of York
(See bottom of page for maps and directions.)
This one-day event gives a light overview of state-of-the-art in formal methods - mathematical approaches to software and system development which support the rigorous specification, design and verification of computer systems.
The event combines a morning tutorial on formal methods, delivered by John Fitzgerald, and an afternoon panel of distinguished speakers providing a snapshot of current use of formal methods in practice and research.
Programme
0930 Registration & Coffee
1000 John Fitzgerald (Newcastle University). Tutorial, part I
"Lightweight Formal Methods"
Slides (ppt)
Abstract:
The term "lightweight formal methods" gained currency just over ten
years ago following the publication of several strongly-worded papers
calling for techniques and tools that provide at least some of the
benefits of formalism, without requiring the wholesale adoption of
highly specialised technology. In this tutorial, we will examine the
formal methods community's response to this challenge and discuss the
state of the art.
We will briefly review some basic concepts of formal methods, the
benefits claimed for them, and the perceived barriers to their use. We
will identify developments in tool support, and in the formalisms
themselves, aimed at lowering those barriers. Drawing on experience
developing tools and methods for one particular model-based formalism,
VDM, we will discuss some of the fascinating challenges faced by
researchers and practitioners in this lively field today.
1100 Break
1130 John Fitzgerald (Newcastle University). Tutorial, part II (Continued from above.)
1230 Lunch
1345 Michael Jackson (Independent Consultant).
"Formality and Non-Formality"
Slides (pdf)
Abstract: As Dijkstra showed so convincingly, a program can usefully be regarded as a formal object: the programmer's task is to develop the program to satisfy the given formal specification. However, a software-intensive system is not just software: the problem world, in which the effects of the software execution must satisfy the system requirements, is largely non-formal. The relationship between the formality of the software and the non-formality of the problem world has a deep impact on the software development task and on what we can realistically expect from it.
1430 Anthony Hall (Independent Consultant).
"Integrating Formality into Requirements Documents"
Slides (pdf)
Abstract: Formal methods play a valuable role in requirements documents, but they do not replace other notations and approaches. Rather they strengthen certain aspects of the descriptions - in particular the so-called model-based approaches - that are used in more conventional requirements practice. Formal notations therefore need to be integrated into existing natural language, graphical and semi-formal description, and formal analysis needs to be combined with other techniques to explore and validate requirements statements. In this talk I will describe our approach to integrating formal methods in large projects. I will draw some conclusions about the implications of our experience for formal notations and their supporting tools.
1515 Emmanuel Letier (University College London).
"Goal-Oriented Requirements Engineering: Applying Formal Reasoning When and Where Needed"
Slides (pdf)
Abstract: Goal-oriented requirements engineering is an increasingly popular paradigm for elaborating software requirements. It provides a semi-formal, graphical language for structuring requirements by relating them to higher-level goals organized in a refinement hierarchy, and systematic support for incrementally eliciting, modelling, and reasoning about such goal structures. An optional formal layer seamlessly integrates with the semi-formal layer to provide more precise reasoning when and where needed, i.e. on the most critical parts of the system. Formal specification patterns are used to facilitate precise modelling by hiding the intricacies of formal notations from the requirements engineers. These techniques have been applied in various industrial settings including domains such as health care, air traffic control, the food industry, publishing, etc. The talk will describe using a running example how to apply a goal-oriented method and its associated formal reasoning techniques to elaborate requirements for complex systems.
16:00 Panel & Questions
16:45 Close
The Speakers
John Fitzgerald is a Reader in Computing Science at Newcastle
University. He is a specialist in the engineering of dependable
computing systems, particularly in rigorous analysis and design tools. His research concerns the use of formal methods, especially
machine-assisted proof, to analyse models of systems in the early stages of development. John is Chairman of Formal Methods Europe, the international association bringing together researchers and practitioners in rigorous methods of systems development. He is a member of the Committee of the BCS Special Interest group on Formal Aspects of Computing (BCS-FACS).
Michael Jackson has worked in computer software since 1961. Since 1989 he has worked as an independent consultant and researcher in software development method.
He has described his work in many papers and in four books: Principles of Program Design (1974); System Development (1983); Software Requirements & Specifications (1995); and Problem Frames (2001). He has held a number of visiting posts at universities in England and Scotland. He is currently a visiting research Professor at the Open University and a visiting Fellow at the University of Newcastle.
Anthony Hall is an independent consultant and an associate of Praxis High Integrity Systems. He currently works both independently and with Praxis on the development of operational systems in air traffic control and other high-integrity areas. During his years working as a Principal Consultant for Praxis Critical Systems, he developed methods for combining rigorous specification with object-oriented design, resulting in software architectures that are maintainable and changeable with very high assurance.
Emmanuel Letier is a Lecturer in the Department of Computer Science,University College London. His research interests are in systems requirements engineering, software design, and the use of practical formal modelling and analysis techniques to support these activities.
Registration
Registration is required.
Morning Tutorial: £50 (RESG Members) / £65 (Non-Members)
Afternoon Talks: Free (RESG Members) / £10 (Non-Members)
Please download and complete the registration form and send to Ljerka Beus-Dukic (L.Beus-Dukic@westminster.ac.uk) at the address provided.
Maps and Directions
The event is going to be held in the King’s Manor, University of York, Huntingdon Room.
Information on how to reach the King’s Manor buildings at the University of York can be found at http://www.york.ac.uk/np/maps/kmdirect.htm.
Parking at King's Manor is not generally available to delegates
attending meetings. There is public parking at Bootham Row and at
Marygate, both close by - see http://www.york.gov.uk/parking/parkingmap.html.
The cheapest way to visit York by car is to use the Park & Ride service.
For King's Manor, use the Rawcliffe Bar site, getting off either in
Museum Street or Bootham - see
http://www.firstgroup.com/ukbus/yorkhumber/york/map/index.php
for city maps (Route 2 P&R), and
http://www.york.gov.uk/transport/Parking/Park_and_Ride/5Rawcliffe_Bar1/
for car-access information.
King's Manor is less than a 10-minute walk from York Railway Station.
[Back]