CSR--SMA: Software Verification Using Plug and Play Components

网络和无线技术的进步导致了对复杂的交互式软件系统的需求增加。 典型的应用程序由多个协作进程组成，其中许多进程是多线程的。 线程之间和进程之间的微妙交互的可能性导致了此类系统的设计、实现和测试中的重大挑战。 目前，形式化验证和确认方法提供了对软件系统正确性和可靠性的高度置信度。 模型检测是一种状态空间探索方法，通常应用于软件生命周期的设计阶段，以验证初步的高级设计规范是否符合其要求。 另一方面，源代码（程序）分析用于检查从设计规范实现后实现的正确性。 目前的做法，验证一个设计和它的实现隔离，有必要采用严格的测试分析，以经验确保实现满足设计规范。 主要研究者（PI）声称，软件开发过程的设计和实现阶段的更紧密集成对于弥合规范及其相应实现之间的固有差距是必要的。 PI建议通过一个正式的框架来实现这一点，该框架允许设计模型包含嵌入式部分实现作为组件;然后对这些模型进行正式分析，以确保满足全局需求。 因此，该框架提供了增量开发的灵活性，并确保设计和相应实现的正确性。要实现上述目标，就需要对传统的形式化验证技术进行整合和扩展，将模型检测、程序分析和约束求解的能力结合起来。

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.