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.