Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Added CSMA/CA protocol study #2

Open
wants to merge 6 commits into
base: main
Choose a base branch
from
Open

Added CSMA/CA protocol study #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
9e93c32
Added CSMA/CA protocol study
mikucionisaau Mar 29, 2023
2269a93
Link to raw svg instead of compressed
mikucionisaau Mar 29, 2023
cc66863
Added white background to the images
mikucionisaau Mar 29, 2023
50726c7
Added white background
mikucionisaau Mar 29, 2023
aafa78f
Renamed directory to IWIGP2012
mikucionisaau Mar 29, 2023
f38f622
Added CSMA study entry
mikucionisaau Feb 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions CaseStudies/CSMA-CA-IWIGP2012/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
# Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach

_**Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach**_,
Peter E. Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikučionis. *2nd Internation Workshop on Interactions, Games and Protocols (IWIGP 2012)*, March 25, 2012, Electronic Proceedings in Theoretical Computer Science (EPTCS). [[DOI:10.4204/EPTCS.78.1](https://doi.org/10.4204/EPTCS.78.1)]

## Abstract

This paper studies the problem of computing Nash equilibrium in wireless networks modeled by
Weighted Timed Automata. Such formalism comes together with a logic that can be used to describe
complex features such as timed energy constraints. Our contribution is a method for solving this
problem using Statistical Model Checking. The method has been implemented in UPPAAL model
checker and has been applied to the analysis of Aloha CSMA/CD and IEEE 802.15.4 CSMA/CA
protocols.

## Model Files

Uppaal SMC model of CSMA/CA protocol: [csma-ca.xml](csma-ca.xml)

Image from the protocol model:

![CSMA/CA protocol in UPPAAL](csma-ca.svg)
2,559 changes: 2,559 additions & 0 deletions CaseStudies/CSMA-CA-IWIGP2012/csma-ca.svg
View file
Open in desktop
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added CaseStudies/CSMA-CA-IWIGP2012/csma-ca.svgz
View file
Open in desktop
Binary file not shown.
339 changes: 339 additions & 0 deletions CaseStudies/CSMA-CA-IWIGP2012/csma-ca.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,339 @@
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
<nta>
<declaration>/** This CSMA/CA model is described in the following publication:
"Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach"
by Peter E. Bulychev, Alexandre David, Kim G. Larsen, Axel Legay and Marius Mikučionis.
2nd Internation Workshop on Interactions, Games and Protocols (IWIGP 2012),
March 25, 2012, Electronic Proceedings in Theoretical Computer Science (EPTCS).
DOI: https://doi.org/10.4204/EPTCS.78.1
*/

//const int N=10; // CORRECT
const int N=6; // INCORRECT

clock time;

typedef int[0,N-1] id_t;

broadcast chan ready;
broadcast chan go;

broadcast chan a;

bool isTransmitting[N];

const int macMaxCSMABackoffs = 4; // CORRECT
//const int macMaxCSMABackoffs = 1; // INCORRECT

// approved consts
const int UnitBackoff = 20;
const int CCA_duration = 8; // CORRECT
const int aTurnaroundTime = 12; // CORRECT
const int ACK_time = 88;
const int aMaxFrameRetries = 3; // CORRECT

const int macMinBE = 3; // CORRECT
const int macMaxBE = 5; // CORRECT

//const int macMinBE = 0; // INCORRECT
//const int macMaxBE = 0; // INCORRECT

//const int minDataLength = 15*8; // CORRECT
//const int maxDataLength = 6*8; // CORRECT
const int data_length = 35*8; // CORRECT 25*8 - is for header
//const int data_length = maxDataLength;

//const int data_length = 3; // INCORRECT
//const int aTurnaroundTime = 2; // INCORRECT
//const int CCA_duration = 10; // INCORRECT

//const int max_waking_delay=6000; for sound speed is 300 m/s
//const int max_waking_delay=10; //CORRECT for something else
const int max_waking_delay=1000; //CORRECT for something else
//const int max_waking_delay=aTurnaroundTime; //CORRECT to show that is_disrete_waiting qualitatively affects the model // exist
//const int max_waking_delay=aTurnaroundTime + data_length + CCA_duration; //CORRECT to show that is_disrete_waiting qualitatively affects the model // forall

const int aMinLIFSPeriod = 40; // CORRECT

const bool is_discrete_waiting = false;
const bool acknowledgment_supported = true;
const bool recover_from_failures = false;

const int wait_after_failure = 0;

hybrid clock energy;
int RX_Power, TX_Power;</declaration>
<template>
<name x="5" y="5">Process</name>
<parameter>const id_t id</parameter>
<declaration>
int be;
int nb;
int nretries;

int backoff;

int waking_delay;

clock x;

bool cca_passed := false;
bool collision_occured := false;

bool is_busy() {
int i;
for(i=0; i&lt;N; i++) {
if (isTransmitting[i])
return true;
}
return false;
}

void start_sending() {
isTransmitting[id] = true;
}

void finish_sending() {
isTransmitting[id] = false;
}

bool is_conflict() {
bool f = false;
int i;
for(i=0; i&lt;N; i++) {
if (isTransmitting[i]) {
if (f)
return true;
else
f = true;
}
}
return false;
}</declaration>
<location id="id0" x="-2315" y="-1582">
<label kind="invariant" x="-2307" y="-1630">energy' == RX_Power
x&lt;=ACK_Time</label>
</location>
<location id="id1" x="-2523" y="-1846">
<urgent/>
</location>
<location id="id2" x="-2227" y="-1846">
<name x="-2227" y="-1830">FAILURE</name>
</location>
<location id="id3" x="-1891" y="-1846">
<urgent/>
</location>
<location id="id4" x="-2667" y="-1934">
<label kind="invariant" x="-2675" y="-1974">x&lt;=MaxWakingDelay</label>
</location>
<location id="id5" x="-2523" y="-1686">
<label kind="invariant" x="-2507" y="-1718">x&lt;=MinLIFS</label>
</location>
<location id="id6" x="-2523" y="-1934">
<urgent/>
</location>
<location id="id7" x="-2299" y="-1774">
<name x="-2379" y="-1798">SUCCESS</name>
</location>
<location id="id8" x="-2299" y="-1686">
<urgent/>
</location>
<location id="id9" x="-2227" y="-2006">
<urgent/>
</location>
<location id="id10" x="-1891" y="-1582">
<label kind="invariant" x="-1883" y="-1614">x&lt;=TurnAround</label>
</location>
<location id="id11" x="-2123" y="-1686">
<label kind="invariant" x="-2115" y="-1718">x&lt;=ACK_time</label>
</location>
<location id="id12" x="-2123" y="-1846">
<label kind="invariant" x="-2195" y="-1878">x&lt;=aTurnaroundTime</label>
</location>
<location id="id13" x="-1891" y="-2006">
<name x="-2027" y="-2038">TRANSMIT_DATA</name>
<label kind="invariant" x="-2027" y="-2022">x&lt;=FrameLength</label>
</location>
<location id="id14" x="-1891" y="-2134">
<name x="-1995" y="-2158">VULNERABLE</name>
<label kind="invariant" x="-1875" y="-2158">energy' == TX_Power
&amp;&amp; x&lt;=TurnAround</label>
</location>
<location id="id15" x="-2227" y="-2134">
<name x="-2275" y="-2158">CCA</name>
<label kind="invariant" x="-2219" y="-2126">energy' == RX_Power
&amp;&amp; x&lt;=CCA</label>
</location>
<location id="id16" x="-2523" y="-2134">
<name x="-2643" y="-2158">WAIT_BACKOFF</name>
<label kind="invariant" x="-2707" y="-2134">x&lt;=backoff*UnitBackoff</label>
</location>
<location id="id17" x="-2523" y="-2006">
<urgent/>
</location>
<init ref="id4"/>
<transition>
<source ref="id0"/>
<target ref="id5"/>
<label kind="guard" x="-2451" y="-1606">x==ACK_Time</label>
<nail x="-2523" y="-1582"/>
</transition>
<transition>
<source ref="id1"/>
<target ref="id2"/>
<label kind="guard" x="-2499" y="-1846">nretries == (MaxFrameRetries-1)</label>
<nail x="-2323" y="-1846"/>
</transition>
<transition>
<source ref="id1"/>
<target ref="id6"/>
<label kind="guard" x="-2515" y="-1886">nretries &lt; (MaxFrameRetries-1)</label>
<label kind="assignment" x="-2515" y="-1870">nretries = nretries + 1</label>
</transition>
<transition>
<source ref="id4"/>
<target ref="id6"/>
</transition>
<transition>
<source ref="id5"/>
<target ref="id1"/>
<label kind="guard" x="-2515" y="-1822">x==MinLIFS</label>
</transition>
<transition>
<source ref="id6"/>
<target ref="id17"/>
<label kind="assignment" x="-2515" y="-1982">be:=macMinBE, nb:=0</label>
</transition>
<transition>
<source ref="id15"/>
<target ref="id15"/>
<label kind="synchronisation" x="-2267" y="-2238">busy?</label>
<label kind="assignment" x="-2267" y="-2222">cca_passed:=false</label>
<nail x="-2267" y="-2198"/>
<nail x="-2179" y="-2198"/>
</transition>
<transition>
<source ref="id11"/>
<target ref="id8"/>
<label kind="guard" x="-2267" y="-1718">x==ACK</label>
<label kind="assignment" x="-2267" y="-1702">nt:=nt-1</label>
</transition>
<transition>
<source ref="id9"/>
<target ref="id2"/>
<label kind="guard" x="-2219" y="-1974">nb == MaxNB</label>
</transition>
<transition>
<source ref="id9"/>
<target ref="id17"/>
<label kind="guard" x="-2507" y="-2046">nb &lt; MaxNB</label>
<label kind="assignment" x="-2507" y="-2030">be:= (be+1 &gt; MaxBE ? MaxBE: be+1)</label>
</transition>
<transition>
<source ref="id11"/>
<target ref="id11"/>
<label kind="synchronisation" x="-2107" y="-1678">busy?</label>
<label kind="assignment" x="-2107" y="-1662">collision_occured:=true</label>
<nail x="-2147" y="-1638"/>
<nail x="-2099" y="-1638"/>
<nail x="-2115" y="-1662"/>
</transition>
<transition>
<source ref="id3"/>
<target ref="id12"/>
<label kind="guard" x="-2043" y="-1870">!collision_occured</label>
</transition>
<transition>
<source ref="id10"/>
<target ref="id0"/>
<label kind="guard" x="-2019" y="-1614">x == TurnAround</label>
<label kind="assignment" x="-2019" y="-1598">x:=0</label>
</transition>
<transition>
<source ref="id3"/>
<target ref="id10"/>
<label kind="guard" x="-1883" y="-1822">collision_occured</label>
<nail x="-1891" y="-1710"/>
</transition>
<transition>
<source ref="id13"/>
<target ref="id13"/>
<label kind="synchronisation" x="-1827" y="-2030">busy?</label>
<label kind="assignment" x="-1827" y="-2014">collision_occured:=true</label>
<nail x="-1835" y="-2038"/>
<nail x="-1835" y="-1966"/>
</transition>
<transition>
<source ref="id8"/>
<target ref="id7"/>
<label kind="guard" x="-2291" y="-1742">!collision_occured</label>
<nail x="-2299" y="-1718"/>
</transition>
<transition>
<source ref="id8"/>
<target ref="id5"/>
<label kind="guard" x="-2443" y="-1678">collision_occured</label>
<label kind="assignment" x="-2371" y="-1710">x:=0</label>
</transition>
<transition>
<source ref="id12"/>
<target ref="id11"/>
<label kind="guard" x="-2115" y="-1822">x==TurnAround</label>
<label kind="synchronisation" x="-2116" y="-1802">busy!</label>
<label kind="assignment" x="-2116" y="-1785">collision_occured:=(nt&gt;0)
nt:=nt+1
x:=0</label>
</transition>
<transition>
<source ref="id13"/>
<target ref="id3"/>
<label kind="guard" x="-1883" y="-1958">x==FrameLength</label>
<label kind="assignment" x="-1883" y="-1942">x:=0
nt:=nt-1</label>
</transition>
<transition>
<source ref="id14"/>
<target ref="id13"/>
<label kind="guard" x="-1883" y="-2118">x==TurnAround</label>
<label kind="synchronisation" x="-2147" y="-2166">busy!</label>
<label kind="assignment" x="-1883" y="-2102">x:=0,
collision_occured:=(nt&gt;0),
nt:=nt+1</label>
</transition>
<transition>
<source ref="id15"/>
<target ref="id14"/>
<label kind="guard" x="-2147" y="-2182">(x==CCA) &amp;&amp; (cca_passed)</label>
<label kind="assignment" x="-2147" y="-2150">x:=0</label>
</transition>
<transition>
<source ref="id15"/>
<target ref="id9"/>
<label kind="guard" x="-2227" y="-2094">(x == CCA_duration) &amp;&amp; !cca_passed</label>
<label kind="assignment" x="-2227" y="-2078">nb := nb+1</label>
</transition>
<transition>
<source ref="id16"/>
<target ref="id15"/>
<label kind="guard" x="-2475" y="-2190">(x==backoff*UnitBackoff)</label>
<label kind="assignment" x="-2475" y="-2174">cca_passed:=(nt==0),
x:=0</label>
</transition>
<transition>
<source ref="id17"/>
<target ref="id16"/>
<label kind="assignment" x="-2515" y="-2094">backoff := random(0..pow(2,be))
x:=0</label>
</transition>
</template>
<system>// Place template instantiations here.

system Process;</system>
<queries>
<query>
<formula></formula>
<comment></comment>
</query>
</queries>
</nta>
11 changes: 8 additions & 3 deletions CaseStudies/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# List of Case Studies

_**[Randomized Reachability Analysis in Uppaal: Fast Error Detection in Timed Systems](RandomizedReachability2021)**_, Kiviriga A., Larsen K.G., Nyman U. (2021). In: Lluch Lafuente A., Mavridou A. (eds) Formal Methods for Industrial Critical Systems. FMICS 2021. Lecture Notes in Computer Science, vol 12863. Springer, Cham. [[DOI]](https://doi.org/10.1007/978-3-030-85248-1_9) [[Springer]](https://link.springer.com/chapter/10.1007/978-3-030-85248-1_9)
_**[Randomized Reachability Analysis in Uppaal: Fast Error Detection in Timed Systems](RandomizedReachability2021)**_, Kiviriga A., Larsen K.G., Nyman U. (2021). In: Lluch Lafuente A., Mavridou A. (eds) Formal Methods for Industrial Critical Systems. FMICS 2021. Lecture Notes in Computer Science, vol 12863. Springer, Cham. [[DOI:10.1007/978-3-030-85248-1_9](https://doi.org/10.1007/978-3-030-85248-1_9)] [[Springer](https://link.springer.com/chapter/10.1007/978-3-030-85248-1_9)]

_**[Modeling and Analysis for Energy-Driven Computing using Statistical Model-Checking](EnergyNeutrality)**_,
Abdoulaye Gamatié, Gilles Sassatelli, Marius Mikučionis. *Design, Automation and Test in Europe (DATE 2021),* February 1, 2021.
Expand All @@ -9,11 +9,16 @@ _**[Fluid Model-Checking in UPPAAL for Covid-19](Covid-19)**_,
Peter G. Jensen, Kenneth Y. Jørgensen, Kim G. Larsen, Marius Mikučionis, Marco Muñiz, and Danny B. Poulsen. *Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies (ISoLA 2020),* October 2020. Springer-Verlag Berlin Heidelberg.

_**[Schedulability of Herschel-Planck Revisited Using Statistical Model Checking](HerschelPlanck2012)**_,
Alexandre David, Kim G. Larsen, Axel Legay and Marius Mikučionis. *Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies (ISoLA 2012)*, October 2012, Springer-Verlag Berlin Heidelberg. ISBN 978-3-642-34032-1, 978-3-642-34031-4. [[DOI](https://doi.org/10.1007/978-3-642-34032-1_28)]
Alexandre David, Kim G. Larsen, Axel Legay and Marius Mikučionis. *Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies (ISoLA 2012)*, October 2012, Springer-Verlag Berlin Heidelberg. ISBN 978-3-642-34032-1, 978-3-642-34031-4. [[DOI:10.1007/978-3-642-34032-1_28](https://doi.org/10.1007/978-3-642-34032-1_28)]

_**[Rewrite-Based Statistical Model Checking of WMTL](CSMA-CA-RV2012)**_,
Peter E. Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Guangyuan Li & Danny Bøgsted Poulsen. *Runtime Verification (RV 2012)*, 2012. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (LNCS). [[DOI:10.1007/978-3-642-35632-2_25](https://doi.org/10.1007/978-3-642-35632-2_25)]

_**[Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach](CSMA-CA-IWIGP2012)**_,
Peter E. Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikučionis. *2nd Internation Workshop on Interactions, Games and Protocols (IWIGP 2012)*, March 25, 2012, Electronic Proceedings in Theoretical Computer Science (EPTCS). [[DOI:10.4204/EPTCS.78.1](https://doi.org/10.4204/EPTCS.78.1)]

_**[Schedulability Analysis of Herschel/Planck Software Using Uppaal](HerschelPlanck2011)**_
Marius Mikučionis, Kim G. Larsen and Brian Nielsen. Quasimodo Industrial Handbook, 2011.

_**[Schedulability Analysis Using Uppaal: Herschel-Planck Case Study](HerschelPlanck2010)**_
Marius Mikučionis, Kim Guldstrand Larsen, Jacob Illum Rasmussen, Brian Nielsen, Arne Skou, Palm Steen Ulrik, Jan Storbank Pedersen, Poul Hougaard. _Proceedings of the 4th international conference on Leveraging applications of formal methods, verification, and validation (ISOLA 2010)_, October 2010, Springer-Verlag, ISBN 3-642-16560-5, 978-3-642-16560-3. [[DOI](https://doi.org/10.1007/978-3-642-16561-0_21)]
Marius Mikučionis, Kim Guldstrand Larsen, Jacob Illum Rasmussen, Brian Nielsen, Arne Skou, Palm Steen Ulrik, Jan Storbank Pedersen, Poul Hougaard. _Proceedings of the 4th international conference on Leveraging applications of formal methods, verification, and validation (ISOLA 2010)_, October 2010, Springer-Verlag, ISBN 3-642-16560-5, 978-3-642-16560-3. [[DOI:10.1007/978-3-642-16561-0_21](https://doi.org/10.1007/978-3-642-16561-0_21)]