A Formal Model for Startups Financial Transactions

• Rodrigo Stevaux USP https://orcid.org/0009-0001-6127-4115
• Ana C. V. de Melo USP https://orcid.org/0000-0003-3839-8141

Resumo

This paper proposes a formal model for a subset of the startup finance transaction space. The initial version of the provided domain is the result of an industry coalition effort to make the data model standard. The data definition explains how this domain can be modeled syntactically. We refined this first model with semantics on transactions by using the Alloy formal modeling language and analyzer, aiming for a more expressive and correct model by capturing domain invariants. As a result, the new model is machine-checkable for important safety integrity criteria. This research contributes to the field of formal methods by demonstrating how to progress from a semi-formal specification to a formal one, evaluating the results, and providing a case study of a real-world domain.

Palavras-chave: Formal methods, Financial modeling, Alloy