Automatized Data Abstraction
| Název práce v češtině: | Automatized Data Abstraction |
|---|---|
| Název v anglickém jazyce: | Automatized Data Abstraction |
| Akademický rok vypsání: | 2005/2006 |
| Typ práce: | diplomová práce |
| Jazyk práce: | angličtina |
| Ústav: | Katedra softwarového inženýrství (32-KSI) |
| Vedoucí / školitel: | doc. RNDr. Jan Kofroň, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 11.11.2005 |
| Datum zadání: | 11.11.2005 |
| Datum a čas obhajoby: | 21.05.2007 00:00 |
| Datum odevzdání elektronické podoby: | 21.05.2007 |
| Datum proběhlé obhajoby: | 21.05.2007 |
| Oponenti: | RNDr. Jiří Adámek, Ph.D. |
| Zásady pro vypracování |
| Model checking is a process of checking for validity of a property within a transition system. In recent years, as the power of computational system has increased, the software model checking has become an interesting issue. Most model checking techniques are based on an exhaustive state space traversal to check the property validity in all states of the system. In most cases, however, the software piece being model checked yields a too large state space that is impossible to traverse in a reasonable time. This is caused mainly because of software parallelism (multi threading) and large data domains. As the parallelism may in principle be inevitable due to the software nature, a way to enable for software model checking is to focus on reducing data domains' sizes.
Reducing the state space size can be achieved via replacing original data types of some application variables by abstract types. Values of original data types are then mapped to the abstract types' values. In most cases, the resulting application state space may be several orders of magnitude smaller. Even though it is obviously impossible to devise the best (in a sense of resulting state space size) data types' abstraction and the variable types' mapping in an automatized way, providing a list of variables with a suggested (not necessarily final) mapping to abstract types may be also of much help for a developer mapping the variable types by hand. Therefore, the goals of thesis are: * Finding methods for determining what variables are a subject for data type abstraction * Finding methods for automatized/semi-automatized mapping of program variable types to abstract data types * Evaluation of proposed methods' usability on programs featuring multiple threads, synchronization mechanisms, ... The proposed methods should be general and programming language independent, however, the Java programming language [1] is supposed to be taken as the default one. |
| Seznam odborné literatury |
| [1] Java programming language - http://java.sun.com
[2] The SLAM project - http://research.microsoft.com/slam [3] The Bandera project - http://bandera.projects.cis.ksu.edu |