Using Contracts to Support Development, Verification, and Maintenance of Multi-threaded Systems

Michigan State University, East Lansing MI

Investigators

Abstract

Stirewalt Abstract: A principal difficulty in the development of high-assurance software is to safely accommodate concurrency and synchronization. The propensity for concurrency to engender state-explosion confounds verification, and the tendency for synchronization logic to be interleaved with "functional" code complicates understanding and maintenance. Thus, development and long-term maintenance of high-assurance software requires design artifacts over which verification is feasible and processes that use these artifacts to maintain separation of concerns in the implementation. This project aims to achieve these goals. Specifically, it explores a design-for-verification (D4V) approach based on synchronization contracts, which provides the high level of abstraction needed to support verification while maintaining a good separation of synchronization and functional concerns. We are developing programming systems that leverage contract awareness for analysis; to automate the generation of models from design artifacts, (e.g., UML diagrams); and to separate synchronization and functional concerns. We are conducting these explorations in the context of an existing software baseline. The project also involves development of undergraduate courses in concurrent systems design, model-based software engineering, and D4V. One benchmark is the extent to which undergraduates are able to design and verify contract-aware programs using the tools and methods developed under this grant.