Original title: Fighting the State Explosion Problem in Component Protocols
Translated title: Fighting the State Explosion Problem in Component Protocols
Authors: Holub, Viliam ; Plášil, František (advisor) ; Brada, Přemysl (referee) ; Reussner, Ralf H. (referee)
Document type: Doctoral theses
Year: 2007
Language: eng
Abstract: In complex software component systems, it is desirable to verify the correctness of the composition before deployment. To achieve a trustworthy composition, the behavior of components is formally described and the composition is veri ed against communication errors. Unfortunately, the number of states of a model tends to grow exponentially with the size of the model's description | the state explosion problem. Because the exhaustive veri cation has to visit all the states of the model, the veri cation leads to unacceptable space and time requirements. In this thesis, we present several approaches to cope with the state explosion problem in behavior protocols. First, we reduce a size of the speci cation by enhancing the speci cation language by exceptions and, additionally, we reduce the speci cation by symbolic manipulations with respect to composition. Then, we present a novel approach to distributed veri cation, which involves external storage devices. Finally, we reduce the number of states, which have to be traversed by identifying representatives in the state space.

Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/13670

Permalink: http://www.nusl.cz/ntk/nusl-289587


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Doctoral theses