Abstract:
Advancements in networking and wireless technologies have led to increased demand of complex, interactive software systems. Typical applications consist of several cooperating processes, many of which are multithreaded. The possibility of subtle interactions between threads and between processes leads to significant challenges in the design, implementation, and testing of such systems. Currently, formal verification and validation methods provide a high degree of confidence of the correctness and reliability of software systems. Model checking, a state-space exploration methodology, is usually applied at the design phase of the software life cycle to verify that preliminary high-level design specifications conform to their requirements. Source code (program) analysis, on the other hand, is used to check for correctness of implementation once it is realized from the design specifications. The current practice of validating a design and its implementation in isolation makes it necessary to employ rigorous testing analysis to empirically ensure that the implementation satisfies the design specification.
The principal investigators (PIs) claim that tighter integration of the design and implementation phase of the software development process is necessary to bridge the inherent gap between specification and its corresponding implementation. The PIs propose to achieve this via a formal framework that allows design models to contain embedded partial implementations as components; these models are then formally analyzed to ensure that global requirements are satisfied. The framework, therefore, provides flexibility to incrementally develop and ensure correctness of the design and the corresponding implementation. Realization of the above objective requires consolidation and expansion of traditional formal verification techniques by bringing together the power of model checking, program analysis and constraint solving.