Poniższa dysertacja stawia oraz dowodzi tezę, iż objęcie metodami formalnymi specyfikacji oraz weryfikacji szczególnych aspektów systemów agentowych wspomaga wytwarzanie poprawnych systemów tej klasy. W celu wykazania tezy określono obszary aktualnie objęte metodami formalnymi specyfikacji i weryfikacji takimi jak środowisko, zasoby, komunikację, działanie czy integralność w ujęciu funkcjonalnym. Przegląd ten pozwolił na sporządzenie projektu oraz implementacji narzędzia wykorzystującego metody formalne do specyfikacji oraz dowodzenia poprawności systemów agentowych. Do specyfikacji używana jest algebra procesów join-calculus a weryfikacja obywa się z wykorzystaniem weryfikacji modelowej gdzie własności poprawności definiowane są przez logikę temporalną CTL. W pracy zawarto opis projektu, implementacji oraz przykładowe rezultaty osiągnięte dzięki użyciu narzędzia.
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.
