An Abstraction Technique for Verifying Shared-Memory Concurrency
| Autor: | Dilian Gurov, Marieke Huisman, Wytse Oortwijn |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Leader election
Computer science Process calculus Concurrency Concurrency verification Program logics Process algebra Code verification Abstraction 02 engineering and technology computer.software_genre lcsh:Technology lcsh:Chemistry 0202 electrical engineering electronic engineering information engineering General Materials Science lcsh:QH301-705.5 Instrumentation Protocol (object-oriented programming) Abstraction (linguistics) Fluid Flow and Transfer Processes lcsh:T business.industry Programming language Process Chemistry and Technology General Engineering 020207 software engineering Usability Modular design lcsh:QC1-999 Computer Science Applications lcsh:Biology (General) lcsh:QD1-999 Shared memory lcsh:TA1-2040 020201 artificial intelligence & image processing lcsh:Engineering (General). Civil engineering (General) business computer lcsh:Physics |
| Zdroj: | Applied Sciences Volume 10 Issue 11 Applied Sciences, 10 (11) Applied Sciences, Vol 10, Iss 3928, p 3928 (2020) |
| ISSN: | 2076-3417 |
| Popis: | Modern concurrent and distributed software is highly complex. Techniques to reason about the correct behaviour of such software are essential to ensure its reliability. To be able to reason about realistic programs, these techniques must be modular and compositional as well as practical by being supported by automated tools. However, many existing approaches for concurrency verification are theoretical and focus primarily on expressivity and generality. This paper contributes a technique for verifying behavioural properties of concurrent and distributed programs that balances expressivity and usability. The key idea of the approach is that program behaviour is abstractly modelled using process algebra, and analysed separately. The main difficulty is presented by the typical abstraction gap between program implementations and their models. Our approach bridges this gap by providing a deductive technique for formally linking programs with their process-algebraic models. Our verification technique is modular and compositional, is proven sound with Coq, and has been implemented in the automated concurrency verifier VerCors. Moreover, our technique is demonstrated on multiple case studies, including the verification of a leader election protocol. Applied Sciences, 10 (11) ISSN:2076-3417 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|