Repository logo

Browsing by Subject "weryfikacja oprogramowania"

Filter results by typing the first few letters
Now showing 1 - 2 of 2
  • thumbnail.journal.alt
    Item type:Article, Access status: Open Access ,
    Zastosowanie języka LOTOS do modelowania wybranych struktur metody HOOD
    (2006) Brzuchacz, Rafał
    W pracy zaprezentowano możliwości użycia języka LOTOS [3, 7] w projektowaniu oprogramowania systemów czasu rzeczywistego metodą HOOD [6, 13]. Wybrane struktury HOOD zostają wyrażone w języku algebry procesów i abstrakcyjnych typów danych, co zapewnia możliwość formalnej analizy tworzonego projektu. We wprowa­dzeniu do pracy wyjaśniono cel i motywacje do tworzenia modelu formalnego projektu systemu czasu rzeczywistego. Następnie przedstawiono skrócony opis metodyki hierarchicznego projektowania HOOD, której notacja i proces projektowy stanowią bazę dla proponowanej metody formalizacji. Wyjaśniono znaczenie takich konstrukcji, jak moduł, interfejs, operacja, hierarchia użycia i zawierania. W kolejnym punkcie, po krótkim przedstawieniu języka LOTOS [3, 7], zaprezentowano technikę, w której konstrukcje metody HOOD zostają zinterpretowane w języku formalnym algebry procesów i abstrakcyjnych typów danych. Opis przeprowadzony jest dla prostego przykładu projektu w HOOD, celem wyjaśnienia istoty interpretacji. W części końcowej pracy podano wnioski wraz ze wska­zaniem dalszych możliwych kierunków rozwoju i zastosowań prezentowanej metody.
  • thumbnail.journal.alt
    Item type:Doctoral Dissertation, Access status: Open Access ,
    Zastosowanie metod formalnych do specyfikacji oraz weryfikacji systemów agentowych
    (Data obrony: 2012) Maludziński, Sławomir P.
    Wydział Elektrotechniki, Automatyki, Informatyki i Elektroniki
    The above dissertation proves the thesis that using formal methods of specification and verification lets to create correct multi-agent systems. The thesis formulated domains that can currently be analysed using formal methods such as environment, resources, communication, operation, functional integration and those which are beyond formal specification and verification. The analysis let to design and implement an automatic tool that can be used to specify and verify such systems. The tool uses join-calculus algebra and model checking using CTL temporal logic to prove correctness. The thesis contains description of the design, implementation and examples of using the tool.