WERYFIKACJA MODELOWA STEROWNIKÓW LOGICZNYCH

Specyfikacja sterownika logicznego jest pierwszym etapem w procesie jego projektowania oraz tworzenia. Niezmiernie ważne jest zatem, aby spełniała wymagania stawiane jej przez przyszłego użytkownika. Specyfikacja może zostać formalnie zapisana w różnych postaciach, na przykład przy wykorzystaniu algorytmicznych maszyn stanów, sieci Petriego, czy też diagramów czynności lub maszyn stanów języka UML 2.x. Wymagania ze strony rynku dotyczące jakości sprzętu są zazwyczaj wyższe niż te dotyczące oprogramowania.
Formalna weryfikacja przygotowanej specyfikacji (jej walidacja) pozwala na wczesne wykrycie błędów wynikających z nieprawidłowej interpretacji specyfikacji. Jedną z metod, oprócz innych, jak na przykład automatycznego dowodzenia twierdzeń (ang. theorem proving), jest technika weryfikacji modelowej (ang. model checking) która pozwala na automatyczną weryfikację behawioralnej specyfikacji systemu przy wykorzystaniu narzędzi komputerowego wnioskowania (narzędzia typu model checker). Jest ona stosowana do weryfikacji systemów związanych z oprogramowaniem oraz ze sprzętem. Weryfikacja jest przeprowadzana automatycznie przez narzędzia wnioskowania komputerowego.
Autorka skupia się głównie na weryfikacji formalnej specyfikacji rekonfigurowalnych sterowników logicznych przedstawionej w postaci interpretowanych sieci Petriego sterowania. Uwzględnione są także pewne aspekty związane z syntezą sterowników logicznych, które pozwalają na zachowanie spójności pomiędzy modelem syntezowalnym a modelem podlegającym weryfikacji. Interpretowane sieci Petriego sterowania (oraz dodatkowo algorytmiczne maszyny stanów ASM są wykorzystywane jako formalna postać specyfikacji osadzonego sterownika logicznego. Język logiki temporalnej jest wykorzystywany do określenia wymagań behawioralnych stawianych projektowanemu sterownikowi logicznemu, a więc do podania wymagań, jakie powinny być spełnione w utworzonej specyfikacji. Formalna weryfikacja modelowa wykorzystująca aparat logiki temporalnej, jest stosowana w celu sprawdzenia sporządzonej specyfikacji systemu pod kątem stawianych mu wymagań.