id:"swepub:oai:DiVA.org:uu-8605"
Sökning: id:"swepub:oai:DiVA.org:uu-8605" > Verifying Absence o...
- 1 av 1
- Föregående post
- Nästa post
- Till träfflistan
- Saksena, Mayank,1978-Uppsala universitet,Avdelningen för datorteknik,Datorteknik (författare)
Verifying Absence of ∞ Loops in Parameterized Protocols
- BokEngelska2008
Förlag, utgivningsår, omfång ...
- Uppsala :Acta Universitatis Upsaliensis,2008
- 80 s.
- electronicrdacarrier
Nummerbeteckningar
- LIBRIS-ID:oai:DiVA.org:uu-8605
- ISBN:9789155471484
- https://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-8605URI
Kompletterande språkuppgifter
- Språk:engelska
- Sammanfattning på:engelska
Ingår i deldatabas
- SwePubSwePub
Klassifikation
Serie
- Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology,1651-6214 ;419
Anmärkningar
- The complex behavior of computer systems offers many challenges for formal verification. The analysis quickly becomes difficult as the number of participating processes increases. A parameterized system is a family of systems parameterized on a number n, typically representing the number of participating processes. The uniform verification problem — to check whether a property holds for each instance — is an infinite-state problem. The automated analysis of parameterized and infinite-state systems has been the subject of research over the last 15–20 years. Much of the work has focused on safety properties. Progress in verification of liveness properties has been slow, as it is more difficult in general. In this thesis, we consider verification of parameterized and infinite-state systems, with an emphasis on liveness, in the verification framework called regular model checking (RMC). In RMC, states are represented as words, sets of states as regular expressions, and the transition relation as a regular relation. We extend the automata-theoretic approach to RMC. We define a specification logic sufficiently strong to specify systems representable using RMC, and linear temporal logic properties of such systems, and provide an automatic translation from a specification into an analyzable model. We develop acceleration techniques for RMC which allow more uniform and automatic verification than before, with greater power. Using these techniques, we succeed to verify safety and liveness properties of parameterized protocols from the literature. We present a novel reachability based verification method for verification of liveness, in a general setting. We implement the method for RMC, with promising results. Finally, we develop a framework for the verification of dynamic networks based on graph transformation, which generalizes the systems representable in RMC. In this framework we verify the latest version of the DYMO routing protocol, currently being considered for standardization by the IETF.
Ämnesord och genrebeteckningar
- formal methods
- verification
- model checking
- infinite-state systems
- regular model checking
- liveness
- graph transformation
Biuppslag (personer, institutioner, konferenser, titlar ...)
- Jonsson, Bengt (preses)
- Bouajjani, Ahmed,ProfessorLIAFA, Paris (opponent)
- Uppsala universitetAvdelningen för datorteknik (creator_code:org_t)
Internetlänk
Hitta via bibliotek
- Verifying Absence of ∞ Loops in Parameterized Protocols (Sök publikationen i LIBRIS)
Till lärosätets databas
- 1 av 1
- Föregående post
- Nästa post
- Till träfflistan
Hitta mer i SwePub
- Av författaren/redakt...
- Saksena, Mayank, ...
- Jonsson, Bengt
- Bouajjani, Ahmed ...
- Delar i serien
- Digital Comprehe ...
- Av lärosätet
- Uppsala universitet
Sök utanför SwePub
- Sök vidare i:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - Nationella bibliotekssystem
- LIBRIS.kb.se
