Designing Software with Complex Configurations
Alcino Cunha
TL;DR
This paper explores how lightweight formal methods like TLA+ and Alloy can be used to specify and verify software with complex configurations, such as distributed protocols on specific networks.
Contribution
It compares two formal methods, TLA+ and Alloy, highlighting their advantages and disadvantages for complex configuration verification.
Findings
TLA+ is effective for specifying distributed protocols.
Alloy provides flexible modeling for complex configurations.
Both methods have unique strengths and limitations.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Engineering Research · Model-Driven Software Engineering Techniques · Advanced Software Engineering Methodologies