Journal article
Counter abstraction in the CSP/FDR setting
- Abstract:
-
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 FDR model checker. We illustrate the method on an example based on a multiprocessor operating system.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Version of record, pdf, 334.1KB, Terms of use)
-
- Publisher copy:
- 10.1016/j.entcs.2009.08.012
Authors
- Publisher:
- Elsevier
- Journal:
- Electronic Notes in Theoretical Computer Science More from this journal
- Volume:
- 250
- Issue:
- 1
- Pages:
- 171–186
- Publication date:
- 2009-09-01
- Edition:
- Publisher's version
- DOI:
- ISSN:
-
1571-0661
- Language:
-
English
- Keywords:
- Subjects:
- UUID:
-
uuid:05a7172f-d055-4ea6-8baf-0c8d70068b8d
- Local pid:
-
ora:9754
- Deposit date:
-
2015-01-15
- ARK identifier:
Terms of use
- Copyright holder:
- Elsevier BV
- Copyright date:
- 2009
- Notes:
- © 2009 Elsevier B.V. Open access under CC BY-NC-ND license.
If you are the owner of this record, you can report an update to it here: Report update to this record