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

系统工程是负责确保现代，通常是软件密集型工程项目的整体成功的学科。成功最终取决于为所有成功关键利益相关者创造价值。创造价值需要理解，指定，管理，验证和发展系统属性之间的复杂权衡，并将这些属性与利益相关者的价值联系起来。这些属性包括，例如，可负担性、可靠性、可进化性、安全性和机密性。然而，今天，主要项目继续出错，在很大程度上是由于未能充分指定和管理这些属性和权衡。一个核心问题是，许多属性的定义和理解是如此不精确，以至于它们会导致误解和混乱。长期以来，人们一直试图用自然的和准数学的语言来定义这些性质，但都没有解决这个问题。该项目旨在开发和评估建设性逻辑的高度表达性的数学，逻辑和计算语言，以产生和验证系统属性，权衡空间以及这些属性和利益相关者价值之间的联系的精确模型。从这样的正式语言规范，计算机实现的模型将自动生成和提供的应用程序和测试的系统engineer.Formal语言有可能澄清和揭示不精确，模糊，不完整和不一致的自然语言规范的概念错误的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.