|
|
Nástroj pro generování testovacích cest dle zadaného kritéria
Bíl, Jan ; Rogalewicz, Adam (oponent) ; Smrčka, Aleš (vedoucí práce)
Automatické generování testovacích vstupů dle zadaného kritéria pokrytí má potenciál ušetřit velkou část nákladů při vývoji kritických aplikací. V rámci této práce byl navržen a naimplementován nástroj, který postupně generuje cesty grafem toku řízení odpovídající funkcím takové aplikace, které splňují zadané kritérium pokrytí. Tyto cesty převádí na odpovídající SMT (Satisfiability Modulo Theories) formuli pro kterou se ověří její sémantická splnitelnost SMT řešičem Z3. Pro sémanticky splnitelné cesty je zároveň vygenerováno ohodnocení vstupů, pro které formule platí. Tato ohodnocení dohromady tvoří sadu testovacích vstupů splňující zadané kritérium pokrytí. Tyto testovací vstupy jsou hodnoty parametrů testované funkce a stavu globálních proměnných.
|
|
|
Novel Methods for Semi-Quantitative Analysis of Biochemical Systems
Bíl, Jan ; Andriushchenko, Roman (oponent) ; Češka, Milan (vedoucí práce)
This thesis aims on providing novel methods for analysis of stochastic bio-chemical systems. It introduces a new population abstraction based on dirac semi-Markov processes. It turned out, that this abstraction is more precise than Continuous time Markov chain abstraction. On this abstraction, analysis methods are provided. Algorithm for transient analysis over this abstraction is described and also novel timed temporal logic formulas, that allow to express interesting biological properties are presented. Further, model-checking algorithm for these formulas is proposed and implemented. Preliminary experiments showing potential of this approach are also described.
|
|
|
Novel Methods for Semi-Quantitative Analysis of Biochemical Systems
Bíl, Jan ; Andriushchenko, Roman (oponent) ; Češka, Milan (vedoucí práce)
This thesis aims on providing novel methods for analysis of stochastic bio-chemical systems. It introduces a new population abstraction based on dirac semi-Markov processes. It turned out, that this abstraction is more precise than Continuous time Markov chain abstraction. On this abstraction, analysis methods are provided. Algorithm for transient analysis over this abstraction is described and also novel timed temporal logic formulas, that allow to express interesting biological properties are presented. Further, model-checking algorithm for these formulas is proposed and implemented. Preliminary experiments showing potential of this approach are also described.
|
host ::
RSS.