academia | Roman Bögli

peer-reviewed

FormaliSE

Temporal Logics Meet Real-World Software Requirements: A Reality Check

Roman Bögli, Atefeh Rohani, Thomas Studer, Christos Tsigkanos, and 1 more author

In Proceedings of the 2025 IEEE/ACM 13th International Conference on Formal Methods in Software Engineering (FormaliSE), Ottawa, Canada, Apr 27-28, 2025

Accepted for publication; forthcoming.

Abs HTML

Reasoning on the behavior of software systems is challenging, especially in critical domains such as aerospace. Transitioning from natural language to formal specifications enables long-pursued activities such as modeling, synthesis, and verification. Temporal logics are often used in this regard, each with different operators, expressiveness or associated implementations. However, a significant gap exists between the theoretical capabilities of the logics applied in formal methods and the practical needs for specifying real-world requirements. This paper addresses this gap through a case study of SpaceWire, a standard specification for a data-handling communication protocol often adopted on spacecraft and other on-board systems. We extract 89 software requirements exhibiting temporal behavior and transcribe them into logic-based formalizations using different established temporal logics, maximizing natural encoding. We analyze the suitability of the chosen logics for formalizing the selected software requirements to reason about potential implications for both researchers and practitioners.
iFM
A Systematic Literature Review on a Decade of Industrial TLA+ Practice

Roman Bögli, Leandro Lerena, Christos Tsigkanos, and Timo Kehrer

In Integrated Formal Methods - 19th International Conference, IFM 2024, Manchester, UK, November 13-15, 2024, Proceedings, Nov 2024

Abs DOI Bib Slides

