Collaborative Research: Developing a Constructive Logic-Based Theory of Value-Based Systems Engineering

系统工程是一门学科，负责确保现代的、通常是软件密集型的工程项目的全面成功。成功最终取决于为所有成功关键利益相关者创造价值。创造价值需要理解、指定、管理、验证和发展系统属性之间的复杂权衡，并将这些属性与涉众价值联系起来。这些属性包括，例如，可负担性、可靠性、可演化性、安全性和保密性。然而，今天，主要项目继续出错，很大程度上是由于未能充分指定和管理这些属性和权衡。一个核心问题是，许多属性的定义和理解都非常不精确，导致了误解和混淆。使用自然和准数学语言来定义这些属性的长期尝试并没有解决这个问题。该项目旨在开发和评估高度表达的数学、逻辑和建设性逻辑的计算语言，以产生和验证系统属性、权衡空间以及这些属性与利益相关者价值之间的联系的精确模型。从这种正式的语言规范中，模型的计算机实现将自动生成，并作为web服务提供给系统工程师用于应用和测试。形式语言有可能澄清和揭示不精确、模棱两可、不完整和不一致的自然语言规范中的概念错误。类型理论符号提供基于高阶逻辑、多态类型、计算和命题内容的无缝集成的高表达性，以及从规范中提取认证软件的能力。该项目将采用建设性的逻辑来开发、测试和细化系统属性、权衡和权衡空间映射到涉众偏好的定义和模型。这种方法在系统工程中是新颖的，并且在知识上仍然存在重要的空白。为了填补这些问题，将解决以下研究问题：(1)确定如何最好地表示概率系统属性的类型理论定义中的不确定性；(2)确定适当的机制，以构建能够可靠地专门用于特定项目的一般财产理论；(3)开发和评估系统属性的语言和模型，特别是可演化性属性；(4)开发和评估连接系统设计、财产和价值空间的正式框架；(5)使用户社区能够通过网络服务参与这些理论构建。该项目将开发和测试假设，即基于建设性逻辑的理论可以帮助系统工程师更好地推理系统设计、属性、权衡和涉众价值。

Systems engineering is the discipline responsible for assuring the overall success of modern, often software-intensive, engineering projects. Success ultimately hinges on the creation of value for all success-critical stakeholders. Creating value requires understanding, specifying, managing, validating, and evolving complex trade-offs across properties of systems, and linking such properties to stakeholder value. Such properties include, for instance, affordabilty, reliability, evolvability, safety, and confidentiality. Today, however, major projects continue to go awry in large part due to a failure to adequately specify and manage such properties and trade-offs. A core problem is that many properties are defined and understood so imprecisely that they cause miscommunication and confusion. A long history of attempts to use natural and quasi-mathematical language to define such properties has not solved this problem. This project aims to develop and evaluate the highly expressive mathematical, logical, and computational language of constructive logic to produce and validate precise models of system properties, trade-off spaces, and linkages between such properties and stakeholder values. From such formal language specifications, computer implementations of the models will be automatically generated and provided as web services for application and testing by systems engineers.Formal languages have the potential to clarify and reveal conceptual errors in imprecise, ambiguous, incomplete, and inconsistent natural language specifications. Type theoretical notations offer high expressiveness based on higher-order logic, polymorphic types, and the seamless integration of computational and propositional content, as well as the ability to extract certified software from specifications. This project will employ constructive logic to develop, test, and refine definitions and models of system properties, trade-offs, and the mapping of trade-off spaces to stakeholder preferences. This approach is novel in systems engineering, and important gaps in knowledge remain. To fill them, the following research problems will be addressed (1) determine how best to represent uncertainty in type theoretic definitions of probabilistic system properties; (2) determine appropriate mechanisms for structuring general property theories that can reliably be specialized to specific projects; (3) develop and evaluate languages and models of system properties, including evolvability properties, in particular; (4) develop and evaluate formal frameworks linking system design, property, and value spaces; (5) enable user communities to engage with such theoretical constructs through web services. The project will develop and test the hypothesis that theories based in constructive logic can help systems engineers to reason better about system designs, properties, trade-offs, and stakeholder value.