Protocols to be analyzed

[김도영 <di...@gmail.com>]

Hi! I’m Doyoung, GSoC Student.

I’m working on [REEF-1745] Formal analysis on REEF protocols.

I’m learning TLA+ for formal verification but I’m not certain about what protocols could be analyzed on REEF.

Any suggestion would be great for me!

Thanks,
Doyoung

Re: Protocols to be analyzed

[Douglas Service <ds...@gmail.com>]

We currently have a protocol between the Java and C# sides of the bridge
that is implemented with using interop between Java-> managed C++ -> C# and
back. I am currently switching this interface to use Avro messages so we
can remove the managed C++ which is not supported on Linux and split the
bridge into two process. I am in the process of finishing up the Avro
serialization classes on both sides and should have a pull request for JIRA
REEF-1763 soon which will contain the networking code, avro messaging
framework, and replace the SystemOnStart interop call. Once this is
reviewed and submitted the other interfaces should follow quickly as the
messaging infrastructure will be in place. Moving this interface to Avro
should allow any language that has Avro bindings to be supported in REEF.

This interface would be a great place to start with verification as it is
an important interface and we may decide to change it based on your results.

Doug

On Thu, May 25, 2017 at 12:41 AM, 김도영 <di...@gmail.com> wrote:

> Hi! I’m Doyoung, GSoC Student.
>
> I’m working on [REEF-1745] Formal analysis on REEF protocols.
>
> I’m learning TLA+ for formal verification but I’m not certain about what
> protocols could be analyzed on REEF.
>
> Any suggestion would be great for me!
>
> Thanks,
> Doyoung
>