Verification of computer-based systems by model checking in tla+ toolbox environment

Formal verification – demonstration of the correctness of an algorithm (computer program or system) in relation to a specification using formal mathematical methods. There are two methods of verification – model checking and theorem proving. The goal of this thesis is to formalize the characteristics of an adaptive computer system and verify several versions (i.e. configurations) of it by model checking in TLA+ Toolbox environment. The considered versions of the adaptive computer system differ by specific integrated dynamic reconfiguration mechanisms. The last version of the computer system has the local view mechanism implemented – each system component of a specific type (control base) has its own isolated understanding of the current global situation which is updated during system work. The presented verification results demonstrate that every adaptive computer-based systems version meets the requirements formulated for it, terminates and in any case, eventually, ends the execution in the required state. The results are compared to determine how the specific dynamic reconfiguration mechanism affects the number of ways the adaptive computer system can act