Change search
ReferencesLink to record
Permanent link

Direct link
Test-inspired runtime verification: Using a unit test-like specification syntax for runtime verification
KTH, School of Computer Science and Communication (CSC).
2014 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

Computer software is growing ever more complex, and more sophisticated tools are required to make sure the software operates in a correct way — i.e. according to its specification. There are two general approaches to assure the correctness of software. While formal methods can give useful mathematical proofs about the correctness of programs,they suffer from complexity and are difficult to use. Often they work only on a constructed system model, not the actual program. Testing, on the other hand, has a simple syntax and great tool support, and it is in widespread use. It is however informal and incomplete, only testing the specific test cases that the test-writers can come up with. A relatively new approach called runtime verification is an attempt for a lightweight alternative. It verifies a program’s actual execution against its specification, possibly while the program is running. This work investigates how testing, and specifically unit testing, can be combined with runtime verification. It shows how the syntax ofunit tests, written in the target program’s programming language, can be used to inspire the syntax for specifications for runtime verification. Both informal and formal specifications are described and supported. A proof-of-concept framework for Python called pythonrv is implemented and described, and it is tested on a real-life application. A formal foundation is constructed for specifications written in a subset of Python, enabling formal verification. Informal specifications are also supported, with the full power of Python as specification language. The result shows that the proof-of-concept framework allow for effective use of runtime verification. It is easy to integrate into existing programs, and the informal specification syntax is relatively simple. It also shows that formal specifications can be written in Python, but in a more unwieldy syntax and structure than the informal one. Many interesting properties can be verified using it that ordinary tests would have trouble with. The recommendation for future work lies in improving the specification syntax, using unit testing concepts such as expectations, and on working to make the formal specification syntax more like that of its informal sibling.

Place, publisher, year, edition, pages
National Category
Computer Science
URN: urn:nbn:se:kth:diva-153674OAI: diva2:753247
Available from: 2014-11-21 Created: 2014-10-07 Last updated: 2014-11-21Bibliographically approved

Open Access in DiVA

fulltext(715 kB)53 downloads
File information
File name FULLTEXT01.pdfFile size 715 kBChecksum SHA-512
Type fulltextMimetype application/pdf

By organisation
School of Computer Science and Communication (CSC)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 53 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 68 hits
ReferencesLink to record
Permanent link

Direct link