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)


  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:}