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

Stirewalt摘要：在高保证软件开发的主要困难是安全地容纳并发和同步。 并发导致状态爆炸的倾向使验证变得混乱，同步逻辑与“功能”代码交织的趋势使理解和维护变得复杂。 因此，高保证软件的开发和长期维护需要验证可行的设计工件，以及使用这些工件在实现中保持关注点分离的过程。 具体来说，它探讨了一种基于同步合同的设计验证（D4 V）方法，该方法提供了支持验证所需的高层次抽象，同时保持了同步和功能问题的良好分离。 我们正在开发利用合同意识进行分析的编程系统;从设计工件自动生成模型，（例如，UML图）;以及分离同步和功能关注点。我们正在现有软件基线的背景下进行这些探索。该项目还涉及开发并行系统设计，基于模型的软件工程和D4 V的本科课程。一个基准是本科生能够在多大程度上设计和验证合同意识的程序使用的工具和方法下开发的这个补助金。

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.