Zastosowanie paradygmatu funkcyjnego do formalnej analizy systemów
modelowanych w języku Alvis
Język Alvis powstał w wyniku poszukiwań formalnego języka modelowania, który będzie łatwy w użytkowaniu dla inżynierów oprogramowania. Celem rozprawy było zaproponowanie i implementacja alternatywnego podejścia do analizy, umożliwiającego skuteczną formalną weryfikację modeli Alvis w oparciu o stany, wykorzystując postać pośrednią modelu w języku Haskell. Postawiono założenie, że proponowane podejście powinno umożliwiać analizę modeli o liczbie stanów przekraczającej 106, na sprzęcie dostępnym dla przeciętnego inżyniera
w akceptowalnym przedziale czasu. Ponadto w ramach pracy miał zostać opracowany język zapytań umożliwiający intuicyjną weryfikację wybranych własności modeli, bez konieczności znajomości wewnętrznej reprezentacji modelu czy języka Haskell. Cele te zostały zrealizowane poprzez opracowanie i implementację języka zapytań Alvis Query Language, umożliwiającego weryfikację modelu operując na postaci IHR. Dodatkowo zaproponowane zostało komplementarne podejście do weryfikacji modeli w narzędziu nuXmv oraz rozszerzenie możliwości weryfikacji obu podejść, poprzez wykorzystanie chmur obliczeniowych. Rozprawa zawiera także studium przypadków formalnej weryfikacji modeli systemów współbieżnych i czasu rzeczywistego. Na podstawie pomiarów zebranych podczas weryfikacji tych modeli przygotowana została analiza porównawcza opracowanych metod.
Alvis language was created in an attempt to find a formal modelling language that would be easy to use for software engineers. The main goal of this dissertation was to propose and implement an alternative approach to the analysis, enabling to effectively and formally verify Alvis models incorporating information carried originally in states representation with the use of intermediate Haskell representation. It was assumed that the presented approach should be able to analyse models containing over 106
states on a standard personal computer in an acceptable amount of time. Moreover, a dedicated query language should be defined, enabling intuitive verification of selected subset of model properties without advanced knowledge of internal representation of the model or Haskell programming skills. These goals were met through the definition and implementation of Alvis Query Language, enabling to verify models using their Haskell representation. Additionally, the dissertation presents a complementary approach to model verification using nuXmv tool and a process of enhancing both methods through the usage of cloud computing. The dissertation also contains a few case studies of formal verification of concurrent and real-time systems. The measurements collected during the verification process are used to provide a comparative analysis of the presented methods.
