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

Stirewalt摘要：高保证软件开发中的一个主要困难是安全地适应并发和同步。并发导致状态爆炸的倾向混淆了验证，而同步逻辑与“功能”代码交错的倾向使理解和维护变得复杂。因此，高保证软件的开发和长期维护需要验证是可行的设计构件，以及使用这些构件在实现中保持关注点分离的过程。具体地说，它探索了一种基于同步契约的设计用于验证(Design-for-Verify，D4V)方法，该方法提供了支持验证所需的高级抽象，同时保持了同步和功能关注点的良好分离。我们正在开发编程系统，以利用契约意识进行分析；从设计构件(例如，UML图)自动生成模型；以及分离同步和功能关注点。我们正在现有软件基线的背景下进行这些探索。该项目还涉及并行系统设计、基于模型的软件工程和D4V的本科生课程的开发。一个基准是本科生能够在多大程度上使用根据这项拨款开发的工具和方法来设计和验证合同意识项目。

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.