| Riassunto: | <p>Consistency 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.</p> <p>In this paper, we begin by motivating the need for alternative measures of consistency. We then identify the <em>failures class</em>—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.</p> <p>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.</p>
|
|---|