Dynamic analysis of java applications for multithreaded antipatterns
Sergiy Boroday, Alexandre Petrenko, J. Singh, Hesham H. Hallal · ACM SIGSOFT Software Engineering Notes · 2005
Formal verification is not always applicable to large industrial software systems due to scalability issues and difficulties in formal model and requirements specification. The scalability and model derivation problems could be alleviated by runtime trace analysis, which combines both testing and formal verification. We implement and compare an ad-hoc custom approach and a formal approach to detect common bug patterns in multithreaded Java software. We use the tracing platform of the Eclipse IDE and state-of-the-art model checker Spin.