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

30 Downloads (Pure)

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	Proceedings 1st South-East European Workshop on Formal Methods (SEEFM 2003, Thessaloniki, Greece, November 20, 2003), included in Proceedings 1st Balkan Conference in Informatics
Editors	Y. Manolopoulos, P. Spirakis
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

Keywords

Process algebra
Probabilistic systems
Verification
Abstraction

Access to Document

ArticleFinal 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.",

keywords = "Process algebra, Probabilistic systems, Verification, Abstraction",

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 = "Proceedings 1st South-East European Workshop on Formal Methods (SEEFM 2003, Thessaloniki, Greece, November 20, 2003), included in Proceedings 1st Balkan Conference in Informatics",

publisher = "Aristotle University of Thessaloniki",

address = "Greece",

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

}

Andova, S & Willemse, TAC 2003, Verification of random behaviours. in Y Manolopoulos & P Spirakis (eds), Proceedings 1st South-East European Workshop on Formal Methods (SEEFM 2003, Thessaloniki, Greece, November 20, 2003), included in Proceedings 1st Balkan Conference in Informatics. Aristotle University of Thessaloniki, pp. 84-99, 1st South-East Europian Workshop on Formal Methods, SEEFM 2003, Thessaloniki, Greece, 20/11/03.

Verification of random behaviours. / Andova, S.; Willemse, T.A.C.
Proceedings 1st South-East European Workshop on Formal Methods (SEEFM 2003, Thessaloniki, Greece, November 20, 2003), included in Proceedings 1st Balkan Conference in Informatics. ed. / Y. Manolopoulos; P. Spirakis. Aristotle University of Thessaloniki, 2003. p. 84-99.

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

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.

KW - Process algebra

KW - Probabilistic systems

KW - Verification

KW - Abstraction

M3 - Conference contribution

SP - 84

EP - 99

BT - Proceedings 1st South-East European Workshop on Formal Methods (SEEFM 2003, Thessaloniki, Greece, November 20, 2003), included in Proceedings 1st Balkan Conference in Informatics

A2 - Manolopoulos, Y.

A2 - Spirakis, P.

PB - Aristotle University of Thessaloniki

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

Keywords

Access to Document

Fingerprint

Cite this