RIA: Automated Support for Verification of Concurrent and Real-Time Software

点击翻译按钮获取中文摘要

The goal of this research is to increase the safety and reliability of real-world software systems. The research is directed toward the development of practical techniques and the construction of automated tools for verifying properties of concurrent and real-time software. Many techniques have been proposed for this task, but little is known about their performance and range of applicability in practice. This research will conduct a thorough empirical evaluation of two promising techniques and a new technique that is a hybrid of the two. The techniques will be evaluated by constructing tools that automate them and applying these tools to a large number of sample systems. The information obtained will provide insights into the strengths and weaknesses of the techniques examined and will help developers choose an appropriate technique for their particular domain.