A hierarchy of failures-based models: theory and application

AbstractConsistency between a process and its specification expressed in CSP is typically presented as a refinement check. Within the traces model consistency is measured by examining only the traces of the systems, whilst in the finer stable failures model the possibility of subsequently refusing a combination of events is also taken into consideration.In this paper, we begin by motivating the need for alternative measures of consistency. We then identify the failures class—a class of semantic models for describing concurrent systems in which each model is associated with a predicate that determines how much availability information is recorded. We show how refinement within members of this class corresponds to confirmation of non-standard measures of consistency, and identify application areas for these measures of consistency. We show how refinement in each model can be automatically tested.We also carry out a theoretical examination of the failures class. We prove that the class forms a complete lattice, and investigate the positions of particular models within that lattice. We also identify the maximal subset of the language over which each model is compositional