Timothy Bourke, Rob van Glabbeek and Peter Hoefner Mechanizing a process algebra for network protocols Journal of Automated Reasoning, Volume 56, Number 3, pp. 309–341, March, 2016 |
Timothy Bourke Mechanization of the Algebra for Wireless Networks (AWN) [AWN] Archive of Formal Proofs, 2014 |
||
Timothy Bourke and Peter Höfner Loop freedom of the (untimed) AODV routing protocol [AODV] Archive of Formal Proofs, 2014 |
isabelle jedit aodv/Aodv_Loop_Freedom.thyOnce Isabelle has processed a .thy file, you can hold down the ctrl key and click on elements of the proof text to see their formal definitions.
Generic Files [AWN, AODV] | |
Lib.thy | Generic functions and lemmas |
TransitionSystems.thy | Transition systems (automata) |
Invariants.thy | Reachability and Invariance |
OInvariants.thy | Open reachability and invariance |
Algebra of Wireless Networks (AWN) and its Proof Theory [AWN] | |
awn/Toy.thy | Simple toy example |
awn/AWN_Main.thy | Import all AWN-related theories |
awn/AWN.thy | Terms of the Algebra for Wireless Networks |
awn/AWN_SOS.thy | Semantics of the Algebra of Wireless Networks |
awn/AWN_Labels.thy | Labelling sequential processes |
awn/AWN_SOS_Labels.thy | Configure the inv_cterms tactic for sequential processes |
awn/AWN_Cterms.thy | Control terms and well-definedness of sequential processes |
awn/Pnet.thy | Lemmas for partial networks |
awn/Closed.thy | Lemmas for closed networks |
awn/OAWN_SOS.thy | Open semantics of the Algebra of Wireless Networks |
awn/OAWN_SOS_Labels.thy | Configure the inv_cterms tactic for open sequential processes |
awn/OPnet.thy | Lemmas for open partial networks |
awn/OClosed_Lifting.thy | Lifting rules for (open) closed networks |
awn/Inv_Cterms.thy | A custom tactic for showing invariants via control terms |
awn/AWN_Invariants.thy | Generic invariants on sequential AWN processes |
awn/OAWN_Invariants.thy | Generic open invariants on sequential AWN processes |
awn/OAWN_Convert.thy | Transfer standard invariants into open invariants |
awn/Qmsg.thy | Model the standard queuing model |
awn/Qmsg_Lifting.thy | Lifting rules for parallel compositions with QMSG |
awn/ONode_Lifting.thy | Lifting rules for (open) nodes |
awn/OPnet_Lifting.thy | Lifting rules for (open) partial networks |
awn/OClosed_Transfer.thy | Transfer open results onto closed models |
AODV Loop Freedom [AODV] | |
aodv/Aodv_Loop_Freedom.thy | Apply invariants to show loop freedom of the AODV model |
aodv/Aodv_Basic.thy | Constants used in all AODV variants |
aodv/Aodv_Data.thy | Predicates and functions used in the AODV model |
aodv/Aodv_Message.thy | Messages used in the AODV protocol |
aodv/Aodv.thy | Model an instance of the AODV protocol |
aodv/Aodv_Predicates.thy | Predicates for stating invariant assumptions and properties |
aodv/OAodv.thy | Adapt the AODV model for the open semantics |
aodv/Fresher.thy | Relations (of quality) between routes |
aodv/Quality_Increases.thy | Predicate and lemmas for quality increases |
aodv/Seq_Invariants.thy | Invariant proofs over individual sequential processes |
aodv/Global_Invariants.thy | Invariant proofs over open sequential processes |
aodv/Loop_Freedom.thy | Routing graphs and loop freedom from invariance |
AODV Variants [AODV] | |
aodv_tr_verA/Aodv_Loop_Freedom.thy | Loop freedom of AODV variant A |
aodv_tr_verB/Aodv_Loop_Freedom.thy | Loop freedom of AODV variant B |
aodv_tr_verC/Aodv_Loop_Freedom.thy | Loop freedom of AODV variant C |
aodv_tr_verD/Aodv_Loop_Freedom.thy | Loop freedom of AODV variant D |
aodv_tr_verE/Aodv_Loop_Freedom.thy | Loop freedom of AODV variant E |