Automated formal analysis methods for concurrent and real-time software

As the use of concurrent and concurrent real-time software systems in safety-critical applications becomes widespread, the verification of their correctness has become an important concern. Unfortunately, analysis of these systems has been stymied by the explosive number of states they possess. The constrained expression approach, which uses an inequality-based technique to avoid the enumeration of these states, showed promise for analyzing large systems, but was incapable of verifying many important properties of interest to designers. For example, properties involving the order of the events in a concurrent system (e.g., mutual exclusion) could not be verified since the inequalities did not capture this information, nor could the technique verify liveness properties, since these require reasoning about infinite executions. I have developed extensions to this inequality-based technique that allow the verification of these more complex properties. In addition, I have completely automated an earlier extension of this technique for deriving bounds in concurrent real-time systems run on a uniprocessor and I have extended this technique to the maximally-parallel multiprocessor setting. Most importantly, I have demonstrated the feasibility of these extensions by implementing them in an automated tool and using this tool to analyze several sample systems