Dorel Lucanu, Shusaku Iida, Razvan Diaconescu

The paper exhibit the power of the Cafeobj system to handle concurrency, synchronization, nondeterminism, and communication in specification of complex systems. A simple and efficient method to handle the fairness assumption in proofs is shown.

Full Document (PS)

Bibtex

@TechReport{abp,
    author = 	{Dorel Lucanu and Shusaku Iida and Razvan Diaconescu},
    title = 	{Concurrent Composition, Refinement, and Fairness in {{sf Cafeobj}}, A Case Study: Alternating Bit Protocol},
    institution = {University ``A.I.Cuza'' of Iasi, Faculty of Computer Science},
    year = 	{2000},
    number = 	{TR 00-01},
    url = 	{https://publications.info.uaic.ro/technical-reports/archive/tr00-01-2000-concurent-composition-refinement-and-fairness-in-cafeobj/}
}