Logic-based Software Modeling with FOML
Logic-based Software Modeling with FOML
复制标题
DOI：
10.5381/jot.2020.19.3.a19
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Mira Balaban;Igal Khitron;M. Kifer
中科院分区：
文献类型：
--
作者：
Mira Balaban;Igal Khitron;M. Kifer
模型是新兴的基于模型的系统工程(MBSE)方法的核心。MBSE的动机是日益增长的软件复杂性，这需要编程语言不支持的多个抽象级别。在MBSE中，模型在软件演化过程中起着核心作用。丰富的模型管理必须依赖于统一的底层正式框架，该框架可以支持、集成和协调强大的建模服务。本文描述了一个基于L逻辑的面向对象建模框架FOML在一个建模工具中的实现，证明了FOML中类建模的正确性，说明了使用该工具进行软件建模的过程，并介绍了该系统的主要特点。用于软件建模的FOML框架紧凑但功能强大、形式化，并且基于一种称为PathLP的底层逻辑规则语言。将基于类的概念化与形式化逻辑基础相结合，可以清晰地协调和集成广泛的建模活动，并提供可以证明是正确的类模型公式。我们的FOML实现具有多个建模服务的无缝集成功能，这些服务同时支持多个模型，并提供推理、元推理、验证、测试和演化服务。
Models are at the heart of the emerging Model-Based Systems Engineering ( MBSE ) approach. MBSE is motivated by the growing complexity of software, which requires multiple levels of abstraction that programming languages do not support. In MBSE, models play a central role in the software evolution process. Rich model management must rely on a unifying underlying formal framework that can support, integrate, and mediate powerful modeling services. This paper describes FOML, a F ramework for O bject M odeling with L ogic, its realization in a modeling tool, proves the correctness of class modeling in FOML, illustrates the process of software modeling with the tool, and presents the main features of the system. The FOML framework for software modeling is compact yet powerful, formal, and is based on an underlying logic rule language called PathLP. The combination of class-based conceptualization with a formal logical base enables clean mediation and integration of a wide range of modeling activities and provides a provably correct formulation of class models. Our implementation of FOML features seamless integration of multiple modeling services that simultaneously support multiple models and provide reasoning, meta-reasoning, validation, testing, and evolution services.