Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: weryfikacja programów

Sortuj według:

Ogranicz wyniki do:

Specification and verification of simple logic control programs using Frama C

Sadolewski J., Świder Z.

Studia Informatica

2011

Vol. 32, nr 3B

21-34

The paper presents an approach to verification process for programs of simple logic controls written in ANSI C. The software is verified with open source tools like Frama C, Jessie and Coq. Process of specification determination and verification whether implementation conforms with specification is demonstrated by several examples, involving combinatorial logic, sequential logic and sequential logic with time constraints.

W artykule zaproponowano proces weryfikacji prostych programów sterowania logicznego napisanych w ANSI C. Programy są weryfikowane przez ogólnodostępne narzędzia, jak Frama C, Jessie i Coq. Proces określania specyfikacji i weryfikacji zgodności specyfikacji z implementacją przedstawiono na kilku przykładach układów kombinacyjnych, sekwencyjnych oraz sekwencyjnych z uzależnieniami czasowymi.

Weryfikacja i synteza programów dla reprogramowalnych sterowników logicznych z wykorzystaniem funkcji monotonicznych i diagramów BDD

Miczulski P.

Pomiary Automatyka Kontrola

2006

R. 52, nr 7 bis

112--114

Artykuł jest podsumowaniem prac badawczych autora w zakresie poszukiwania efektywnych metod projektowania reprogramowalnych sterowników cyfrowych. Opisana metoda weryfikacji behawioralnej i syntezy funkcjonalnej, programów sterowania binarnego, bazuje na autorskiej koncepcji reprezentacji przestrzeni stanów, za pomocą funkcji monotonicznych i hierarchicznych diagramów decyzyjnych. Metoda weryfikacji behawioralnej pozwala na analizę właściwości sieci Petriego, w celu wykrycia wadliwych konstrukcji układu. Wynikiem syntezy funkcjonalnej są równania logiczne opisujące zachowanie układu i dekompozycja współbieżnych algorytmów sterowania binarnego na algorytmy sekwencyjne.

The results of research for the effective methods of designing of reprogrammable logical controllers were presented. The described method of behavioural verification and functional synthesis of binary control programs is based of author's idea of state space representation. The state space is represented by means of monotone logical functions and hierarchical binary decision diagrams. The method of behavioural verification allows, during the analysis of Petri net properties, to find out the incorrect part of a controller specification. As the result of the functional synthesis logical equations are obtained. They define a control behaviour and a decomposition of the concurrent algorithms into sequential algorithms.