Verification of random behaviours

S. Andova; T.A.C. Willemse

Verification of random behaviours

S. Andova, T.A.C. Willemse

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Abstract

We introduce abstraction in a probabilistic process algebra. The process algebra can be employed for specifying processes that exhibit both probabilistic and non-deterministic choices in their behaviours. Several rules and axioms are identified, allowing us to rewrite processes to less complex processes by removing redundant internal activity. Using these rules, we have successfully conducted a verification of the Concurrent Alternating Bit Protocol. The verification shows that after abstraction of internal activity, the protocol behaves as a buffer.

Original language	English
Title of host publication	SEEFM 200: First south-east europian workshop on formal methods
Editors	Y. Manolopoulos, P. Spirakis
Place of Publication	Thessaloniki, Greece
Publisher	Aristotle University of Thessaloniki
Pages	84-99
Number of pages	16
Publication status	Published - 20 Nov 2003
Event	1st South-East Europian Workshop on Formal Methods, SEEFM 2003 - Thessaloniki, Greece Duration: 20 Nov 2003 → 20 Nov 2003 Conference number: 1

Conference

Conference	1st South-East Europian Workshop on Formal Methods, SEEFM 2003
Country/Territory	Greece
City	Thessaloniki
Period	20/11/03 → 20/11/03

Access to Document

Andova2003verificationFinal published version, 234 KB

Cite this

@inproceedings{ff9d25e9c7c240c280e86f2c9f9f753d,

title = "Verification of random behaviours",

abstract = "We introduce abstraction in a probabilistic process algebra. The process algebra can be employed for specifying processes that exhibit both probabilistic and non-deterministic choices in their behaviours. Several rules and axioms are identified, allowing us to rewrite processes to less complex processes by removing redundant internal activity. Using these rules, we have successfully conducted a verification of the Concurrent Alternating Bit Protocol. The verification shows that after abstraction of internal activity, the protocol behaves as a buffer.",

author = "S. Andova and T.A.C. Willemse",

year = "2003",

month = nov,

day = "20",

language = "English",

pages = "84--99",

editor = "Y. Manolopoulos and P. Spirakis",

booktitle = "SEEFM 200: First south-east europian workshop on formal methods",

publisher = "Aristotle University of Thessaloniki",

note = "1st South-East Europian Workshop on Formal Methods, SEEFM 2003 ; Conference date: 20-11-2003 Through 20-11-2003",

}

TY - GEN

T1 - Verification of random behaviours

AU - Andova, S.

AU - Willemse, T.A.C.

N1 - Conference code: 1

PY - 2003/11/20

Y1 - 2003/11/20

N2 - We introduce abstraction in a probabilistic process algebra. The process algebra can be employed for specifying processes that exhibit both probabilistic and non-deterministic choices in their behaviours. Several rules and axioms are identified, allowing us to rewrite processes to less complex processes by removing redundant internal activity. Using these rules, we have successfully conducted a verification of the Concurrent Alternating Bit Protocol. The verification shows that after abstraction of internal activity, the protocol behaves as a buffer.

AB - We introduce abstraction in a probabilistic process algebra. The process algebra can be employed for specifying processes that exhibit both probabilistic and non-deterministic choices in their behaviours. Several rules and axioms are identified, allowing us to rewrite processes to less complex processes by removing redundant internal activity. Using these rules, we have successfully conducted a verification of the Concurrent Alternating Bit Protocol. The verification shows that after abstraction of internal activity, the protocol behaves as a buffer.

M3 - Conference contribution

SP - 84

EP - 99

BT - SEEFM 200: First south-east europian workshop on formal methods

A2 - Manolopoulos, Y.

A2 - Spirakis, P.

PB - Aristotle University of Thessaloniki

CY - Thessaloniki, Greece

T2 - 1st South-East Europian Workshop on Formal Methods, SEEFM 2003

Y2 - 20 November 2003 through 20 November 2003

ER -

Verification of random behaviours

Abstract

Conference

Access to Document

Fingerprint

Cite this