Bachelor work
Executable code
Executable file
Presentation
Saint-Petersburg State University of Information Technologies, Mechanics and Optics
Bachelor work
Executable code
Executable file
Presentation
The project purpose is to verify automata programs model provided by instrumental tool UniMod. This tool generates XML-file and verifier constructs model for verification using only this file. Requirements are written using Linear Time Logic (LTL).
Main verifier's feature is specialization on automata programs model. So model transformation is unnecessary and verifier checks claims about automata program directly. Concurrent double DFS algorithm was implemented in this work, thus verifier was optimized to execute on multi-core systems.