Warning: Trying to access array offset on value of type bool in /data/www/freeminded.org/www/wp-content/plugins/wp-latex/wp-latex.php on line 39 Tag » modelchecking « @ Freeminded.org Warning: Trying to access array offset on value of type bool in /data/www/freeminded.org/www/wp-content/plugins/wp-latex/wp-latex.php on line 46

Posts Tagged modelchecking

Matlab: increasing precision

Posted by on Wednesday, 19 October, 2011

Sometimes Matlab does not always perform as expected. This can be because of the IEEE 754 binary double precision floating point (double) representation used by Matlab: there is a finite number of digits to represent a number and this may not always be enough. We discuss how to use the Symbolic Toolkit to circumvent this. Read the rest of this entry »

Using PRISM – a probabilistic symbolic modelchecker

Posted by on Tuesday, 14 June, 2011

There are IEEE standards. There are implementations in hard- and software. There are implementations in software meant for simulation – and then there are models built to validate them. I’ll list some peculiarities of the PRISM modelchecker, as I started using it with only Java / C / C++ / php experience. The syntax is sometimes slightly obscure. Read the rest of this entry »

Wrong duration of SlotTime in IEEE 802.11p in NS-2 / NS-3

Posted by on Wednesday, 20 April, 2011

IEEE 802.11p is designed for use in the V2V / V2I context. It uses an OFDM physical layer largely based on IEEE 802.11a. Some values are directly reused, others are modified. The slottime (often denoted with the Greek ‘sigma’ or aSlotTime) is one of those values which are unclear.

As a result, NS-2 and NS-3 erroneously use a wrong 802.11p slotTime of 13 microseconds. Scientific works using these simulators should carefully check sensitivity to this bug – results may be off!
Read the rest of this entry »

A Markov Chain in TiKz

Posted by on Monday, 17 May, 2010

When you want to draw a Markov Chain (or any other graph-theoretical structure) you can toil around with various drawing programs, or you can simply turn to PGF/TiKz, the LaTeX drawing environment. Since true scientists publish their work in LaTeX, this immediately eases the work required for your next paper. Read the rest of this entry »