Synteza i weryfikacja algorytmów konwersji protokołów komunikacyjnych w polowych magistralach rozgłoszeniowych

Abstract

The subject of the thesis is to develop a methodology for synthesis and automated verification of conversion alaorithms for fieldbus communication Drotocols. Broadcast and master-slave Communications are considered. The synthesis is based on selection of suitable conversion technique, depending on communication mechanisms. It is based on successive enlargement of the set of functions that together constitute the algorithm, until the verification produces satisfactory results. Specifications of master-slave and broadcast protocols and their conversion algorithms are developed using MTL temporal logic. Liveness and safety conditions are formulated for verification with compositional method. PVS {Prototype Verification System) software is employed for automated verification. A verification scheme involving a prover module from PVS system is developed. A study of broadcast-to-master/slave and master/slave-to-master/slave conversion algorithms is presented, taking standard Modbus and CANopen, and proprietary CANpsw protocols as examples. The methodology proposed has been used for development of CANpsw-Modbus converter prototype, that operates with short cycle while transferring data for logic control and with longer cycle for continuous regulation.

Przedmiotem pracy było opracowanie metodyki dla syntezy i zautomatyzowanej weryfikacji algorytmów konwersji protokołów komunikacyjnych magistral polowych. Rozpatrywano komunikację typu rozgłoszeniowego (broadcasi) i nadrzędnego (master-slave). Syntezę oparto na wyborze odpowiedniej techniki konwersji w zależności od mechanizmów komunikacyjnych. Polega ona na sukcesywnym rozbudowywaniu zbioru funkcji składających się na algorytm, dopóki weryfikacja nie da pozytywnego wyniku. Opracowano specyfikacje wybranych nadrzędnych i rozgłoszeniowych protokołów oraz ich algorytmów konwersji wykorzystując logikę temporalną MTL. Sformułowano warunki żywotności i bezpieczeństwa, które posłużyły do weryfikacji metodą kompozycyjną. Jako narzędzie automatycznej weryfikacji wykorzystano oprogramowanie PVS (Prototype Verification System). Opracowano schemat weryfikacji za pomocą modułu prover systemu PVS. Przeprowadzono studium algorytmów konwersji protokołów rozgłoszeniowego-na-nadrzędny i nadrzędny-na-nadrzędny na przykładzie standardowych protokołów Modbus i CANopen oraz specjalizowanego CANpsw. Proponowaną metodykę zastosowano przy tworzeniu prototypu konwertera CANpsw-Modbus uwzględniającego krótki cykl przekazywania danych do sterowania logicznego i dłuższy dla regulacji ciągłej.