Title :
On the Numerical Verification of Probabilistic Rewriting Systems
Author :
Jounaidi Ben Hassen ; Tahar, Sofiène
Author_Institution :
Dept. of Electr. & Comput. Eng., Concordia Univ., Montreal, Que.
Abstract :
We present in this paper a technique for the formal verification of probabilistic systems described in PMaude, a probabilistic extension of the rewriting system Maude. Our methodology is based on a numerical verification using the probabilistic symbolic model checking tool PRISM. In particular, we show how we can construct an abstract system from the runs of a model that preserve all the probabilistic properties of the latter. Then we deduce the probabilistic matrix that will be used for the verification in PRISM
Keywords :
electronic engineering computing; formal logic; formal specification; formal verification; logic testing; rewriting systems; symbol manipulation; Maude rewriting system; PMaude; PRISM; numerical verification; probabilistic matrix; probabilistic rewriting system; probabilistic symbolic model checking tool; Computational modeling; Equations; Formal verification; Labeling; Probabilistic logic; Real time systems; Stochastic processes; Stochastic systems; Testing;
Conference_Titel :
Design, Automation and Test in Europe, 2006. DATE '06. Proceedings
Conference_Location :
Munich
Print_ISBN :
3-9810801-1-4
DOI :
10.1109/DATE.2006.244073
