Workshop on
Refinement Based Development of Software Systems using Event-B
15 - 16 July. 2011
Indian Institute of Science, Bangalore, India
This workshop
will address the key role played by formal modelling
and verification in systems engineering. Modelling
may be used at all stages of the development process from requirements analysis
to system acceptance testing. Formal modelling and verification lead to deeper understanding and
higher consistency of specification and design than informal or semi-formal
methods. In order to manage system complexity, composition, decomposition and
refinement of formal models are key methods for structuring the formal modelling effort since they support separation of concerns
and layered reasoning. A refinement approach means that models and compositions
of models represent different abstraction levels of system design; consistency
between abstraction levels is ensured by formal verification.
This workshop will provide an intensive introduction to Event-B
and Rodin platform. Event-B is a formal method for
system-level modelling and analysis. The key features of Event-B are the use of
set theory as a modelling notation, the use of refinement to represent systems
at different abstraction levels and the use of mathematical proof to verify the
consistency between refinement levels. Event-B is an extension of the B-Method.
The B-method has been successfully used in the
development of many complex high integrity systems. The prominent among them
are the Driverless Train controller in Paris Metro (Line 14), the controllers
for the Light Driverless Shuttle for Paris-Roissy
airport and Platform Screen-Door Controllers.
The Rodin Platform is an Eclipse-based IDE for Event-B
that provides effective support for refinement and mathematical proof. The
platform is open source, contributes to the Eclipse framework and is further
extendable with plugins.
Michael Butler (University
of Southampton, UK)
Colin Snook (University of
Southampton, UK)
S. Ramesh (GM R&D, Bangalore)
Manoranjan Satpathy (GM R&D
Bangalore)
Deepak D'Souza
(IISc, Bangalore) [deepakd@csa.iisc.ernet.in] (+91
9845688439)
Prahladavaradan Sampath (GM R&D,
Bangalore)[p.sampath@gm.com]
(+91 9341296550)
Manoranjan Satpathy (GM R&D
Bangalore) [manoranjan.satpathy@gm.com] (+91 9341714181)
S. Ramesh
(GM R&D, Bangalore) [ramesh.s@gm.com] (+91 9972589113)
The workshop will be held in the CSA seminar hall (Room 254 in the first floor of the CSA building). More detailed directions and maps can be found here.
|
Friday
15th July 2011 |
||
|
Session 1 |
||
|
9:30 |
Registration |
|
|
10:00 |
Participant interaction and tea |
|
|
Session 2 |
||
|
10:30 |
Next generation design and verification of embedded systems |
Ramesh S, GM
R&D, India Science Lab |
|
11:00 |
System level modelling and reasoning with
Event-B |
Michael
Butler, Univ. of Southampton |
|
11:30 |
Industrial uses of Event-B |
Michael
Butler, Univ. of Southampton |
|
12:00 |
Rodin platform |
Michael
Butler, Univ. of Southampton |
|
13:00 -
Lunch |
||
|
Session 3 |
||
|
14:30 |
Initial introduction to UML-B |
Colin
Snook, Univ. of Southampton |
|
15:15 |
Development of control designs using RRM diagrams |
Manoranjan Satpathy, GM R&D, India Science Lab |
|
16:00 -
Tea Break |
||
|
Session 4 |
||
|
16:30 |
Modelling
control systems in Event-B |
Michael
Butler, Univ. of Southampton |
|
17:30 -
End of Day |
||
|
Saturday
16th July 2011 |
||
|
Session 5 |
||
|
9:00 |
Event-B modelling guidelines |
Michael
Butler, Univ. of Southampton |
|
10:30 -
Tea Break |
||
|
session 6 |
||
|
11:00 |
Refinement in Event-B |
Michael
Butler, Univ. of Southampton |
|
12:00 |
Decomposition in Event-B |
Michael
Butler, Univ. of Southampton |
|
13:00 -
Lunch |
||
|
Session 7 |
||
|
14:00 |
Refinement in UML-B |
Colin
Snook, Univ. of Southampton |
|
15:00 -
Tea Break |
||
|
Session 8 |
||
|
15:30 |
Overview of Proof |
Michael
Butler, Univ. of Southampton |
|
16:00 |
Overview of code-generation |
Michael
Butler, Univ. of Southampton |
|
16:30 |
Wrap-up session |
|
Michael Butler:
Colin Snook:
The registration for the workshop will be by email. There
is no workshop fee, but there is an upper limit on the total number of
participants.
As part of the application, please mention your
affiliation and the position you hold. The students interested in attending the
workshop are requested to include contact details of their supervisors and
heads of the department.
Please email your applications to Prahladavaradan
Sampath or Manoranjan Satpathy with the subject line “[Event-B Workshop 2011]”.
Please feel free to contact us for any further details.