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.

Volume

1

fYear

2006

fDate

6-10 March 2006

Firstpage

1

Lastpage

2

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Design, Automation and Test in Europe, 2006. DATE '06. Proceedings

Conference_Location

Munich

Print_ISBN

3-9810801-1-4

Type

conf

DOI

10.1109/DATE.2006.244073

Filename

1657080