ABS TRACT
Showing posts with label software analysis. Show all posts
Showing posts with label software analysis. Show all posts
Sunday, August 2, 2015
Monday, July 20, 2015
Generalized Büchi automaton
In automata theory, generalized Büchi automaton (GBA) is a variant of Büchi automaton. The difference with the Büchi automaton is its accepting condition, i.e., a set of sets of states. A run is accepted by the automaton if it visits at least one state of every set of the accepting condition infinitely often. Generalized büchi automata (GBA) is equivalent in expressive power with Büchi automata; a transformation is given here.
In formal verification, the model checking method needs to obtain an automaton from a LTL formula that specifies the program property. There are algorithms that translate a LTL formula into a GBA[1] [2] [3] [4] for this purpose. The notion of GBA was introduced specifically for this translation.
Source: https://en.wikipedia.org/wiki/Generalized_B%C3%BCchi_automaton
In formal verification, the model checking method needs to obtain an automaton from a LTL formula that specifies the program property. There are algorithms that translate a LTL formula into a GBA[1] [2] [3] [4] for this purpose. The notion of GBA was introduced specifically for this translation.
Source: https://en.wikipedia.org/wiki/Generalized_B%C3%BCchi_automaton
Software Model Checking
This article is about checking of models in computer science. For the checking of models in statistics, see regression model validation.
In computer science, model checking or property checking refers to the following problem: Given a model of a system, exhaustively and automatically check whether this model meets a given specification. Typically, one has hardware or software systems in mind, whereas the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash. Model checking is a technique for automatically verifying correctness properties of finite-state systems.
In order to solve such a problem algorithmically, both the model of the system and the specification are formulated in some precise mathematical language: To this end, it is formulated as a task in logic, namely to check whether a given structure satisfies a given logical formula. The concept is general and applies to all kinds of logics and suitable structures. A simple model-checking problem is verifying whether a given formula in the propositional logic is satisfied by a given structure.
In computer science, model checking or property checking refers to the following problem: Given a model of a system, exhaustively and automatically check whether this model meets a given specification. Typically, one has hardware or software systems in mind, whereas the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash. Model checking is a technique for automatically verifying correctness properties of finite-state systems.
In order to solve such a problem algorithmically, both the model of the system and the specification are formulated in some precise mathematical language: To this end, it is formulated as a task in logic, namely to check whether a given structure satisfies a given logical formula. The concept is general and applies to all kinds of logics and suitable structures. A simple model-checking problem is verifying whether a given formula in the propositional logic is satisfied by a given structure.