Guus Bosman

software engineering director


You are here

vu

3rd assignment

ABP before and after bcg_min

I've been working on the 3rd assignment of Formal Methods today.

The assignments basically involve describing various systems in a formal language, and then generating a state-space of it. There are a number of tricks to reduce this state-space, while some properties will still hold. This way it's easy to prove certain behaviour.

In the assignment I did today (not quite finished yet), the goal is to prove that the alternating-bit protocol is a good protocol. That is, that a bit put in from one side will come out from the other one (even though the channels might be unreliable). After reduction of the original state-space (left), only 3 states remain: 0 (nothing going on), 1 (a 1 is sent and received) and 2 (a 0 is sent and received). The thing we proved this way is that there is no 'state 3' in which for example a 1 is sent and a 0 received (this would be an error).


Tomorrow I'll go to Chess and continue there because I want to print a few of the state-spaces. This to help me understand exactly how the state-space reduction algorithms work.

Recent comments

Recently read

Books I've recently read: