Verification of random behaviours

S. Andova, T.A.C. Willemse

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

30 Downloads (Pure)


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.
Originele taal-2Engels
TitelProceedings 1st South-East European Workshop on Formal Methods (SEEFM 2003, Thessaloniki, Greece, November 20, 2003), included in Proceedings 1st Balkan Conference in Informatics
StatusGepubliceerd - 2003


Duik in de onderzoeksthema's van 'Verification of random behaviours'. Samen vormen ze een unieke vingerafdruk.

Citeer dit