Mailing-List: contact dev-help@reef.apache.org; run by ezmlm
Precedence: bulk
Reply-To: dev@reef.apache.org
Date: Sat, 18 Mar 2017 16:28:41 +0000 (UTC)
From: "Gyewon Lee (JIRA)" <jira@apache.org>
To: dev@reef.apache.org
Message-ID: <JIRA.13045869.1487905865000.57129.1489854521563@Atlassian.JIRA>
In-Reply-To: <JIRA.13045869.1487905865000@Atlassian.JIRA>
References: <JIRA.13045869.1487905865000@Atlassian.JIRA> <JIRA.13045869.1487905865389@jira-lw-us.apache.org>
Subject: [jira] [Commented] (REEF-1745) Formal analysis on REEF protocols
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 7bit
archived-at: Sat, 18 Mar 2017 16:28:47 -0000


    [ https://issues.apache.org/jira/browse/REEF-1745?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=15931266#comment-15931266 ] 

Gyewon Lee commented on REEF-1745:
----------------------------------

To students who are interested in this issue as a possible GSoC 2017 topic,

I think only verifying protocols' correctness is not enough to be a good GSoC topic, because the verification itself cannot contribute to the REEF code base.
When writing a GSoC proposal on this issue, you should have a concrete plan on how to improve current protocol designs based on the formal analysis.

It would be also good to have one more proposal on another issue, in case that you fail to find any bugs on REEF protocols thus cannot contribute to REEF code base.


> Formal analysis on REEF protocols
> ---------------------------------
>
>                 Key: REEF-1745
>                 URL: https://issues.apache.org/jira/browse/REEF-1745
>             Project: REEF
>          Issue Type: Improvement
>            Reporter: Gyewon Lee
>              Labels: gsoc2017
>
> In REEF, there are some protocols which are used for communication between different components(ex. Driver <-> Evaluator, C# <-> Java), but we don't have any formal specifications on them. This topic has been discussed in reef developer mailing list.
> Writing formal specifications on these protocols will help us find bugs and verify the correctness of the protocols. TLA+(http://lamport.azurewebsites.net/tla/tla.html) and Alloy(http://alloy.mit.edu/alloy/) are suggested as possible tools.


--
This message was sent by Atlassian JIRA
(v6.3.15#6346)