A formalization of a startup finance transaction model using Alloy - Stevaux, Rodrigo Ehrlich (2023)
This dissertation presents a software design of a fragment of the domain of startup financing. Our design can be machine-checked for key safety integrity properties, and is written as a formal specification of the domain. In the given domain, we start from a data specification language built by an industry coalition. The data specification describes how our domain can be modeled from a syntactic perspective. We give it semantics by adopting the Alloy formal modeling language and analyzer, aiming at a more expressive and correct model, by capturing invariants in the problem domain. Our model and can be explored and checked automatically by the Alloy Analyzer. We can both express and check for critical invariants of the problem domain. Our research contributes to the field of formal methods as it shows how one can proceed from a semiformal specification to a formal one, evaluates what the results, and contributes to other researchers and practitioners in the field of formal methods by providing a case study of a real-world problem domain.