12/13/2018                                          UYMK Tutorial (Ferhat Erata) - Google Docs




                        Formal Specification and Verification of System and Software Models
                                                       Ferhat Erata
                                          UNIT Informa on Technologies R&D Ltd.
                                                  (ferhat@computer.org)

          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.




https://docs.google.com/document/d/1JSVmX6yUPwQNn7lgjQrtqzMFIBe3eNIjryeZ9zJReRE/edit                                    1/1