s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
3593 Commits
5 Branches
0 Tags
31 MiB
 
 
 
 
 
 
Branch: master
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'master'
${ noResults }
prism-accumulation/prism-examples/csma
Dave Parker a00471be4b
Added txt extension to README files. 		15 years ago
..
.autopp Re-tidy csma. 17 years ago
.csmaN_K.nm.pp Fix(es) for previous commit. 17 years ago
README.txt Added txt extension to README files. 15 years ago
auto auto file tweak. 17 years ago
csma.pctl Fix(es) for previous commit. 17 years ago
csma2_2.nm Fix(es) for previous commit. 17 years ago
csma2_4.nm Fix(es) for previous commit. 17 years ago
csma2_6.nm Fix(es) for previous commit. 17 years ago
csma3_2.nm Fix(es) for previous commit. 17 years ago
csma3_4.nm Fix(es) for previous commit. 17 years ago
csma3_6.nm Fix(es) for previous commit. 17 years ago
csma4_2.nm Re-tidy csma. 17 years ago
csma4_4.nm Re-tidy csma. 17 years ago
csma4_6.nm Re-tidy csma. 17 years ago

README.txt 

This case study concerns the IEEE 802.3 CSMA/CD (Carrier Sense, Multiple Access with Collision Detection) protocol


model files csmaN_K.nm
property file: csma.pctl

where N is the number of stations and K is the maximum backoff


For more information on the probabilistic timed automata see: http://www.prismmodelchecker.org/casestudies/csma.php

The PRISM model uses the integer semantics given in [KNPS06].

=====================================================================================

[KNPS06]
M. Kwiatkowska, G. Norman, D. Parker and J. Sproston
Performance Analysis of Probabilistic Timed Automata using Digital Clocks
Formal Methods in System Design, 29:33-78, 2006