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.

Essa dissertação apresenta um design de software de um fragmento do domínio de financiamento de startups. Nosso design pode ser verificado por máquina quanto a propriedades chave de integridade de segurança e é escrito como uma especificação formal do domínio. No domínio em questão, começamos a partir de uma linguagem de especificação de dados construída por uma coalizão da indústria. A especificação de dados descreve como nosso domínio pode ser modelado de uma perspectiva sintática. Damos a ela semântica adotando a linguagem de modelagem formal Alloy e analisador, visando um modelo mais expressivo e correto, capturando invariantes no domínio do problema. Nosso modelo pode ser explorado e verificado automaticamente pelo Analisador Alloy. Podemos tanto expressar quanto verificar invariantes críticos do domínio do problema. Nossa pesquisa contribui para o campo dos métodos formais, pois mostra como se pode proceder de uma especificação semiformal para uma formal, avalia os resultados e contribui para outros pesquisadores e praticantes no campo dos métodos formais ao fornecer um estudo de caso de um domínio de problema do mundo real.