reef-dev mailing list archives

Site index · List index
Message view « Date » · « Thread »
Top « Date » · « Thread »
From "Gyewon Lee (JIRA)" <>
Subject [jira] [Commented] (REEF-1745) Formal analysis on REEF protocols
Date Sat, 18 Mar 2017 16:28:41 GMT


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:
>             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+( and Alloy(
are suggested as possible tools.

This message was sent by Atlassian JIRA

View raw message