A formalization of a startup finance transaction model using Alloy

• Ano de defesa: 2023
• Autor(a) principal: Stevaux, Rodrigo Ehrlich
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Instituição de defesa: Biblioteca Digitais de Teses e Dissertações da USP
• Palavras-chave em Português: Alloy analyzer; Bounded-model checking; Capitalization table management; Domain-specific formalisms; Especificação formal; Especificações de dados semânticas; Financiamento de capital de risco; Formal methods; Formal specification; Formalismos específicos do domínio; Gestão de tabela de capitalização; Métodos formais; Semantic data specifications; Venture capital; Verificação de modelo limitado
• Link de acesso: https://www.teses.usp.br/teses/disponiveis/45/45134/tde-05042024-151358/

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.