Google Summer of Code 2009

For the last few years, Google has offered a fantastic opportunity for students to help out Open Source software projects in the summer while getting paid for it. It's called Google Summer of Code™, and it provides free software projects a great way of attracting development effort while providing software developers who are still in university with some interesting and useful experiences. Find out more about the Summer of Code (SoC) from their site.

Event-B is a formal method for system-level modelling and analysis. 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 consistency between refinement levels. You can know more of Event-B by reading materials available on http://www.event-b.org/

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.

We would like to participate in 2009's Summer of Code.

See also GSoC 2009 FAQ.

Notes on applying

Here are some tips on what you might want to include in your application.

• First of all: get feedback on your proposal from the community. The devel mailing list is a good channel for that. Ask around and get to know some people, see if they think your project is feasible or how you should change the scope to better fit the timeline and the project. (If you are new to Open Source development, reading this part of "Producing OSS" may help you find the right tone.) Talking to people before applying dramatically increases your chances of approval: it shows us that you are genuinely able to communicate your ideas, allows us to gauge your expertise level and see who might be the right mentor for you.

• Tell us about yourself. We don't know you, so it helps if you give an outline of your background and what your prior experiences are (e.g. Open Source development, using Eclipse, general software engineering experience or education). If it turns out you wouldn't be a good fit for the Rodin platform or your project idea, it's helpful for everyone involved if that can be determined before you get started. However, don't hesitate to apply just because this would be your first time working in Open Source or with Eclipse; at some point this was new for each of us.

• Make it clear that you've thought through your application. Don't use a project idea from this page verbatim. Instead, come up with your own proposal, or expand on a proposal from this page. Explore the code a little bit. Make a clear schedule to show the intermediate milestones you'll reach while progressing towards your final goal.

• Let us know why you care, what you like about formal methods in general and Event-B and the Rodin platform specifically, what things you think could be improved and how they could be improved. We like working on this project because this project makes our work more effective, and we hope you'll like it, too. Showing your motivation helps.

Getting things done

Some tips on how you can get to project completion within the scheduled timeline.

• Working on the Rodin platform in the summer should be your main activity. Having a vacation for one or two weeks is fine, of course, but we want you to take the project and the time mentors put into it seriously. If you are working two other jobs this summer, that probably won't work. Realize that collaborating on software development takes time, and not just the time used to reason about and write the code. This also means that we want you to set some intermediate milestones to be able to keep track of your progress.

• Communicate. In some ways, open source software development is more about communicating than about writing code. Some part of your time will be spent writing code, but a large part of the time spent will go towards explaining the code on mailing lists, asking and answering questions on IRC and in general reasoning about proposed software changes. If you can't do this, you take the risk of not understanding the goals of our project or not being able to explain why your patch is necessary.

• We want you to work in the open, with our community. Get on the mailing lists, both to ask for help and to provide it to other users, spend time on IRC (#rodin on irc.freenode.net) discussing your work with other developers.

• We're not going to just compare what you did at the end to what you stated you'd be doing in the beginning. We want you to put effort into the project, to think about the feature you're doing, to communicate with the community and integrate your code with the project. If you end up implementing some other cool feature or fixing some annoyance, that is great as well.

Project Ideas

Here are a bunch of project ideas you might like to apply for. Of course, if you have a different idea of something in the Rodin platform that badly needs fixing or some feature you think would make a difference, go ahead and apply with it!

Tool Support for Design Patterns

Objective Reusing formal models in order to reduce the effort of modelling is an important aspect of Event-B methods. The background theoretical work for design patterns in Event-B has been done as part of a master thesis. The objective of this project is to have a tool support for this work as a Rodin plug-in.

Expectations

- Study the concept of Event-B patterns.

- Study the architecture of the Rodin platform.

- Implement the tool as a Rodin platform plug-in (Eclipse plug-in)

- Prepare basic documentation for users

Requirements - Good communication skill.

- Good command of Java programming.

Mentor

Thai Son Hoang <htson at inf dot ethz dot ch>

Optional

- Basic step-by-step tutorial for using the plug-in.

Integration of External Provers

Mentor

Matthias Schmalz

Mentors

A list of potential mentors.

• Laurent ?
• Son ?
• ...