skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Logic-based Software Modeling with 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 Framework for Object Modeling with Logic, 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.  more » « less
Award ID(s):
1814457
PAR ID:
10188061
Author(s) / Creator(s):
Date Published:
Journal Name:
Journal of object technology
Volume:
19
Issue:
1
ISSN:
1660-1769
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. MLM has attracted much attention over the last two decades. MLM activities include philosophical discussions about ontologies, requirements and relevant services, and development of theories, languages, and tools. Approaches differ in their support for MLM concepts on the levels of syntax, semantics and pragmatics. The Mediation-based MLM (MedMLM), is a formal theory that defines a multilevel model as an ordered collection of levels that are inter-related by mediators, and can be enriched by inter-level relationships and interactions. The levels of MedMLM are plain class models, and the mediators define inter-level instantiation relations. MedMLM is unique in supporting a modular architecture of levels and mediators. This paper introduces the MedMLM software modeling tool, that is built on top of the FOModeLer class modeling tool. The tool supports MLM construction, querying and reasoning, meta-reasoning, validation, syntax verification, and plain computation. We also compare the MedMLM tool with older MLM approaches using semantic, syntactic, and pragmatic MLM criteria. 
    more » « less
  2. Model-based systems engineering (MBSE) is being rapidly adopted in U.S. industries across various sectors. While practitioners and academics recognize many benefits of adopting MBSE, industries also report challenges such as limited tool expertise and a shortage of skilled personnel. Highlighting the difficulties in industry adoption of MBSE, prior research by the authors identified challenges such as tool limitations, knowledge gaps, cultural and political barriers, costs, and the level of customer understanding and acceptance of MBSE practices. Additionally, another study by the authors points out a gap between industry demands for MBSE skills in new hires and the current academic training programs. To further assess the MBSE industry’s workforce needs, this paper introduces a two-phase method for the Structured Extraction of MBSE competencies using large language models based on current workforce demands from LinkedIn job postings. Phase 1 involved extracting 1960 job descriptions from LinkedIn using the term “model-based systems engineer.” In phase 2, large language models (LLMs) employing deep transformer architectures were used to transform unstructured text into structured data. An AI agent was used as an autonomous software layer to manage every interaction between the raw dataset from Phase 1 and the LLM. Supported by the analyzed data, a competency framework is proposed that summarizes the tools, technical skills, and soft skills expected of a model-based systems engineer by the industry. The framework is designed to include core competencies shared across all MBSE roles, with specific competencies tailored for aerospace & defense, manufacturing and automotive, and software and IT sectors. 
    more » « less
  3. Abstract This paper describes model construction practices used by scientifically trained experts. Our work on science experts has involved analyzing data from videotaped protocols of experts thinking aloud about unfamiliar explanation problems. These studies document the value of nonformal heuristic reasoning processes such as analogies, identification of new variables, Gedanken experiments, and the construction and running of visualizable explanatory models. Although theses processes are less formal than formal deduction or induction or statistical inference procedures, the case study analyzed here shows that they can lead to real insights and conceptual change. At a larger time scale, the subject went through model evolution cycles of model generation, evaluation, and modification that utilized the heuristic reasoning processes above. In addition, the prevalence of imagistic simulation as an underlying foundation in these episodes suggests that it may be important to pay greater attention to an imagistic level of processing in the analysis of expert thinking. Larger time scale modes of model evolution and model competition were also evidenced. The analysis leads to four levels of processes or practices: IV. An overarching set of Model Construction Modes, primarily alternating between Model Evolution, in which a model is improved, and Model Competition, in which two or more models compete. III. Modeling (GEM) Cycle process of Model Generation, Evaluation, and Modification at a Macro level, as shown in Figure 10. II. Nonformal Reasoning Processes at a Micro level: e.g. analogy, running a model, identifying a new variable, and conducting a Gedanken experiment. I. Underlying Imagistic process including Imagistic Simulation that may have been occurring within all of the above processes. To our knowledge these four levels of processes have not been analyzed together in the past. They complement empirical processes of discovery, experimentation, and evaluative argumentation documented by others. Diagrams of how the above processes interact may give us some new ways to picture the roles of nonformal reasoning and imagistic processes during qualitative model construction. We call the set of processes at all four levels a 'Modeling Practices Framework'. Processes at a lower level serve as subprocesses for the level above it in this framework. Each level has multiple "things to try" to achieve tasks at the level above it. Thus the framework is an organized but flexible structure of heuristic processes. This lies between and contrasts with those who would describe theory making in science as either 'anarchistic', with no method structure, or 'algorithmic', with fairly standardized procedures. 
    more » « less
  4. Industrial control systems (ICS) are increasingly targeted by sophisticated attacks on sensors and actuators, necessitating advanced frameworks that enable proactive mitigation. This paper introduces HyTwin, a formal framework that models both adversarial actions and corresponding mitigation strategies through digital twin-based interventions. HyTwin leverages differential dynamic logic (dL) to represent the temporal evolution of attacks and quantify the mitigation horizon, a critical parameter enabling precise reasoning about when and how to deploy fail-safe mechanisms during ongoing attacks. Our approach integrates temporal semantics with attack models to dynamically engage fail-safe controls. This work provides a rigorous framework for designing proactive countermeasures that preserve system safety, ensuring robustness in adversarial scenarios. The proposed framework establishes a foundation for advancing ICS security through verifiable temporal reasoning and contributes to bridging gaps between theoretical modeling and real-world industrial applications. 
    more » « less
  5. Commitments support flexible interactions between agents by capturing the meaning of their interactions. However, commitmentbased reasoning is not adequately supported in agent programming models. We contribute Azorus, a programming model based on declarative specifications centered on commitments and aligned with information protocols. Azorus supports reasoning about goals and commitments and combines modeling of commitments and protocols, thereby uniting three leading declarative approaches to engineering decentralized multiagent systems. Specifically, we realize Azorus over three existing technology suites: (1) Jason, a popular BDI-based programming model; (2) Cupid, a formal language and query-based model for commitments; and (3) BSPL, a language and its associated tools for information protocols, including Jason programming. We implement Azorus and demonstrate how it enables capturing interesting patterns of business logic. 
    more » « less