Difference between pages "Rodin Workshop 2009" and "Rodin Workshop 2013"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
 
imported>WikiSysop
 
Line 1: Line 1:
−
{{TOCright}}
+
==4th Rodin User and Developer Workshop==
  
 +
''June 10-11, 2013''
  
−
= Rodin User and Developer Workshop July 15-17 2009 =
+
Turku, Finland
  
 +
http://wiki.event-b.org/index.php/Rodin_Workshop_2013
  
−
While much of the continued development and use of Rodin takes place within the DEPLOY Project, there is a growing group of users and plug-in developers outside of DEPLOY. In July 2009, DEPLOY organised a workshop at the University of Southampton to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers. For Rodin users the workshop provided an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop provided an opportunity to showcase their tools and to achieve better coordination of tool development effort.  Moving towards an open source development project will mean that features that cannot be resourced from within the project can be developed outside the project.  It will also help to guarantee the longer-term future of the Rodin platform.
+
The purpose of the Rodin workshop
−
This report contains the abstracts of the presentations at the workshop on 16 and 17 July 2009.  The workshop was preceded by a tutorial for Rodin Plug-in developers on 15 July.
+
is to bring together existing and potential users and developers of the Rodin  
 +
toolset and to foster a broader community of Rodin users and developers.
 +
For Rodin users the workshop will provide an opportunity to share tool
 +
experiences and to gain an understanding of on-going tool developments.
 +
For plug-in developers the workshop will provide an opportunity to
 +
showcase their tools and to achieve better coordination of tool
 +
development effort.
  
−
We would like to acknowledge the support of the School of Electronics and Computer Science at the University of Southampton (especially the organisational work of Maggie Bond), the DEPLOY project and additional government funding.
+
Preceding Rodin User and Developer Workshops were held at the University of
 +
Southampton, the University of Düsseldorf and the University of Paris-Est Créteil.
 +
The fourth Rodin workshop will be collocated with the conference iFM 2013: http://www.it.abo.fi/iFM2013/
  
 +
==Registration==
  
−
'''Organisers'''
+
Registration for the Rodin 2013 Workshop is open:
  
−
Michael Butler, University of Southampton
+
http://www.it.abo.fi/iFM2013/rodin_registration.php
  
−
Stefan Hallerstede, Heinrich-Heine-Universität Düsseldorf
+
==Programme==
  
−
Laurent Voisin, Systerel
+
===Monday 10 June - Tutorials===
  
 +
'''12:30 - 13:00'''  Registration and coffee
  
