Praca dyplomowa dotyczy problemów powstających przy weryfikacji w środowisku COSMA oprogramowania projektowanego w sposób obiektowy . Przedstawia techniki redukcji wielkości grafu stanów osiągalnych bazującej na abstrakcji zmiennych w systemie. Pokazuje sposób zadawania wymagań co do poprawności zachowań systemu poprzez diagramy sekwencji. Działanie obu technik (oraz oprogramowania implmentującego te techniki) zilustrowane jest przykładami.

This thesis deals with problems involved in verification of object- oriented software by the model-checking in the COSMA environment. Two techniques are proposed: one for reduction of Reachability Graph (based on abtraction of variables in designed system), the other for the specification of system requirements using a version of Message Sequence Charts. Both techniques are supported by software tools designed and implemented as a part of diploma project.