A Comparison of Simulation Techniques and Algebraic Techniques for Verifying Concurrent Systems
Simulation-based assertional techniques and process algebraic techniques are two of the major methods that have been proposed for the verification of concurrent and distributed systems. It is shown how each of these techniques can be applied to the task of verifying systems described as input/output...
| Main Authors: | , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149218 |
| _version_ | 1811081882178158592 |
|---|---|
| author | Lynch, Nancy A. Segala, Roberto |
| author_facet | Lynch, Nancy A. Segala, Roberto |
| author_sort | Lynch, Nancy A. |
| collection | MIT |
| description | Simulation-based assertional techniques and process algebraic techniques are two of the major methods that have been proposed for the verification of concurrent and distributed systems. It is shown how each of these techniques can be applied to the task of verifying systems described as input/output automata; both of these ways, first using forward simulations, an execution correspondence lemma, and a simple fairness argument, and second using deductions within the process algebra DIOA for I/O automata. An extended evaluation and comparison of the two methods is given. |
| first_indexed | 2024-09-23T11:53:53Z |
| id | mit-1721.1/149218 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T11:53:53Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1492182023-03-30T03:48:33Z A Comparison of Simulation Techniques and Algebraic Techniques for Verifying Concurrent Systems Lynch, Nancy A. Segala, Roberto Simulation-based assertional techniques and process algebraic techniques are two of the major methods that have been proposed for the verification of concurrent and distributed systems. It is shown how each of these techniques can be applied to the task of verifying systems described as input/output automata; both of these ways, first using forward simulations, an execution correspondence lemma, and a simple fairness argument, and second using deductions within the process algebra DIOA for I/O automata. An extended evaluation and comparison of the two methods is given. 2023-03-29T14:37:28Z 2023-03-29T14:37:28Z 1993-11 https://hdl.handle.net/1721.1/149218 MIT-LCS-TM-499 application/pdf |
| spellingShingle | Lynch, Nancy A. Segala, Roberto A Comparison of Simulation Techniques and Algebraic Techniques for Verifying Concurrent Systems |
| title | A Comparison of Simulation Techniques and Algebraic Techniques for Verifying Concurrent Systems |
| title_full | A Comparison of Simulation Techniques and Algebraic Techniques for Verifying Concurrent Systems |
| title_fullStr | A Comparison of Simulation Techniques and Algebraic Techniques for Verifying Concurrent Systems |
| title_full_unstemmed | A Comparison of Simulation Techniques and Algebraic Techniques for Verifying Concurrent Systems |
| title_short | A Comparison of Simulation Techniques and Algebraic Techniques for Verifying Concurrent Systems |
| title_sort | comparison of simulation techniques and algebraic techniques for verifying concurrent systems |
| url | https://hdl.handle.net/1721.1/149218 |
| work_keys_str_mv | AT lynchnancya acomparisonofsimulationtechniquesandalgebraictechniquesforverifyingconcurrentsystems AT segalaroberto acomparisonofsimulationtechniquesandalgebraictechniquesforverifyingconcurrentsystems AT lynchnancya comparisonofsimulationtechniquesandalgebraictechniquesforverifyingconcurrentsystems AT segalaroberto comparisonofsimulationtechniquesandalgebraictechniquesforverifyingconcurrentsystems |