TLA+ is a formal specification language used for designing, modeling, documenting, and verifying systems through model checking. Despite significant interest from the research community, knowledge about usage of the TLA+ ecosystem in practice remains scarce. Industry reports suggest that software engineers could benefit from insights, innovations, and solutions to the practical challenges of TLA+. This paper explores this development by conducting a systematic literature review of TLA+’s industrial usage over the past decade. We analyze the trend in industrial application, characterize its use, examine whether its promised benefits resonate with practitioners, and identify challenges that may hinder further adoption.
@inproceedings{DBLP:conf/ifm/BogliLTK24, author = {B{\"{o}}gli, Roman and Lerena, Leandro and Tsigkanos, Christos and Kehrer, Timo}, editor = {Kosmatov, Nikolai and Kov{\'{a}}cs, Laura}, title = {A Systematic Literature Review on a Decade of Industrial TLA+ Practice}, booktitle = {Integrated Formal Methods - 19th International Conference, {IFM} 2024, Manchester, UK, November 13-15, 2024, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {15234}, pages = {24--34}, publisher = {Springer}, year = {2024}, month = nov, url = {https://doi.org/10.1007/978-3-031-76554-4\_2}, doi = {10.1007/978-3-031-76554-4\_2}, timestamp = {Wed, 08 Jan 2025 21:12:55 +0100}, biburl = {https://dblp.org/rec/conf/ifm/BogliLTK24.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}, }

other

Masters Thesis
Assessing RISC Zero Using ZKit: An Extensible Testing and Benchmarking Suite for ZKP Frameworks

Roman Bögli

Jan 2024

Abs Bib HTML PDF

This thesis summarizes the most important properties of ZKPs and highlights the key differences between two famous implementation families, namely SNARK and STARK systems. Also, we provide a summary of promising software libraries or frameworks that help to create and verify ZKPs. Next, we analyze risc0 in detail using the above-addressed use case of an IP, i.e., proving a the inclusion of leaf in a Merkle tree data structure. Therefore, we propose the concept of ZKit, an extensible toolkit for testing and benchmarking various ZKP frameworks. Besides a Command Line Interface (CLI) to execute parameterized benchmarks or generate Merkle tree test data, it also contains functionality to define and exchange IPs in a unified way. Furthermore, ZKit exemplifies how ZKP circuits written in Rust can be ported to the Go ecosystem through a wrapper library. This portability facilitates the integration of ZKPs in existing Go projects such as for example the Fabric Token-SDK (FTS). Last but not least, we share our risc0 benchmark results on IPs in two different settings. In the first setting, we measured the performance and allocated resources to create one proof for a single IP. In the second setting, we aggregate or batch multiple IPs in a single proof. We compare and interpret the results of these two settings at the end and state our recommendations that we drew from it.
@mastersthesis{bogli2024AssessingRISCZero, type = {Masters Thesis}, title = {Assessing {{RISC Zero}} Using {{ZKit}}: {{An Extensible Testing}} and {{Benchmarking Suite}} for {{ZKP Frameworks}}}, author = {Bögli, Roman}, editora = {El Khiyaoui, Kaoutar and De Caro, Angelo and Caracas, Alexandru}, editoratype = {collaborator}, date = {2024-01-23}, month = jan, year = {2024}, language = {English}, school = {Eastern Switzerland University of Applied Science}, url = {https://eprints.ost.ch/id/eprint/1158/}, }
Semester Project
Zero-Knowledge Inclusion Proofs

Roman Bögli

Aug 2023

Abs Bib HTML PDF

This work discusses a solution for implementing a zero-knowledge inclusion proof using existing software components, referred to as automation frameworks. In the beginning, the use case that necessitates such proofs is stated together with establishing the contextual backdrop. This includes elaborating essential prerequisites such as cryptographic hash functions, commitment schemes, and Merkle trees. Furthermore, it presents an overview of zero-knowledge proof systems, detailing their core characteristics, analogies, and real-world applications. The discussion delves into the two prominent implementation families, namely zkSNARK and zkSTARK, emphasizing their distinguishing features. To ensure resistance against potential threats originating from quantum computers, the proposed approach centers on utilizing non-interactively employed zkSTARK proofs enabled through the Fiat-Shamir transformation. Finally, this work formally states the objective of the zero-knowledge inclusion proof for the specific use case and proposes an algorithmic specification. A curated selection of promising automation frameworks with the potential to facilitate the objective’s implementation is presented, with in-depth scrutiny applied to two specific frameworks: RISC Zero and the Winterfell. The work concludes by discussing initial experiences with these frameworks and outlining future endeavors to chart the path towards implementing a minimal viable product.
@misc{bogli2023ZeroKnowledgeInclusionProofs, title = {Zero-{Knowledge} {Inclusion} {Proofs}}, language = {EN}, publisher = {Eastern Switzerland University of Applied Science}, author = {Bögli, Roman}, collaborator = {El Khiyaoui, Kaoutar and De Caro, Angelo and Purandare, Mitra}, date = {2023-08-21}, month = aug, year = {2023}, url = {https://eprints.ost.ch/id/eprint/1121/}, }
Semester Project
A Security Focused Outline on Bitcoin Wallets

Roman Bögli

Mar 2023

Abs Bib HTML PDF

The famous electronic peer-to-peer cash system called Bitcoin is an open-source protocol allowing individuals to store and transact units of the same named currency. Private and public key cryptography plays a central role in this value transfer system, which implies the importance of professionally managing the information about such keys. This work elaborates on the essential prerequisites to understand this relatively new technology that combines elements from the fields of computer science, cryptography, mathematics, and game theory. In doing so, crucial general and Bitcoin-specific terms are defined and contextually explained. The central part of this work addresses the outline of different Bitcoin interaction means, commonly known as wallets. The structure of the presented wallet types orients itself alongside a potential user’s experience. Besides defining explanations and examples of use cases, this work outlines advantages and disadvantages concerning security and privacy. The start concerns two wallets that target beginners in the field of Bitcoin. The concept of online accounts is elaborated and attention is drawn to the inherent need to trust when using them. Also, the relatively primitive type of paper wallets is surveyed. For a more intermediate interaction with this peer-to-peer cash system, the concept of software wallets, in general, is explained and examples are provided. The bridge from single-address paper wallets will be drawn to the more sophisticated multi-address wallets enabled through rooted key derivation techniques. Designated computer devices that solely serve the purpose of managing keying material, known as hardware wallets, represent another intermediate wallet type discussed in this work. Last, advanced topics are discussed that further leverage the security and privacy of someone’s interaction with Bitcoin. One concerns the setup of a self-managed Bitcoin full node. This undertaking not only harmonies with the concept of verification over trust but also allows for the complete exclusion of any third party between wallet communication. Equally advanced is the concept of multi-signature wallets, which is discussed at the end of this work.
@misc{bogli2023SecurityFocusedOutline, title = {A {Security} {Focused} {Outline} on {Bitcoin} {Wallets}}, language = {en}, publisher = {Eastern Switzerland University of Applied Science}, author = {Bögli, Roman}, collaborator = {Weiler, Nathalie}, date = {2023-03-07}, month = mar, year = {2023}, url = {https://eprints.ost.ch/id/eprint/1103/}, }

Bachelors Thesis

Time Series Clustering with Water Temperature Data

Roman Bögli

Aug 2020

Abs Bib HTML PDF

@thesis{bogli2020TimeSeriesClustering,
  type = {Bachelors Thesis},
  title = {Time {Series} {Clustering} with {Water} {Temperature} {Data}},
  language = {English},
  school = {University of Applied Sciences and Arts Northwestern Switzerland (FHNW)},
  author = {Bögli, Roman},
  collaborator = {Bigler, Vidushi C.},
  date = {2020-08-07},
  month = aug,
  year = {2020},
  url = {https://studierendenprojekte.wirtschaft.fhnw.ch/view/61},
}

Semester Project
Statistical vs. Structural Pattern Recognition - A Survey

Roman Bögli

Dec 2019

Abs Bib PDF

This paper surveys the different approaches in pattern recognition (PR). After the fundamental idea of PR is stated, a taxonomy landscape is presented which divides into three families, namely statistical, structural, and hybrids. The first represents a well-researched topic in PR which engendered popular and efficient supervised and unsupervised pattern discovery algorithms. The second family addresses techniques to find patterns in structurally represented data using graphs that allow capturing the information of relationships among objects. Thirdly, the hybridization of the prior two families will be discussed. This includes the elaboration of transformation methods that allow to embed a graph into a vector space using graph kernels or graph embedding.
@misc{bogli2019StatisticalVsStructural, type = {Literature {Review}}, title = {Statistical vs. {Structural} {Pattern} {Recognition} - {A} {Survey}}, language = {English}, publisher = {University of Applied Science and Arts Northwestern Switzerland (FHNW)}, author = {Bögli, Roman}, date = {2019-12-24}, month = dec, year = {2019}, }

supervised

Bachelors Thesis
An Algorithmic Approach for Solving the Grouping Problem

Andrin Müller, and Viola Meier

Feb 2025

Abs Bib

The grouping problem, a challenging combinatorial optimization problem classified as NP-hard, seeks to divide a set of objects into optimal groups while satisfying predefined constraints. This thesis explores algorithmic approaches to solve this problem for fixed group sizes and in scenarios involving must-link and cannot-link constraints, which enforce mandatory co-membership or exclusion between specific individuals. The primary focus is on developing novel methods for encoding features and constraints that minimize total intra-group distances, ensuring the desired homogeneity or heterogeneity at the feature level. One of the key contributions of this work is the development of a unified feature encoding technique that accommodates various feature types, enhancing the accuracy of member compatibility analysis by seamlessly integrating both homogeneous and heterogeneous features. Another significant contribution is the transformation of compatibility measurements into a single-objective optimization framework, which simplifies the computational process. This transformation enables the evaluation of member compatibility with greater efficiency, ensuring that the minimization of intra-group distances remains the central objective. Additionally, the thesis presents three algorithmic approaches for group assembly: Ant Colony Optimization (ACO), a customized PCKMeans clustering algorithm, and the Occurrence Ranking (OCCR) approach. Each of these algorithms provides a different strategy for solving the grouping problem and can be adapted for various optimization objectives. The effectiveness and efficiency of these algorithms are thoroughly evaluated, with performance metrics tailored specifically for group formation tasks. This evaluation demonstrates their capability to generate optimal groupings in a reasonable computational time frame. The experimental results highlight the potential applications of these methods in collaborative learning, team-building, and other domains that require structured group formation. The findings also lay the groundwork for future work, including improvements to algorithm scalability, the integration of more complex constraints, and the exploration of alternative optimization techniques.
@thesis{muellerMeierAGAT, type = {Bachelors Thesis}, title = {An Algorithmic Approach for Solving the Grouping Problem}, language = {English}, school = {University of Bern}, author = {Müller, Andrin and Meier, Viola}, supervisor = {Kehrer, Timo and Bögli, Roman}, date = {2025-02-06}, month = feb, year = {2025}, }