@inbook {IOPORT.00140260, author = {Wu, Cheng and Bochmann, Gregor v.}, title = {Fairness in LOTOS.}, year = {1992}, booktitle = {Formal description techniques, IV. Proceedings of the IFIP TC6/WG6.1 4th international conference on formal description techniques for distributed systems and communication protocols, FORTE '91, Sydney, Australia, 19-22 November 1991}, isbn = {0-444-89402-0}, pages = {543-558}, publisher = {Amsterdam etc.: Elsevier Science Publishers B. V. (North-Holland)}, abstract = {Summary: [For the entire collection see Zbl 0747.00044.] Fairness is an important concept related to specification languages that are based on concurrent and nondeterministic computation models; it is related to liveness. We formally introduce fairness into the LOTOS specification language by employing the standard LOTOS semantics together with a formalism which states restrictions on fair infinite execution sequences. We extend three fairness concepts of CSP, namely process, guard and channel fairness, to LOTOS. Certain features of LOTOS, such as the dynamic creation of processes, the dynamic relation between gates and processes, and related membership in multi-way rendezvous, not present in CSP, make the definition of fairness difficult. We introduce the concept of ``transition groups'', which leads to a general notion of fairness, and use LOTOS action indexes to define the concepts of process, alternative and channel for LOTOS. We explain how a fair execution model for LOTOS can be obtained, and demonstrate the use of these concepts by showing how fairness assumptions can be used to prove liveness properties for a given LOTOS specification.}, identifier = {00140260}, }