If you're interested you can read the full paper here: The full paper
Abstract
Personal computing devices and servers are becoming more powerful by the day through hardware parallelisation. Such advances require developers to look into concurrency in order to
take advantage of the new computing power. However, much of the code is written without
formal verification and checked only heuristically through unit or other tests. This dissertation
will show how Communicating Sequential Processes (CSP) can be used to detect errors in an
application that supports concurrent execution. This is done by isolating common concurrency
problems and mapping them into CSP representations. Finally, Failures-Divergences Refinement (FDR) software package is used to perform refinement checks to detect the errors in the
source code. This process allows the developer to build assertions that their code must pass to
prove its correctness.
Acknowledgements
I would like to thank my advisor, Dr. Andrew Simpson, and the Software Engineering Program staff for their guidance and quick responses. This project could not have been accomplished without the generosity, patience and accommodation of the family scholarship fund. I am particularly grateful to the American people for providing the opportunity and the Lithuanian people for their infinitely delicious food and heavenly honey. Finally, I wish to thank my wife, Diana, for her love, support and conversation.
I would like to thank my advisor, Dr. Andrew Simpson, and the Software Engineering Program staff for their guidance and quick responses. This project could not have been accomplished without the generosity, patience and accommodation of the family scholarship fund. I am particularly grateful to the American people for providing the opportunity and the Lithuanian people for their infinitely delicious food and heavenly honey. Finally, I wish to thank my wife, Diana, for her love, support and conversation.
Nice work!
ReplyDelete