Verification of Timed Automata by CEGAR-Based Algorithms. Farkas, R. 2016. Master's Thesis, Budapest University of Technology and Economics![Verification of Timed Automata by CEGAR-Based Algorithms [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Pdf ![Verification of Timed Automata by CEGAR-Based Algorithms [link]](https://bibbase.org/img/filetypes/link.svg "link")
Link abstract bibtex Nowadays safety-critical systems are becoming increasingly prevalent, however, faults in their behaviour can lead to serious damage. Therefore, it is extremely important to use mathematically precise verification techniques during their development. One of them is formal verification, that is able to find design problems from early phases of the development. However, the complexity of safety-critical systems often prevents successful verification. This is particularly true for real-time systems: the set of possible states and transitions can be large or infinite, even for small timed systems. Thus, selecting appropriate modelling formalisms and efficient verification algorithms is very important. One of the most common formalisms for describing timed systems is the timed automaton that extends finite automata with clock variables to represent the elapse of time. When applying formal verification, reachability becomes an important aspect – that is, examining whether the system can reach a given erroneous state during its execution. The complexity of the problem is exponential even for simple timed automata (without discrete variables), thus it can rarely be solved for large models. A possible solution to overcome this deficiency is to use abstraction, which simplifies the problem to be solved by focusing on the relevant information. However, the main difficulty when applying abstraction-based techniques is finding the appropriate precision, which is coarse enough to reduce complexity but fine enough to be able to solve the problem. Counterexample-guided abstraction refinement (CEGAR) is an iterative method starting from a coarse abstraction and refining it until a sufficient precision is reached. The goal of my work is to develop efficient algorithms for the verification of timed automata. In my work I examine and develop CEGAR-based reachability algorithms applied to timed automata and I integrate them to a common framework where components of different algorithms are combined to form new and efficient verification methods. The framework offers two realizations of the CEGAR approach: one of them applies abstraction to the automaton in order to gain an overapproximation of the set of reachable states (the state space), and the other applies abstraction directly to the state space. I demonstrate the efficiency of the developed algorithms by measurements on examples that are commonly used to benchmark model checking algorithms for timed automata.
@misc{farkasrMsc2016,
author = {Farkas, Rebeka},
title = {Verification of Timed Automata by CEGAR-Based Algorithms},
note = {Master's Thesis, Budapest University of Technology and Economics},
year = {2016},
type = {Thesis},
url_pdf = {farkasrMsc2016.pdf},
url_link = {http://diplomaterv.vik.bme.hu/en/Theses/Idozitett-rendszerek-CEGAR-alapu-analizise},
abstract = {Nowadays safety-critical systems are becoming increasingly prevalent, however, faults in their behaviour can lead to serious damage. Therefore, it is extremely important to use mathematically precise verification techniques during their development. One of them is formal verification, that is able to find design problems from early phases of the development. However, the complexity of safety-critical systems often prevents successful verification. This is particularly true for real-time systems: the set of possible states and transitions can be large or infinite, even for small timed systems. Thus, selecting appropriate modelling formalisms and efficient verification algorithms is very important. One of the most common formalisms for describing timed systems is the timed automaton that extends finite automata with clock variables to represent the elapse of time. When applying formal verification, reachability becomes an important aspect – that is, examining whether the system can reach a given erroneous state during its execution. The complexity of the problem is exponential even for simple timed automata (without discrete variables), thus it can rarely be solved for large models. A possible solution to overcome this deficiency is to use abstraction, which simplifies the problem to be solved by focusing on the relevant information. However, the main difficulty when applying abstraction-based techniques is finding the appropriate precision, which is coarse enough to reduce complexity but fine enough to be able to solve the problem. Counterexample-guided abstraction refinement (CEGAR) is an iterative method starting from a coarse abstraction and refining it until a sufficient precision is reached. The goal of my work is to develop efficient algorithms for the verification of timed automata. In my work I examine and develop CEGAR-based reachability algorithms applied to timed automata and I integrate them to a common framework where components of different algorithms are combined to form new and efficient verification methods. The framework offers two realizations of the CEGAR approach: one of them applies abstraction to the automaton in order to gain an overapproximation of the set of reachable states (the state space), and the other applies abstraction directly to the state space. I demonstrate the efficiency of the developed algorithms by measurements on examples that are commonly used to benchmark model checking algorithms for timed automata.},
}
Downloads: 0
{"_id":"727svnzsjSYdfNHFC","bibbaseid":"farkas-verificationoftimedautomatabycegarbasedalgorithms-2016","downloads":0,"creationDate":"2017-01-03T21:45:57.335Z","title":"Verification of Timed Automata by CEGAR-Based Algorithms","author_short":["Farkas, R."],"year":2016,"bibtype":"misc","biburl":"https://ftsrg.mit.bme.hu/theta/publications/publications.bib","bibdata":{"bibtype":"misc","type":"Thesis","author":[{"propositions":[],"lastnames":["Farkas"],"firstnames":["Rebeka"],"suffixes":[]}],"title":"Verification of Timed Automata by CEGAR-Based Algorithms","note":"Master's Thesis, Budapest University of Technology and Economics","year":"2016","url_pdf":"farkasrMsc2016.pdf","url_link":"http://diplomaterv.vik.bme.hu/en/Theses/Idozitett-rendszerek-CEGAR-alapu-analizise","abstract":"Nowadays safety-critical systems are becoming increasingly prevalent, however, faults in their behaviour can lead to serious damage. Therefore, it is extremely important to use mathematically precise verification techniques during their development. One of them is formal verification, that is able to find design problems from early phases of the development. However, the complexity of safety-critical systems often prevents successful verification. This is particularly true for real-time systems: the set of possible states and transitions can be large or infinite, even for small timed systems. Thus, selecting appropriate modelling formalisms and efficient verification algorithms is very important. One of the most common formalisms for describing timed systems is the timed automaton that extends finite automata with clock variables to represent the elapse of time. When applying formal verification, reachability becomes an important aspect – that is, examining whether the system can reach a given erroneous state during its execution. The complexity of the problem is exponential even for simple timed automata (without discrete variables), thus it can rarely be solved for large models. A possible solution to overcome this deficiency is to use abstraction, which simplifies the problem to be solved by focusing on the relevant information. However, the main difficulty when applying abstraction-based techniques is finding the appropriate precision, which is coarse enough to reduce complexity but fine enough to be able to solve the problem. Counterexample-guided abstraction refinement (CEGAR) is an iterative method starting from a coarse abstraction and refining it until a sufficient precision is reached. The goal of my work is to develop efficient algorithms for the verification of timed automata. In my work I examine and develop CEGAR-based reachability algorithms applied to timed automata and I integrate them to a common framework where components of different algorithms are combined to form new and efficient verification methods. The framework offers two realizations of the CEGAR approach: one of them applies abstraction to the automaton in order to gain an overapproximation of the set of reachable states (the state space), and the other applies abstraction directly to the state space. I demonstrate the efficiency of the developed algorithms by measurements on examples that are commonly used to benchmark model checking algorithms for timed automata.","bibtex":"@misc{farkasrMsc2016,\n author = {Farkas, Rebeka},\n title = {Verification of Timed Automata by CEGAR-Based Algorithms},\n note = {Master's Thesis, Budapest University of Technology and Economics},\n year = {2016},\n type = {Thesis},\n url_pdf = {farkasrMsc2016.pdf},\n url_link = {http://diplomaterv.vik.bme.hu/en/Theses/Idozitett-rendszerek-CEGAR-alapu-analizise},\n \n abstract = {Nowadays safety-critical systems are becoming increasingly prevalent, however, faults in their behaviour can lead to serious damage. Therefore, it is extremely important to use mathematically precise verification techniques during their development. One of them is formal verification, that is able to find design problems from early phases of the development. However, the complexity of safety-critical systems often prevents successful verification. This is particularly true for real-time systems: the set of possible states and transitions can be large or infinite, even for small timed systems. Thus, selecting appropriate modelling formalisms and efficient verification algorithms is very important. One of the most common formalisms for describing timed systems is the timed automaton that extends finite automata with clock variables to represent the elapse of time. When applying formal verification, reachability becomes an important aspect – that is, examining whether the system can reach a given erroneous state during its execution. The complexity of the problem is exponential even for simple timed automata (without discrete variables), thus it can rarely be solved for large models. A possible solution to overcome this deficiency is to use abstraction, which simplifies the problem to be solved by focusing on the relevant information. However, the main difficulty when applying abstraction-based techniques is finding the appropriate precision, which is coarse enough to reduce complexity but fine enough to be able to solve the problem. Counterexample-guided abstraction refinement (CEGAR) is an iterative method starting from a coarse abstraction and refining it until a sufficient precision is reached. The goal of my work is to develop efficient algorithms for the verification of timed automata. In my work I examine and develop CEGAR-based reachability algorithms applied to timed automata and I integrate them to a common framework where components of different algorithms are combined to form new and efficient verification methods. The framework offers two realizations of the CEGAR approach: one of them applies abstraction to the automaton in order to gain an overapproximation of the set of reachable states (the state space), and the other applies abstraction directly to the state space. I demonstrate the efficiency of the developed algorithms by measurements on examples that are commonly used to benchmark model checking algorithms for timed automata.},\n}\n\n","author_short":["Farkas, R."],"key":"farkasrMsc2016","id":"farkasrMsc2016","bibbaseid":"farkas-verificationoftimedautomatabycegarbasedalgorithms-2016","role":"author","urls":{" pdf":"https://ftsrg.mit.bme.hu/theta/publications/farkasrMsc2016.pdf"," link":"http://diplomaterv.vik.bme.hu/en/Theses/Idozitett-rendszerek-CEGAR-alapu-analizise"},"metadata":{"authorlinks":{}},"downloads":0},"search_terms":["verification","timed","automata","cegar","based","algorithms","farkas"],"keywords":[],"authorIDs":[],"dataSources":["7MDizr2BZojXoNdPN"]}