"S" . "RIV/68407700:21340/13:00210799!RIV14-MSM-21340___" . "Configuration Dynamics Verification Using UPPAAL" . "Configuration Dynamics Verification Using UPPAAL"@en . "21340" . . . "1"^^ . "1"^^ . . "[8BEF0A751BB3]" . "Praha" . "Configuration Dynamics Verification Using UPPAAL"@en . "Praha" . "2013-11-15+01:00"^^ . "software; configuration; hierarchy; model; verification; UPPAAL"@en . "Software applications become more and more complicated, nowadays. The complexity of the internal dynamics of a modern software application can be hard to maintain. Software configuration is one of the areas where the internal dynamics can become very complicated because there usually exists a huge amount of states that the system can be in. Of course, implementation of configuration tools is a hard task, especially in imperative-style languages, since the programmer must take into consideration all special combinations of states and implement the appropriate behavior of the program for all of them. It is very easy to make a mistake or to omit a special condition in such a code. There are two ways to solve this problem. One is to use declarative programming which is suitable for these classes of problems~(but the programmer must be familiar with an unusual approach of this style of programming) or to use system verifiers to check whether the application behaves correctly under all circumstances. In [1], a multi-platform configuration tool Freeconf is described. This tool has different types of configuration keys and for each key it uses an extra set of Boolean properties that extend the semantics of the key [2]. The development of values of these semantic properties is highly dynamic since the values change according to the user's actions and one change usually propagates further and induce more changes. Freeconf in its core implements this dynamic behavior in Python. The code is not very maintainable since it is complex and adding more properties or changing some rules of propagation is particularly non-trivial. In [1], attempts have been made to abstract away from Freeconf and design a formalism that would allow us to describe the general dynamic processes in a compact way and to be able to verify whether the implementation is sound and the model itself does not have any deadlocks." . . . . . "66706" . . . "\u010Cesk\u00E1 technika - nakladatelstv\u00ED \u010CVUT" . . "Software applications become more and more complicated, nowadays. The complexity of the internal dynamics of a modern software application can be hard to maintain. Software configuration is one of the areas where the internal dynamics can become very complicated because there usually exists a huge amount of states that the system can be in. Of course, implementation of configuration tools is a hard task, especially in imperative-style languages, since the programmer must take into consideration all special combinations of states and implement the appropriate behavior of the program for all of them. It is very easy to make a mistake or to omit a special condition in such a code. There are two ways to solve this problem. One is to use declarative programming which is suitable for these classes of problems~(but the programmer must be familiar with an unusual approach of this style of programming) or to use system verifiers to check whether the application behaves correctly under all circumstances. In [1], a multi-platform configuration tool Freeconf is described. This tool has different types of configuration keys and for each key it uses an extra set of Boolean properties that extend the semantics of the key [2]. The development of values of these semantic properties is highly dynamic since the values change according to the user's actions and one change usually propagates further and induce more changes. Freeconf in its core implements this dynamic behavior in Python. The code is not very maintainable since it is complex and adding more properties or changing some rules of propagation is particularly non-trivial. In [1], attempts have been made to abstract away from Freeconf and design a formalism that would allow us to describe the general dynamic processes in a compact way and to be able to verify whether the implementation is sound and the model itself does not have any deadlocks."@en . "RIV/68407700:21340/13:00210799" . . . . "Fabian, David" . . . "Doktorandsk\u00E9 dny 2013" . . "Configuration Dynamics Verification Using UPPAAL" . . . . "2"^^ . "978-80-01-05379-9" .