In two-phase testing of multi-threaded software (e.g., Ada tasking programs or multi-threaded Java programs), we combine scalable state-space analysis techniques with dynamic testing. The state-space analysis techniques provide strong assurances of certain critical properties, like freedom from deadlock, but they do not "scale up" when applied directly to source code or implementation-level design structures. Instead, these strong techniques are applied in a hierarchical, modular manner to a well-structured architectural model, and dynamic testing is used to validate the "as built" implementation structure against the verified architectural model.
Together, testing and analysis contribute to an indirect argument about the desired properties of the software. The complex relation between layered architectural structures and implementation structures is the source of a set of analysis and testing obligations. The combination can be more sensitive to subtle, timing dependent errors than directly testing for the properties of interest. [More]
Contact: Michal
Young