Thesis

This thesis deals with problems involved in verification of Object Oriented Programming software by the model-checking in the COSMA. In few words we attempt to check a program against formal requirements without runing one. The process is performed by checking formal requirements in generated RG (Reachability Graph). RG consists of all possible states of program - bad states and paths can be easily found. If there's no errant states we can say the system holds all the requirements we've cheked.

Of course this method has it's own disadvantages - verified system has to be presented by automatons using special formalism: CSM. RG gets bigger when complexity of the problem raises. One of tasks realised in thesis is to reduce RG.

  • Thesis in polish (html)
  • Thesis in polish, one page (html)
  • Program model_danych (ZIP, C++ source, Windows binary)

This image shows graphic representation of automatons I'm working on. Squares are states, arrows are transitions between states, labels written near arrows are boolean conditions. When condition in given state becomes true, actual state can be changed. Inside sqares there are names of state (above line) and list of generated signals (below). Simple, is't it ?

(...) Nie ma bowiem łatwych odpowiedzi. Nie istnieje nic takiego jak najlepsze rozwiązanie - zarówno jeśli chodzi o narzędzia, jak i języki czy systemy operacyjne. Są jedynie systemy, które mogą być bardziej odpowiednie w konkretnych okolicznościach.

I tu właśnie do gry wchodzi pragmatyzm. Nie należy przywiązywać się do żadnej określonej metody, ale mieć na tyle rozległą wiedzę i doświadczenie, by w danej sytuacji wybrać dobre rozwiązanie. (...)

Andrew Hunt, David Thomas "Pragmatyczny Programista"