Advanced Design Methods for Critical Components of Concurrent Systems

这项工作的目的是评估形式程序派生技术在并发系统的关键(但大小合理)组件设计中的潜在使用。将解决几个技术问题。程序规范的概念将被扩展为不仅包括行为规范，而且还包括正式指定的约束，例如，目标体系结构的特征。正式声明的约束将为设计过程提供额外的正式指导，并将导致新程序派生方法的出现。这项研究的正式组成部分将通过若干案例研究的实验加以补充，从文献中具有普遍吸引力的简单问题到与工业伙伴合作选择的实际组成部分。在工业级问题上成功地使用形式推导技术将需要形式方法和实际见解的仔细结合。关于后者，迄今的经验表明有两个特别有希望的想法可供评估。首先是将大部分设计过程从昂贵的形式证明中解放出来，而不损害形式推导典型的有纪律的思维。第二，是由已经开发的最先进的程序可视化设施提供强大的视觉探索、通信和原型能力的想法。

The objective of this work is to evaluate the potential use of formal program derivation techniques in the design of critical (yet reasonable-sized) components of concurrent systems. Several technical issues will be addressed. The notion of program specification will be extended to include not only a behavior specification but also formally specified constraints, e.g., the characteristics of the target architecture. The formally stated constraints will provide additional formal guidance to the design process and will lead to the emergence of new program derivation methods. The formal component of this research will be complemented by experimentation with a number of case studies ranging from simple problems having popular appeal in the literature to real components selected in cooperation with an industrial partner. Successful use of formal derivation techniques on industrial-grade problems will require a careful blend of formal methods and practical insights. Regarding the latter, experience to date suggests two particularly promising ideas to evaluate. First, is the notion of freeing much of the design process from costly formal proofs without compromising the disciplined thinking typical of formal derivation. Second, is the idea of providing powerful visual exploration, communication, and prototyping capabilities supplied by an already developed state-of-the art program visualization facility.