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

Suny At Stony Brook, Stony Brook NY

Investigators

Abstract

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.