| Popis: |
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. |
