Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: asystent dowodzenia

Sortuj według:

Ogranicz wyniki do:

Wprowadzenie do weryfikacji prostych programów w języku ST za pomocą narzędzi Coq, Why i Caduceus

Sadolewski J.

Metody Informatyki Stosowanej

2009

nr 2 (19)

121-138

Przedstawiono metodę przeprowadzania dowodów poprawności prostych programów sterowania napisanych w języku ST w środowisku Coq. Wykorzystano w tym celu dwa pomocnicze narzędzia Why i Caduceus należące do wspólnego projektu Proval. Metoda polega na ręcznej konwersji programu sterowania zapisanego w języku ST za pomocą przedstawionych reguł do równoważnej postaci w ANSI C. Ze względu na prostotę ST i podobieństwo do ANSI C nie powinno stanowić to problemu. Postać tę uzupełnia się o specyfikację wejść i wyjść a następnie poddaje automatycznym transformacjom programami Caduceus i Why. Program Why generuje lematy, które należy udowodnić, aby wykazać poprawność realizacji. Przedstawione reguły konwersji z języka ST do ANSI C stosuje się do przekształcania prostych bloków funkcjonalnych i programów. Zastosowanie niektórych reguł prowadzi do ograniczeń w liczbie instancji bloków, co jest wadą zaproponowanego rozwiązania. Wśród pozytywnych cech prezentowanych reguł wyróżnić można przejrzysty zapis specyfikacji i łatwość przeprowadzania dowodów w podobnych przypadkach.

Based on three simple examples, the paper introduces into verification technique of control programs by means of Coq, Why and Caduceus tools developed in France. The examples involve binary multiplexer, RS fillip-flop and a Start-Stop circuit composed of theflip-flop and a gale. The programs to be verified are written in ST language (Structured Text) of lEC 61131-3 standard. The approach consists of four basic steps. First the original ST program is converted into ANSI C to be handled by Caduceus. This in turn converts the ANSI C into a code interpreted by Why. Coq is a proof assistant for verificaton of conditions generated by Why. Conversions and proofs for each of the examples are presented in details, together with trees involving tactics applied for verification. Based on these, some recommendations and hints how to handle problems of similar classes are given.