TR00-01 (2000) – Concurent Composition, Refinement, and Fairness in CafeOBJ

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.

Bibtex

@TechReport{abp,
  author = 	 {D. Lucanu and S. Iida  and R. Diaconescu},
  title = 	 {Concurrent Composition, Refinement, and Fairness in
{{sf Cafeobj}},
                  A Case Study: Alternating Bit Protocol},
  institution =  {University ``A.I.Cuza'' of Iac{s}i, Faculty of
Computer Science},
  year = 	 {2000},
  number = 	 {TR 00-01},
  note = 	 {URL:http://www.infoiasi.ro/~tr/tr.pl.cgi}
}