Abstract: Light-Weight Analysis of Compositional Designs --- Towards Compositional Verification.

Modern systems are continuously increasing in scale and complexity, causing a proportionate increase in the complexity of their design and verification. Formal analysis is of particular interest in this area because it provides the mathematical foundation necessary for rigorous analysis of computer systems; successful formal analysis of a system provides a high level of assurance of correctness and conformance with specifications. Unfortunately, for a number of reasons, formal analysis techniques have failed to scale to large systems. In traditional engineering disciplines, decomposition and component-based design activities have contributed substantially to effective design of large systems. We contend that similar techniques can be utilized to extend formal analysis to large-scale systems. Towards that end, this paper presents some proof obligations that perform light-weight checks on systems that are designed decompositionally. The proof obligations are extracted automatically from each design. They represent initial steps towards the goal of decompositional verification of designs.
Back to Nael's homepage , or view my resume .