Alloy and Belay

[Joe Gibbs Politz]

I've put up two posts about modeling parts of Belay with Alloy.  In our most promising foray into formalisms yet, we've successfully defined the trustedness of launch, one of our concerns with the current implementation.  The first post is an overview of the problem and the approach, the second is a deep dive into the details of building up the model.  Another, future post will finish the story of how we fixed the model to address the problems we found, but these were getting long enough already.

https://sites.google.com/site/belayresearchproject/team-blog/modelingclientcommunicationinbelay

https://sites.google.com/site/belayresearchproject/team-blog/understandingbelaywithalloy

Cheers,

Joe P.