Contracts for concurrency describe required atomicity of method sequences in concurrent programs. This work proposes a dynamic analyzer to verify programs written in Java against contracts for concurrency. The analyzer was designed to detect violations of parametric contracts with spoilers. The proposed analyzer was implemented as an extension to the RoadRunner framework. Support for accessing the method arguments and return values was added to RoadRunner as a part of the solution. The analyzer was fully implemented and verified on a set of testing programs.
| Identifer | oai:union.ndltd.org:nusl.cz/oai:invenio.nusl.cz:445489 |
| Date | January 2021 |
| Creators | Žárský, Jan |
| Contributors | Křena, Bohuslav, Smrčka, Aleš |
| Publisher | Vysoké učení technické v Brně. Fakulta informačních technologií |
| Source Sets | Czech ETDs |
| Language | Czech |
| Detected Language | English |
| Type | info:eu-repo/semantics/masterThesis |
| Rights | info:eu-repo/semantics/restrictedAccess |
Page generated in 0.0467 seconds