Concurrent program analysis for state space generation and complexity evaluation

We address two different dimensions for the analysis of concurrent programs.;The first dimension for program analysis is the generation and evaluation of the state space for some program model. Because these state spaces tend to grow very large very fast, it is important to limit the types of program events that are preserved by the program model and hence become explicit in the model's state space. We suggest that concurrency analysis for Ada can be effectively performed by using a program model that directly preserves only the task interaction constructs; control flow events are indirectly modeled and need not become explicit in the state space. Two existing models of Ada tasking are evaluated in this context and associated problems are discussed. Two new task-interaction preserving models are defined and shown to be comparatively more effective for state space analysis.;The second dimension for program analysis is the study of the communication complexity of a program. We note that nondeterminism is a key contributing factor to concurrent-software complexity. We discuss language constructs contributing to nondeterminism in Ada and derive some complexity measures based on these programming constructs. We subject these measures to both theoretical and empirical evaluations and discuss the results.