| changeset 1050 | 0c36c6a52a1d |
| 1049:92de80b43d28 | 1050:0c36c6a52a1d |
|---|---|
1 Isabelle Verification of the Alternating Bit Protocol by |
|
2 combining IOA with Model Checking |
|
3 |
|
4 ------------------------------------------------------------- |
|
5 |
|
6 Correctness.ML contains the proof of the abstraction from unbounded |
|
7 channels to finite ones. |
|
8 |
|
9 Check.ML contains a simple ModelChecker prototype checking Spec against |
|
10 the finite version of the ABP-protocol. |