Name
Abstract | ||
|---|---|---|
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.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. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1016/j.tcs.2004.10.004 | Theor. Comput. Sci. |
Keywords | DocType | Volume |
failures class,complete lattice,traces model consistency,refinement check,finer stable failures model,alternative measure,class corresponds,semantic model,particular model,failures class-a class,failures-based model | Journal | 330 |
Issue | ISSN | Citations |
3 | Theoretical Computer Science | 5 |
PageRank | References | Authors |
0.46 | 10 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christie Bolton | 1 | 132 | 9.27 |
| Gavin Lowe | 2 | 2389 | 175.16 |