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

CCF-BSF：SHF：小型：具有可执行逻辑的软件模型的集成和演化

• 批准号: 1814457
• 负责人: Michael Kifer
• 金额: $ 41.25万
• 依托单位: SUNY at Stony Brook
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-10-01 至 2023-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1814457&HistoricalAwards=false
• 关键词: CCF; BSF; SHF; Small; Integration

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.

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

项目成果

Mediation-based MLM in FOModeLer

FOModeLer 中基于中介的 MLM

• DOI: 10.1145/3550356.3561599
• 发表时间: 2022
• 期刊: ACM
• 作者: Balaban, Mira;Khitron, Igal;Maraee, Azzam;Kifer, Michael
• 通讯作者: Kifer, Michael

Querying Knowledge via Multi-Hop English Questions

• DOI: 10.1017/s1471068419000103
• 发表时间: 2019-09-01
• 期刊: THEORY AND PRACTICE OF LOGIC PROGRAMMING
• 影响因子: 1.4
• 作者: Gao, Tiantian;Fodor, Paul;Kifer, Michael
• 通讯作者: Kifer, Michael

Knowledge authoring for rule-based reasoning

基于规则的推理的知识创作

• 发表时间: 2018
• 期刊: and Applications of Semantics
• 作者: Gao, Tiantian;Fodor, Paul;Kifer, Michael
• 通讯作者: Kifer, Michael

Logic-based Software Modeling with FOML

• DOI: 10.5381/jot.2020.19.3.a19
• 发表时间: 2020
• 期刊: J. Object Technol.
• 作者: Mira Balaban;Igal Khitron;M. Kifer

Knowledge Authoring with Factual English

用事实英语创作知识

• DOI: 10.4204/eptcs.364.10
• 发表时间: 2022
• 期刊: Electronic proceedings in theoretical computer science
• 作者: Wang, Yuheng;Borca-Tasciuc, Giorgian;Goel, Nikhil;Fodor, Paul;Kifer, Michael
• 通讯作者: Kifer, Michael