WFRF:(Santos C. N.)
Sökning: WFRF:(Santos C. N.) > (2000-2004) > New Directions in S...
- d'Orso, Julien,1975-Uppsala universitet,Avdelningen för datorteknik,Datorteknik (författare)
New Directions in Symbolic Model Checking
- BokEngelska2003
Förlag, utgivningsår, omfång ...
- Uppsala :Acta Universitatis Upsaliensis,2003
- 138 s.
- electronicrdacarrier
Nummerbeteckningar
- LIBRIS-ID:oai:DiVA.org:uu-3753
- ISBN:9155457819
- https://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-3753URI
Kompletterande språkuppgifter
- Språk:engelska
- Sammanfattning på:engelska
Ingår i deldatabas
- SwePubSwePub
Klassifikation
Serie
- Uppsala Dissertations from the Faculty of Science and Technology,1104-2516 ;50
Anmärkningar
- In today's computer engineering, requirements for generally high reliability have pushed the notion of testing to its limits. Many disciplines are moving, or have already moved, to more formal methods to ensure correctness. This is done by comparing the behavior of the system as it is implemented against a set of requirements. The ultimate goal is to create methods and tools that are able to perform this kind of verfication automatically: this is called Model Checking. Although the notion of model checking has existed for two decades, adoption by the industry has been hampered by its poor applicability to complex systems. During the 90's, researchers have introduced an approach to cope with large (even infinite) state spaces: Symbolic Model Checking. The key notion is to represent large (possibly infinite) sets of states by a small formula (as opposed to enumerating all members). In this thesis, we investigate applying symbolic methods to different types of systems: Parameterized systems. We work whithin the framework of Regular Model Chacking. In regular model checking, we represent a global state as a word over a finite alphabet. A transition relation is represented by a regular length-preserving transducer. An important operation is the so-called transitive closure, which characterizes composing a transition relation with itself an arbitrary number of times. Since completeness cannot be achieved, we propose methods of computing closures that work as often as possible. Games on infinite structures. Infinite-state systems for which the transition relation is monotonic with respect to a well quasi-ordering on states can be analyzed. We lift the framework of well quasi-ordered domains toward games. We show that monotonic games are in general undecidable. We identify a subclass of monotonic games: downward-closed games. We propose an algorithm to analyze such games with a winning condition expressed as a safety property. Probabilistic systems. We present a framework for the quantitative analysis of probabilistic systems with an infinite state-space: given an initial state sinit, a set F of final states, and a rational Θ > 0, compute a rational ρ such that the probability of reaching F form sinit is between ρ and ρ + Θ. We present a generic algorithm and sufficient conditions for termination.
Ämnesord och genrebeteckningar
- NATURVETENSKAP Data- och informationsvetenskap hsv//swe
- NATURAL SCIENCES Computer and Information Sciences hsv//eng
- Informatics
- computer and systems science
- Informatik
- data- och systemvetenskap
- Informatics, computer and systems science
- Informatik, data- och systemvetenskap
Biuppslag (personer, institutioner, konferenser, titlar ...)
- Abulla, Parosh (preses)
- Lakhnech, Yassine,professorVerimag, Grenoble (opponent)
- Uppsala universitetAvdelningen för datorteknik (creator_code:org_t)
Internetlänk
Hitta via bibliotek
- New Directions in Symbolic Model Checking (Sök publikationen i LIBRIS)
Till lärosätets databas
Hitta mer i SwePub
- Av författaren/redakt...
- d'Orso, Julien, ...
- Abulla, Parosh
- Lakhnech, Yassin ...
- Om ämnet
-
- NATURVETENSKAP
- NATURVETENSKAP
- och Data och informa ...
- Delar i serien
- Uppsala Disserta ...
- 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
