Difference between pages "FAQ" and "Google Summer of Code 2009"

Revision as of 15:28, 10 March 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.

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) .

Evaluate the tool on a set of example.

Prepare basic documentation for users.

Requirements

Good communication skill.

Good command of Java programming.

Interest in formal methods.

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

Objective

Overall objective

Expectations

List of expected work to be carried out.

Study ...

Implement ...

Requirements

Requirements for students.

Good programming skills in ...

...

Mentor

Matthias Schmalz <someone at somewhere>

Optional

Optional goals

Evaluate ...

Document ...

Mentors

A list of potential mentors.

Laurent ?
Son ?
...

@@ Line 1: / Line 1: @@
-== General ==
+{{TOCright}}
-=== What is event-B? ===
+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&trade;''', 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 [http://code.google.com/soc/ 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. More details are available in http://www.event-b.org/
-=== What is the difference between event-B and the B method? ===
+'''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/ http://www.event-b.org/]
-Event-B is derived from the [http://en.wikipedia.org/wiki/B-Method B method]. Both notations have the same [http://en.wikipedia.org/wiki/Jean-Raymond_Abrial inventor], and share many common concepts (set-theory, refinement, proof obligations, ...) However, they are used for quite different purpose.  The B method is devoted to the development of ''correct by construction'' software, while the purpose of event-B is to model full systems (including hardware, software and environment of operation).
+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 [http://code.google.com/opensource/gsoc/2009/faqs.html 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 lists|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 [http://producingoss.com/en/communications.html#you-are-what-you-write 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|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 ==
-Both notations use a mathematical language which are quite close but do not match exactly (in particular, operator precedences are different).
+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!
-=== What is Rodin? ===
+=== Tool Support for Design Patterns ===
-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.
+'''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) .
+* Evaluate the tool on a set of example.
+* Prepare basic documentation for users.
+'''Requirements'''
+* Good communication skill.
-=== Where does the ''Rodin'' name come from? ===
+* Good command of Java programming.
-The Rodin platform was initially developed within the European Commission funded Rodin project (IST-511599 ), where Rodin is an acronym for "Rigorous Open Development Environment for Complex Systems” .  Rodin is also the name of a famous French [http://en.wikipedia.org/wiki/Auguste_Rodin sculptor], one of his most famous work being the [http://en.wikipedia.org/wiki/The_Thinker Thinker].
+* Interest in formal methods.
-== General Tool Usage? ==
+'''Mentor'''
-=== How do I install external plug-ins without using Eclipse Update Manager? ===
+Thai Son Hoang <htson at inf dot ethz dot ch>.
-Although it is preferred to install additional plug-ins into the Rodin platform using the Update Manager of Eclipse, this might not always be practical. In this case, a manner to install these plug-ins is to emulate either manually or using ad-hoc scripts the operations normally performed by the Update Manager.
-This manual installation of plug-ins is described in ''[[Installing external plug-ins manually]]''.
+'''Optional'''
-=== The builder takes too long ===
+* Basic step-by-step tutorial for using the plug-in.
-Generally, the builder spends most of its time attempting to prove POs.  There are basically two ways to get it out of the way:
-* the first one is to disable the automated prover in the Preferences panel.
-* the second one is to mark some PO as reviewed when you don't want the auto-prover to attempt them anymore.
-Note that if you disable the automated prover, you always can run it later on some files by using the contextual menu in the event-B Explorer.
-To disable the automated prover, open Rodin <tt>Preferences</tt> (menu {{menu|Window > Preferences...}}).  In the tree in the left-hand panel, select {{menu|Event-B > Sequent Prover > Auto-tactic}}. Then, in the right-hand panel ensure that the checkbox labelled <tt>Enable auto-tactic for proving</tt> is disabled.
+=== Integration of External Provers ===
-To review a proof obligation, just open it in the interactive prover, then click on the ''review'' button (this is a round blue button with a ''R'' in the proof control toolbar).  The proof obligation should now labelled with the same icon in the event-B explorer.
+'''Objective'''
-===What are the ASCII shortcuts for mathematical operators===
+Overall objective
-The ASCII shortcuts that can be used for entering mathematical operators are described in the help of the event-B keyboard plug-in.  In the help system, this page has the following path {{menu|Event-B Keyboard User Guide > Getting Started > Special Combos}}.
+'''Expectations'''
-This page is also available in the dynamic help system.  The advantage of using dynamic help is that it allows to display the help page side-by-side with the other views and editors.  To start the dynamic help, click {{menu|Help > Dynamic Help}}, then click {{menu|All Topics}} and select the page in the tree.
+List of expected work to be carried out.
+* Study ...
-===Rodin (and eclipse) doesn't take into account the MOZILLA_FIVE_HOME environment variable===
+* Implement ...
-You have to add a properties by appending the following code to your eclipse/eclipse.ini file:
- -Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner/xulrunner-xxx
-== Modeling and Proving==
+'''Requirements'''
-=== Witness for {{Ident|Xyz}} missing. Default witness generated ===
-A parameter as disappeared during a refinement. If this is intentional, you have to add a [[Witnesses (Modelling Language)|witness]] telling how the abstract parameter is refined.
-=== Identifier {{ident|Xyz}} should not occur free in a witness ===
+Requirements for students.
-You refer to {{ident|Xyz}} in a witness predicate where {{ident|Xyz}} is a disappearing abstract variable or parameter which is not set as the witness label.
-=== In {{event|INITIALISATION}}, I get  ''Witness {{ident|Xyz}} must be a disappearing abstract variable or parameter'' ===
+* Good programming skills in ...
-You should mark the variable as an ''after variable'' by using a tick. The witness label should be {{ident|Xyz'}}, and the predicate should refer to {{ident|Xyz'}} too.
-=== I've added a witness for {{ident|Xyz}} but it keeps saying ''"Identifier {{ident|Xyz}} has not been defined"'' ===
+* ...
-As specified in the [[Witnesses (Modelling Language)|modelling language manual]], the witness must be labelled by the name {{Ident|Xyz}} of the concrete variable being concerned.
-=== How can I do a Proof by Induction? ===
+'''Mentor'''
-[[Induction proof|This page about proof by induction]] will give you some starting tips.
-=== Labels  of proof tree nodes explained ===
+* Matthias Schmalz <someone at somewhere>
-* {{ident|ah}} means ''add hypothesis'',
-* {{ident|eh}} means rewrite with ''equality from hypothesis'' from left to right,
-* {{ident|he}} means rewrite with ''equality from hypothesis'' from right to left,
-* {{ident|rv}} tell us that this goal as been manually [[The_Proving_Perspective_(Rodin_User_Manual)#The_Proof_Control_Window|reviewed]],
-* {{ident|sl/ds}} means ''selection/deselection'',
-* {{ident|PP}} means ''discharged by the predicate prover''
-* {{ident|ML}} means ''discharged by the mono lemma prover''
+'''Optional'''
-== How to contribute? ==
+Optional goals
-See the [[How_To_Contribute|How to contribute]] page.
-== Developer FAQ ==
+* Evaluate ...
-=== Using Rodin-SVN from eclipse consumes too much memory ===
-You can [[#How_do_I_generate_a_Rodin_product_from_SVN.3F|generate a product]] and use it as if it was a normal release.
-=== How do I generate a ''Rodin'' product from SVN? ===
+* Document ...
-In the project ''org.rodinp.platform'', right-click on ''Rodin.platform'' and select {{menu|export}}. Choose {{menu|Plug-in Development > Eclipse product}} and click on {{button|Next}} type <tt>Rodin</tt> for the ''Root directory'', and choose the ''Destination directory''. Then click on {{button|Finish}}.
-=== How do I collect debug information from the Rodin platform? ===
+== Mentors ==
-You may see the log in the console by appending <tt>-consoleLog</tt> to the rodin executable: <code>rodin -consoleLog</code>
-You may add specific debug informations by setting specific options: <code>rodin --debug options.file -consoleLog</code> where {{file|options.file}} contains something like:
+A list of potential mentors.
-<pre>
-org.pluginname/debug = true
-org.pluginname/debug/optionaldebug = true
-</pre>
-where'' optionaldebug'' may be found in the {{file|org.pluginname/.options}} file in the [http://rodin-b-sharp.cvs.sourceforge.net/rodin-b-sharp/ rodin source repository].
-=== How do I submit a patch? ===
+* Laurent ?
-Good practises for patch submission are described [[How to Submit Patches|here]].
+* Son ?
+* ...
-=== How do I track memory leaks? ===
+== Students Considering Application ==
-If you suspect that some memory isn't freed, you may find some useful directions on how to track memory leaks [[Tracking Memory Leaks|here]].
-=== How do I report a bug. ===
-See [[How_To_Contribute#How_do_I_report_a_bug_or_a_feature_request.3F|the ''How to contribute'' page]].
-=== How do I save the models ? ===
+== Applications Received From ==
-After the separation between a file ({{class|IRodinFile}}) and its root (a {{class|IInternalElement}}), that occurred in version 0.9.2, model saving is no more achievable through internal elements. Instead, you have to save the {{class|IRodinFile}}.
- IInternalElement element = ...
- element.getRodinFile().save(...);
+== Project status ==
-[[Category:User FAQ]]
+== Other GSoc Projects related to RODIN ==
-[[Category:Developer FAQ]]

Difference between pages "FAQ" and "Google Summer of Code 2009"

Revision as of 15:28, 10 March 2009

Contents

Notes on applying

Getting things done

Project Ideas

Tool Support for Design Patterns

Integration of External Provers

Mentors

Students Considering Application

Applications Received From

Project status

Other GSoc Projects related to RODIN

Navigation menu

Page actions

Page actions

Personal tools

Navigation

contribute

Search

Tools