English

Designing Software with Complex Configurations

Software Engineering 2024-07-19 v1
Authors: Alcino Cunha
View on arXiv ↗ PDF ↗

Abstract

In this paper I discuss how can lightweight formal methods be used to specify and verify software with complex configurations (for example, distributed protocols that work on specific network configurations). More specifically, I briefly present two popular formal methods - TLA+ and Alloy - and discuss the pros and cons of both in this particular context.

Keywords

formal verification program analysis theorem proving

Cite

@article{arxiv.2407.13633,
  title  = {Designing Software with Complex Configurations},
  author = {Alcino Cunha},
  journal= {arXiv preprint arXiv:2407.13633},
  year   = {2024}
}

Related papers

View all related →
Software Engineering · Computer Science
Alloy meets TLA+: An exploratory study
Nuno Macedo, Alcino Cunha
2016-03-14
Programming Languages · Computer Science
Validating Traces of Distributed Programs Against TLA+ Specifications
Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier, Stephan Merz
2024-09-18
Logic in Computer Science · Computer Science
Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS
Igor Konnov, Markus Kuppe, Stephan Merz
2022-11-15
Cryptography and Security · Computer Science
A formal methodology for integral security design and verification of network protocols
Jesus Diaz, David Arroyo, Francisco B. Rodriguez
2013-10-29
Software Engineering · Computer Science
A Systematic Literature Review on a Decade of Industrial TLA+ Practice
Roman Bögli, Leandro Lerena, Christos Tsigkanos, Timo Kehrer
2024-11-22
Software Engineering · Computer Science
Enhancing the Alloy Analyzer with Patterns of Analysis
William Heaven, Alessandra Russo
2007-05-23
Software Engineering · Computer Science
A tlm-based platform to specify and verify component-based real-time systems
Mostafavi Amjad Davoud, Zolfy Lighvan Mina
2014-05-01
Formal Languages and Automata Theory · Computer Science
What is Formal Verification without Specifications? A Survey on mining LTL Specifications
Daniel Neider, Rajarshi Roy
2025-01-28
Logic in Computer Science · Computer Science
Formal Verification of Usage Control Models: A Case Study of UseCON Using TLA+
Antonios Gouglidis, Christos Grompanopoulos, Anastasia Mavridou
2018-06-27
Software Engineering · Computer Science
A Short Survey on Formalising Software Requirements using Large Language Models
Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan
2025-06-16
Software Engineering · Computer Science
Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects
Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan
2025-08-29
Logic in Computer Science · Computer Science
Towards Language Model Guided TLA+ Proof Automation
Yuhao Zhou, Stavros Tripakis
2026-03-03
Logic in Computer Science · Computer Science
A Scalable Approach for Hardware Semiformal Verification
Tomas Grimm, Djones Lettnin, Michael Hübner
2018-02-12
Software Engineering · Computer Science
TLA+ Proofs
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz +2
2012-08-30
Logic in Computer Science · Computer Science
Modal Verification Patterns for Systems Software
Ismail Kuru, Colin S. Gordon
2025-09-30
Software Engineering · Computer Science
Validating Formal Specifications with LLM-generated Test Cases
Alcino Cunha, Nuno Macedo
2026-02-19
Logic in Computer Science · Computer Science
Verifying Safety Properties With the TLA+ Proof System
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
2010-11-12
Software Engineering · Computer Science
Towards Classification of Lightweight Formal Methods
Anna Zamansky, Maria Spichkova, Guillermo Rodriguez-Navas, Peter Herrmann +1
2018-07-06
Computation and Language · Computer Science
From Ambiguity to Explicitness: NLP-Assisted 5G Specification Abstraction for Formal Analysis
Shiyu Yuan, Jingda Yang, Sudhanshu Arya, Carlo Lipizzi +1
2023-08-08
Logic in Computer Science · Computer Science
Towards making formal methods normal: meeting developers where they are
Alastair Reid, Luke Church, Shaked Flur, Sarah de Haas +2
2020-11-02
Software Engineering · Computer Science
What Good Are Strong Specifications?
Nadia Polikarpova, Carlo A. Furia, Yu Pei, Yi Wei +1
2013-08-14
Systems and Control · Electrical Eng. & Systems
Verifying Compositional Refinement of Assume/Guarantee Contracts using Linear Programming
Miel Sharf, Bart Besselink, Karl Henrik Johansson
2021-03-26
Software Engineering · Computer Science
Tutorial on the Executable ASM Specification of the AB Protocol and Comparison with TLA$^+$
Paolo Dini, Manuel Bravo, Philipp Paulweber, Alexander Raschke +1
2023-02-01
Networking and Internet Architecture · Computer Science
It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols
David Basin, Nate Foster, Kenneth L. McMillan, Kedar S. Namjoshi +4
2025-09-17
Software Engineering · Computer Science
Natural Language based Specification and Verification
Zhaorui Li, Chengyu Song
2026-05-13
R2 v1 2026-06-28T17:46:13.281Z