reef-dev mailing list archives

Site index · List index
Message view « Date » · « Thread »
Top « Date » · « Thread »
From Byung-Gon Chun <bgc...@gmail.com>
Subject Re: Formal methods for REEF?
Date Wed, 13 Apr 2016 00:22:15 GMT
I talked about the need of formally specifying REEF protocols long time
ago. :)

TLA+ has been used in some MS projects (e.g., FARSITE) and Amazon products.
There's a book about it.
http://www.amazon.com/Specifying-Systems-Language-Hardware-Engineers/dp/032114306X/ref=sr_1_1?ie=UTF8&qid=1460506815&sr=8-1&keywords=specifying+systems

On Wed, Apr 13, 2016 at 9:18 AM, Markus Weimer <markus@weimo.de> wrote:

> On 2016-04-12 15:16, Dudoladov, Sergey wrote:
>
>> @Markus Which ideas  do you have in mind ?
>>
>
> A good candidate would be the protocol between Driver and Evaluator. We've
> never really formally specified it, nor do we have proofs as to its
> deadlock and race properties.
>
> TLA+ seems like a framework for that sort of task.
>
> Markus
>



-- 
Byung-Gon Chun

Mime
  • Unnamed multipart/alternative (inline, None, 0 bytes)
View raw message