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

摘要开发高保证软件的一个主要困难是如何安全地适应并发和同步。并发导致状态爆炸的倾向混淆了验证，而同步逻辑与“功能”代码交织的倾向使理解和维护变得复杂。因此，高保证软件的开发和长期维护需要验证可行的设计工件，以及使用这些工件来维护实现中的关注点分离的过程。本项目旨在实现这些目标。特别地，它探讨了一种基于同步契约的为验证而设计（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.