Lightweight Formal Support for Software Design

软件系统是我们的社会和经济日常运作所依赖的基础设施的核心。它们是软件开发人员每天所做的无数设计决策的累积产物。因此，它们的质量在很大程度上取决于它们的设计过程。 尽管经过了几十年的创新，但由于软件设计固有的创造性和协作性以及当代软件行业不断变化的速度，正式的数学工程技术往往面临很高的采用障碍。软件设计仍然是一门手艺，也是一门工程学科。 该研究计划旨在帮助软件设计人员在当代软件工程的压力面前平衡效率和质量。 关键在于识别利基设计环境，在这种环境中，形式化技术可以变得"轻量级"，即，对用户技能和计算资源的要求降低。这减少了采用障碍，而重要的是，丰富的上下文信息弥补了失去的表达能力和/或分析能力。 具体来说，我的目标是研究软件设计的背景，以便明智地应用形式化技术，有力地支持设计师的创造力。 这一背景描述了需要做出的设计决策，并确定了可能的设计解决方案的空间。 因此，拟议的研究计划有以下目标：（a）识别和表征的设计决策和他们的背景下使用"设计仪表板"，（B）创建一个"轻量级设计工具包"的正式技术管理的空间设计解决方案，和（c）集成的技术在现代软件开发方法中使用"灵活的建模工具"。 该计划的成果将是特定于上下文的软件设计理论，这些理论所告知的轻量级形式化技术，以及可以在各种软件设计环境中部署的实现它们的工具。这些成果将使从业者受益，使他们能够在新的开发环境中使用强大的工程技术。 此外，它将进一步科学地理解在现代软件设计环境中创建和部署实用的正式设计和分析技术所涉及的权衡。最终，这项研究计划将提高高质量软件生产的最先进水平，同时培养具有经验，正式和以用户为中心的软件工程专业知识的高素质人才。

Software systems are at the heart of the infrastructure that our societies and economies depend on for their daily function. They are the accumulated product of the myriads of design decisions made by software developers every day. Their quality is thus highly dependent on the process by which they are designed. Despite decades of innovation, formal, mathematical engineering techniques often face high adoption barriers because of the inherently creative and collaborative character of software design and the unrelenting rate of change in the contemporary software industry. Software design remains as much a craft as an engineering discipline. This research program aims to help the designers of software balance efficiency and quality in the face of the pressures in contemporary software engineering. The key lies in identifying niche design contexts in which formal techniques can be made "lightweight", i.e., with reduced demands on user skill and computational resources. This reduces adoption barriers, while, crucially, rich contextual information makes up for the lost expressiveness and/or analytical power. Specifically, I aim to study the context of software design in order to judiciously apply formal techniques that robustly support designers' creativity. This context characterizes the design decisions that need to be made and determines the space of possible design solutions. Therefore the proposed research program has the following objectives: (a) identification and characterization of design decisions and their context using a "Design Dashboard", (b) creation of a "Lightweight Design Toolkit" of formal techniques for managing the space of design solutions, and (c) integration of the techniques within modern software development methodologies using "Flexible Modelling Tools". Outcomes of this program will be context-specific theories of software design, lightweight formal techniques informed by these theories, and tools implementing them that can be deployed in various software design settings. These outcomes will benefit practitioners by allowing them to use robust engineering techniques in new development contexts. Additionally, it will further the scientific understanding of the tradeoffs involved in the creation and deployment of practical formal design and analysis techniques in modern software design settings. Ultimately, this research program will improve the state of the art in the production of quality software, while producing highly-qualified personnel with expertise in empirical, formal, and user-centered software engineering.