The complexity of so ware systems in safety cri cal domains (e.g., avionics and automo ve) has significantly increased over the years. To tackle with this complexity, development of such systems requires various phases which result in several ar facts that are increasingly represented as models (e.g., requirement models, architecture models, and design models). To achieve model correctness and thereby to increase so ware quality, formal verifica on of so ware models has become a promising approach and received a considerable amount of a en on in the last decade. Different methods and tools exist in the literature that allow to specify models based on mathema cal theories or formalisms and to reason about the correctness proper es.
In this tutorial, I am going to introduce two mainstream formal specifica on and formal analysis techniques to ensure model correctness on an illustra ve reac ve system. The tutorial will be split into three parts. The first part will immediately introduce to the audience the basic mathema cal no ons required to model an abstrac on of the example reac ve system. The second part demonstrates how to formally specify the system using two different formalisms: first-order rela onal logic (FORL), an expressive logic with transi ve closure supported by Alloy Analyzer and the logic of equality with uninterpreted func ons (EUF), a first-order logic with many well-supported tools (e.g., SMT solvers). The final part presents finding correct instances and checking asser ons wri en in these formalisms using Alloy Analyzer (h ps://github.com/AlloyTools/) and Z3 SMT Solver (h ps://github.com/Z3Prover/z3). All three parts are accompanied by live demonstra ons.