Counter Abstraction in the CSP/FDR setting
In this paper we consider an adaptation of counter abstraction for the CSP/FDR setting. The technique allows us to transform a concurrent system with an unbounded number of agents into a finite-state abstraction. The systems to which the method can be applied are composed of many identical node proc...
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Published: |
2007
|
| _version_ | 1797104877182124032 |
|---|---|
| author | Mazur, T Lowe, G |
| author_facet | Mazur, T Lowe, G |
| author_sort | Mazur, T |
| collection | OXFORD |
| description | In this paper we consider an adaptation of counter abstraction for the CSP/FDR setting. The technique allows us to transform a concurrent system with an unbounded number of agents into a finite-state abstraction. The systems to which the method can be applied are composed of many identical node processes that run in parallel with a controller process. Refinement checks on the abstract state machine can be performed automatically in the traces and stable failures models using the model checker FDR. We illustrate the method on an example based on a multiprocessor operating system. |
| first_indexed | 2024-03-07T06:39:40Z |
| format | Conference item |
| id | oxford-uuid:f8d415d2-8c40-46d2-8bc9-287053a6b3eb |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:39:40Z |
| publishDate | 2007 |
| record_format | dspace |
| spelling | oxford-uuid:f8d415d2-8c40-46d2-8bc9-287053a6b3eb2022-03-27T12:53:31ZCounter Abstraction in the CSP/FDR settingConference itemhttp://purl.org/coar/resource_type/c_5794uuid:f8d415d2-8c40-46d2-8bc9-287053a6b3ebDepartment of Computer Science2007Mazur, TLowe, GIn this paper we consider an adaptation of counter abstraction for the CSP/FDR setting. The technique allows us to transform a concurrent system with an unbounded number of agents into a finite-state abstraction. The systems to which the method can be applied are composed of many identical node processes that run in parallel with a controller process. Refinement checks on the abstract state machine can be performed automatically in the traces and stable failures models using the model checker FDR. We illustrate the method on an example based on a multiprocessor operating system. |
| spellingShingle | Mazur, T Lowe, G Counter Abstraction in the CSP/FDR setting |
| title | Counter Abstraction in the CSP/FDR setting |
| title_full | Counter Abstraction in the CSP/FDR setting |
| title_fullStr | Counter Abstraction in the CSP/FDR setting |
| title_full_unstemmed | Counter Abstraction in the CSP/FDR setting |
| title_short | Counter Abstraction in the CSP/FDR setting |
| title_sort | counter abstraction in the csp fdr setting |
| work_keys_str_mv | AT mazurt counterabstractioninthecspfdrsetting AT loweg counterabstractioninthecspfdrsetting |