Formal methods in the scope of the Software and Systems Modeling journal

Marsha Chechik, Benoît Combemale, Jeff Gray, Bernhard Rumpe

<figure><img src="image_1.png" /></figure>

To cite this version:

Marsha Chechik, Benoît Combemale, Jeff Gray, Bernhard Rumpe. Formal methods in the scope of the Software and Systems Modeling journal. Software and Systems Modeling, 2025, 24 (2), pp.271-272. 10.1007/s10270-025-01287-0. hal-05108048

HAL Id: hal-05108048

https://hal.science/hal-05108048v1

Submitted on 11 Jun 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>
Formal methods in the scope of the Software and Systems Modeling journal

Marsha Chechik<fnref n="1" /> · Benoit Combemale<fnref n="2" /> · Jeff Gray<fnref n="3" /> · Bernhard Rumpe<fnref n="4" />

Published online: 22 April 2025

© The Author(s) 2025

Software and Systems Modeling (SoSyM) is a journal dedicated to advancing the field of software and systems modeling by publishing high-quality research that contributes to the theory and practice of modeling in software and systems engineering, which also includes processes executed automatically or involving humans. The journal aims to bridge the gap between academia and industry by fostering discussions on modeling languages, methodologies, tools, and their applications to real-world challenges. SoSyM encourages submissions that present innovative modeling approaches, their precise semantic foundations, empirical evaluations, and applications that have tangible impacts on software and system development processes.

Given this mission, the journal welcomes research on formal methods, provided that such work is framed within the context of software and systems modeling. Formal methods, as mathematically rigorous techniques for specifying, developing, and verifying software and systems, undoubtedly have significant potential to enhance modeling practices. However, the focus of SoSyM is not formal methods in isolation but rather their role and contribution to the field of software and systems modeling.

Thus, a manuscript that centers on a formal method must explicitly articulate its relevance to software and systems modeling. This means that a submission should not merely

introduce a new formalism or theoretical result; instead, it must also ground the contribution in a concrete modeling challenge or need within the software and systems modeling domain. Note that the use of the formalism for reasoning is not sufficient, per se! Authors should clearly demonstrate how their work advances the state of the art in modeling by addressing specific problems, improving existing methodologies, or enabling novel applications. Moreover, an evaluation should be provided to illustrate the impact and practical applicability of the proposed approach within the modeling domain. Such an evaluation should leverage one or more case studies that are representative of real-world challenges.

Furthermore, positioning is crucial in establishing the relevance of formal methods research to SoSyM. Manuscripts should not only compare their proposed formal techniques against existing formal approaches but, more importantly, situate their contributions within the broader landscape of software and systems modeling. This includes discussing how the proposed method relates to and extends existing modeling techniques, frameworks, and tools.

For instance, a submission might explore how a formal verification technique enhances model-based software design by detecting inconsistencies in UML state machines before implementation, thereby preventing costly errors. Another example could be the application of formal refinement techniques to ensure that high-level architectural models, e.g., defined in SysML or another ADL, correctly translate into executable system components, improving traceability and correctness in model-driven engineering workflows. Likewise, work on domain-specific modeling languages (DSMLs) could integrate formal semantics to enable a precise understanding of the meaning of a model, or even automated reasoning about system properties, such as safety, security or performance constraints, within a modeling environment. Case studies demonstrating how formal methods improve the precision and reliability of digital twin models of cyber-physical systems would illustrate their practical impact on real-world modeling challenges. These

<figure><img src="image_3.png" /></figure>

Bernhard Rumpe
bernhard.rumpe@sosym.org

Marsha Chechik
marsha.chechik@sosym.org

Benoit Combemale
benoit.combemale@sosym.org

Jeff Gray
jeff.Gray@sosym.org

<footnote n="1">¹ University of Toronto, Toronto, ON, Canada</footnote>

<footnote n="2">² University of Rennes, Rennes, France</footnote>

<footnote n="3">³ University of Alabama, Tuscaloosa, AL, USA</footnote>

<footnote n="4">⁴ RWTH Aachen University, Aachen, Germany</footnote>
examples highlight how formal methods can meaningfully
contribute to software and systems modeling.

However, a paper that solely introduces a new temporal
logic without demonstrating or at least discussing its rel-
evance to modeling practices would not be suitable, as it
lacks a concrete connection to software and systems mod-
eling challenges. Similarly, a study that proves theoretical
properties of a formal specification language without show-
ing how it improves a modeling methodology or tool would
not meet the journal's criteria.

Another counter example is work that extends a model-
ing notation, e.g., by encoding numerical constraints or data
properties, with the primary goal of enabling effective rea-
soning, without specific integration in a development setting.
In these cases, while the research may really be valuable
within the realm of formal methods, it does not sufficiently
engage with the core mission of advancing software and sys-
tems modeling without tying the verification process to a
practical software or systems modeling context, and thus,
the paper would be out of scope for SoSyM.

In summary, SoSyM welcomes research on formal meth-
ods insofar as it aligns with the journal's core mission of
advancing software and systems modeling. Authors submit-
ting such manuscripts should ensure that their contributions
are motivated by concrete modeling challenges, supported by
rigorous evaluation, and positioned within the broader soft-
ware and systems modeling research landscape. By adhering
to these principles, contributions from the formal methods
community can play a vital role in strengthening the field
of software and systems modeling and fostering meaningful
advances in both theory and practice.

We look forward to receiving high-quality submissions
that apply or integrate formal methods into the rich and evolv-
ing discourse of software and systems modeling.

**Open Access** This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.

**Funding** Open Access funding enabled and organized by Projekt DEAL.

**Publisher's Note** Springer Nature remains neutral with regard to juris-
dictional claims in published maps and institutional affiliations.