−
== [http://deploy-eprints.ecs.soton.ac.uk/137/ Report containing the abstracts is available here] ==
+
'''13:00 - 14:45''' Colin Snook: ''UML-B tutorial''
  
−
== Slides from presentations ==
+
'''14:45 - 15:15''' Coffee
  
−
=== Wednesday 15 July ===
+
'''15:15 - 17:00'''  Jens Bendisposto, Sebastian Krings: ''ProB Tutorial''
  
−
Laurent Voisin and
+
===Tuesday 11 June - Presentations===
−
Stefan Hallerstede,
 
−
[http://wiki.event-b.org/images/Rodin_plug-in_tutorial_2009-07-15.pdf Rodin Plug-in Development Tutorial]
 
  
−
===Thursday 16 July===
+
'''09:00 - 10:30 Session 1'''
  
−
* Michael Butler, [http://wiki.event-b.org/images/Intro.pdf Introduction]
+
*Yuliya Prokhorova, Elena Troubitsyna, Linas Laibinis: ''Supporting Formal Modelling in Event-B with Safety Cases''
  
−
* Ken Robinson, System Modelling and Design: Refining Software Engineering
+
*Tsutomu Kobayashi, Fuyuki Ishikawa, and Shinichi Honiden: ''Systematic Planning of Refinement in Event-B''
  
−
* Jean-Raymond Abrial, [http://deploy-eprints.ecs.soton.ac.uk/138/ Doing Mathematics with the Rodin Platform]
+
*Colin Snook, Michael Butler: ''iUML-B Diagram Developments''
  
−
* Stephen Wright, Experiences with a Quite Big Event-B Model
+
*Neil Evans, Neil Grant, Helen Marshall, James Sharp, Michael Butler, John Colley, Andy Edmunds, Colin Snook: ''The Co-Design Architecture (CODA) Methodology and Plug-in Tool, Progress Update''
  
−
* John Colley,  [http://wiki.event-b.org/images/ColleyJuly09.pdf On Proving with Event-B that a Pipelined Processor Model Implements its ISA Specification]
+
'''10:30 - 11:00 Coffee'''
  
−
* Fangfang Yuan, [http://wiki.event-b.org/images/soton-workshop.pdf Quantitative Design Decisions Measurement using Formal Method]
+
'''11:00 - 12:30 Session 2'''
 +
                 
 +
* Laurent Voisin and Minh-Thang Khuu: ''Domain Specific Event-B Modeling''
  
−
* Kriangsak Damchoom and Michael Butler,  [http://www.event-b.org/rodin09/FlashFileSysRodinWorkshopJuly2009.ppt An Experiment in Applying Event-B and Rodin to a Flash-Based Filestore]
+
* Ulyana Tikhonova, Maarten Manders, Mark van den Brand, Suzana Andova, and Tom Verhoeff: ''Event-B for Defining the Dynamic Semantics of a DSL''
  
−
* Philipp Ruemmer,  [http://wiki.event-b.org/images/Talk_rodin09_philipp_ruemmer.pdf A Theory of Finite Sets, Lists, and Maps for the SMT-Lib Standard]
+
* Jens Bendisposto, Philipp Korner and Michael Leuschel: ''Parallel Model Checking of B Specifications''
  
−
* Matthias Schmalz, [http://wiki.event-b.org/images/Atp_improvements.pdf Better automated theorem proving in Event-B]
+
* Sebastian Krings, Jens Bendisposto, Ivaylo Dobrikov and Michael Leuschel: ''B Constrained''
  
−
* Issam Maamria, [http://wiki.event-b.org/images/Proposal_for_Rule-based_prover.pdf Proposal for an extensible rule-based prover for Event-B]
+
'''12:30 - 13:30 Lunch'''
  
−
* Gudmund Grov,  [http://wiki.event-b.org/images/Reasoned_modelling.pdf A Proposal for a Rodin Proof Planner & Reasoned Modelling Plug-in]
+
'''13:30 - 14:30 Session 3'''
 +
                 
 +
* '''Invited Talk''' - Luigia Petre, Elena Troubitsyna and Marina Waldén: ''On Kaisa Sere's Contributions to Refinement Research''
  
−
* Jens Bendisposto, [http://wiki.event-b.org/images/Using_and_extending_prob.pdf  Using and Extending ProB]
+
'''14:30 - 15:15 Session 4'''
  
−
* Ilya Lopatkin, Towards the SAL plugin for the Rodin platform
+
* Thai Son Hoang: ''Generic Instantiation and Tool Support''
  
−
* Kenneth Lausdahl and Miguel Ferreira, An Overview of Overture
+
* Alexei Iliasov, Linas Laibinis, Elena Troubitsyna, Alexander Romanovsky: ''Support for Indexed Modules in Event-B''
  
−
* Michael Butler,  [http://wiki.event-b.org/images/Roadmap.pdf Roadmap for the Rodin Tool]
+
'''15:15 - 15:45 Coffee'''
  
−
===Friday 17 July===
+
'''15:45 - 17:15 Session 5'''
  
−
* Aryldo G Russo, [http://wiki.event-b.org/images/ICFEM_2009_revised_presentation.pdf Formal Methods Outside the Mother Land  ]
+
* Andy Edmunds: ''Developments in Code Generation Tools for Event-B''
  
−
* Maria Teresa Llano, [http://wiki.event-b.org/images/RodinWorkshopPresentation.pdf Systems Evolution via Animation and Reasoning]
+
* Sergey Ostroumov , Leonidas Tsiopoulos , Juha Plosila , Kaisa Sere: ''Derivation of Structural VHDL from Component-Based Event-B Models''
−
* Atif Mashkoor, BRANIMATION
 
  
−
* Fredrik Degerlund and Richard Grönblom, A Framework for Code Generation and Scheduling of Event-B Models
+
* Vitaly Savicks, Michael Butler, Jens Bendisposto, John Colley: ''Co-simulation of Event-B and Continuous Models in Rodin''
  
−
* Andy Edmunds, [http://wiki.event-b.org/images/RodinWorkshop2009.pdf Code Generation from Event-B - Using an Intermediate Specification Notation]
+
* Adisak Intana, Michael R. Poppleton, and Geoff V. Merrett: ''Proof-based formal methods for WSN development with Simulation Approach''
  
−
* Alexei Iliasov, On Event-B and Control Flow
+
==Organisers==
  
−
* Michael Jastram, [http://wiki.event-b.org/images/Requirements-quo-vadis.pdf Requirements Traceability]
+
Michael Butler, University of Southampton
  
−
* Joris Rehm, LORIA, [http://wiki.event-b.org/images/Timed_machine_plugin_visual.pdf A Rodin plugin for quantitative timed models]
+
Stefan  Hallerstede, Aarhus University
  
−
* Renato Silva, [http://wiki.event-b.org/images/Composition,_Renaming_and_Generic_Instantiation.pdf Composition, Renaming and Generic Instantiation in Event-B Development] 
+
Thierry Lecomte, ClearSy
  
−
* Abderrahman Matoussi, [http://wiki.event-b.org/images/Slides_matoussi_-Southampton-.pdf Expressing KAOS Goal Refinement Patterns with Event-B ]
+
Michael Leuschel, University of Düsseldorf
  
−
* Eduardo Mazza, A tool for specifying and validating software responsibility
+
Alexander Romanovsky, Newcastle University
  
−
* Mar Yah Said, Language and Tool Support for Class and State Machine Refinement in UML-B
+
Laurent Voisin, Systerel
−
 
 
−
* Colin Snook, [http://wiki.event-b.org/images/An_EMF_framework_for_EventB.pdf An EMF Framework for Event-B]
 
  
−
* James Sharp, Using CSP Refusal Specifications to Ensure Event-B Refinement
+
Marina Walden, Åbo Akademi University

Revision as of 21:31, 13 May 2013

4th Rodin User and Developer Workshop

June 10-11, 2013

Turku, Finland

http://wiki.event-b.org/index.php/Rodin_Workshop_2013

The purpose of the Rodin workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers. For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop will provide an opportunity to showcase their tools and to achieve better coordination of tool development effort.

Preceding Rodin User and Developer Workshops were held at the University of Southampton, the University of Düsseldorf and the University of Paris-Est Créteil. The fourth Rodin workshop will be collocated with the conference iFM 2013: http://www.it.abo.fi/iFM2013/

Registration

Registration for the Rodin 2013 Workshop is open:

http://www.it.abo.fi/iFM2013/rodin_registration.php

Programme

Monday 10 June - Tutorials

12:30 - 13:00 Registration and coffee

13:00 - 14:45 Colin Snook: UML-B tutorial

14:45 - 15:15 Coffee

15:15 - 17:00 Jens Bendisposto, Sebastian Krings: ProB Tutorial

Tuesday 11 June - Presentations

09:00 - 10:30 Session 1

  • Yuliya Prokhorova, Elena Troubitsyna, Linas Laibinis: Supporting Formal Modelling in Event-B with Safety Cases
  • Tsutomu Kobayashi, Fuyuki Ishikawa, and Shinichi Honiden: Systematic Planning of Refinement in Event-B
  • Colin Snook, Michael Butler: iUML-B Diagram Developments
  • Neil Evans, Neil Grant, Helen Marshall, James Sharp, Michael Butler, John Colley, Andy Edmunds, Colin Snook: The Co-Design Architecture (CODA) Methodology and Plug-in Tool, Progress Update

10:30 - 11:00 Coffee

11:00 - 12:30 Session 2

  • Laurent Voisin and Minh-Thang Khuu: Domain Specific Event-B Modeling
  • Ulyana Tikhonova, Maarten Manders, Mark van den Brand, Suzana Andova, and Tom Verhoeff: Event-B for Defining the Dynamic Semantics of a DSL
  • Jens Bendisposto, Philipp Korner and Michael Leuschel: Parallel Model Checking of B Specifications
  • Sebastian Krings, Jens Bendisposto, Ivaylo Dobrikov and Michael Leuschel: B Constrained

12:30 - 13:30 Lunch

13:30 - 14:30 Session 3

  • Invited Talk - Luigia Petre, Elena Troubitsyna and Marina Waldén: On Kaisa Sere's Contributions to Refinement Research

14:30 - 15:15 Session 4

  • Thai Son Hoang: Generic Instantiation and Tool Support
  • Alexei Iliasov, Linas Laibinis, Elena Troubitsyna, Alexander Romanovsky: Support for Indexed Modules in Event-B

15:15 - 15:45 Coffee

15:45 - 17:15 Session 5

  • Andy Edmunds: Developments in Code Generation Tools for Event-B
  • Sergey Ostroumov , Leonidas Tsiopoulos , Juha Plosila , Kaisa Sere: Derivation of Structural VHDL from Component-Based Event-B Models
  • Vitaly Savicks, Michael Butler, Jens Bendisposto, John Colley: Co-simulation of Event-B and Continuous Models in Rodin
  • Adisak Intana, Michael R. Poppleton, and Geoff V. Merrett: Proof-based formal methods for WSN development with Simulation Approach

Organisers

Michael Butler, University of Southampton

Stefan Hallerstede, Aarhus University

Thierry Lecomte, ClearSy

Michael Leuschel, University of Düsseldorf

Alexander Romanovsky, Newcastle University

Laurent Voisin, Systerel

Marina Walden, Åbo Akademi University

Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Workshop_2009&oldid=8963’