CCF-BSF: SHF: Small: Integration and Evolution of Software Models with Executable Logic

基于模型的系统工程（MBSE）是一种用于构建大型软件系统的方法，在这种方法中，人们用建模语言描述系统，一旦模型被认为是一致和正确的，然后将模型转换为软件程序。MBSE方法是由不断增长的软件复杂性所驱动的，它需要在多个抽象层次上对软件系统进行多个视图。编程语言不支持这种建模活动，它触发了新的建模技术和各种模型级服务的开发，例如模型验证和确认、测试、分析、转换、重构、设计模式、元建模和模型演化。这项研究的目标是开发一个可执行的正式建模框架，它可以支持和集成各种各样的建模任务，从而能够构建健壮的大型软件系统。该项目的目标是为模型工程开发逻辑基础和推理服务的原型实现。特别地，该计划将重点放在基于中介的集成、划分和软件模型的演化上，并使用最近开发的语言F-OML，该语言受到F-logic、HiLog和事务逻辑的启发。F-OML是一种紧凑但功能强大的基于逻辑的语言，由定义良好的语义和可证明正确的执行方法支持。该项目包括以下主要工作：(1)构建推理服务的逻辑基础，包括高阶能力、动作、不一致或不完整知识下的推理和解释生成；(2)为软件模型的集成（纵向和横向）和进化建立统一的逻辑基础；(3)基于上述思路构建MBSE系统的概念验证原型；(4)通过案例研究和基准模型对所提出的方法进行评价。这个项目涉及许多具有挑战性的问题，从模型的推理到模型的验证和集成，再到模型引导的代码生成，再到模型划分和进化。这项工作的预期结果将是用于基于逻辑的系统工程的中介推理服务的理论、算法和原型，这将支持建模服务的集成和发展。最终将这些服务合并到现有的交互式软件开发环境中，将使软件工程师能够获得新的功能，从而提高他们所生产软件的生产力和可靠性。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Model Based Systems Engineering (MBSE) is an approach for building large software systems in which one describes the system in a modeling language and, once the model is considered consistent and correct, then transforms the models into software programs. The MBSE approach is motivated by the growing complexity of software, which requires multiple views of the software system at multiple levels of abstraction. Programming languages do not support this modeling activity, which has triggered the development of new modeling technologies and a variety of model-level services such as model verification and validation, testing, analysis, transformation, refactoring, design patterns, meta-modeling, and model evolution. The goal of this research is to develop an executable formal modeling framework that can support and integrate a wide variety of modeling tasks, and thus enable the building of robust, large software systems. The goal of this project is to develop logical foundations and a prototype realization of reasoning services for model engineering. In particular, the plan is to focus on mediation-based integration, partitioning, and evolution of software models and use the recently developed language, F-OML, inspired by prior work on F-logic, HiLog, and Transaction Logic. F-OML is a compact yet powerful logic-based language supported by a well-defined semantics and a provably correct execution method. The project includes the following main efforts: (1) Building logical foundations for reasoning services, including higher-order capabilities, actions, reasoning under inconsistent or incomplete knowledge, and explanation generation; (2) building uniform logical foundations for integration (vertical and horizontal) and evolution of software models; (3) building a proof-of-concept prototype of an MBSE system based on the above ideas; and (4) evaluation of the proposed approach via case studies and benchmark models. This project involves a number of challenging problems ranging from reasoning about models to verification and integration of models to model-guided code generation to model partitioning and evolution. The expected outcome of this work will be a theory, algorithms, and a prototype for mediated reasoning services for logic-based systems engineering, which will support integration and evolution of modeling services. Eventual incorporation of such services into existing interactive software development environments will make the new capabilities available to software engineers to increase their productivity and reliability of the software they produce.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.