Name
Abstract | ||
|---|---|---|
Nondeterminism is an inevitable constituent of any theory that describes concurrency. For the validation and verification of concurrent systems, it is essential to investigate the presence or absence of nondeterminism, just as much as deadlock or livelock. CSP is a well established process algebra; the main tool for practical use of CSP, the model checker FDR, checks determinism using a global analysis. We propose a local analysis, in order to improve performance and scalability. Our strategy is to use a compositional approach where we start from basic deterministic processes and check whether any of the composition operators introduce nondeterminism. We present the algorithms used in our strategy and experiments that show the efficiency of our approach. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1007/978-3-319-70848-5_8 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
Model checking,FDR,Performance,Experiments | Programming language,Model checking,Verification and validation,Computer science,Concurrency,Determinism,Deadlock,Theoretical computer science,Operator (computer programming),Process calculus,Scalability | Conference |
Volume | ISSN | Citations |
10623 | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 7 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Rodrigo Otoni | 1 | 0 | 0.34 |
| Ana Cavalcanti | 2 | 224 | 18.41 |
| Augusto Sampaio | 3 | 501 | 43.38 |