Correct behavior of programs can be defined by their temporal properties. One of the options for formal specification of such properties is linear temporal logic - LTL . This master's thesis describes design and implementation of a tool for automatic checking of temporal properties of programs, that are specified using Past-Time LTL formulae. The trace of a given program is analyzed in run-time and any violation of given formulae is reported in details to help to find the code location with a root cause of the bug.
Identifer | oai:union.ndltd.org:nusl.cz/oai:invenio.nusl.cz:403176 |
Date | January 2019 |
Creators | Sečkařová, Petra |
Contributors | Češka, Milan, 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.0016 seconds