Ing. Richard Šusta, Ph.D.

The paper deals with automatic testing of programmable logical controller (PLC) programs in a distant education. Students control a physical model, which that has also its virtual counterpart. While one user is connected to the physical model, others debug programs with the aid of the virtual model. We discuss the structure of models, the organization of education, and the testing process of student's programs. Finally, we present a new theory of delta-graphs used for conversion programs into a timed abstraction of PLC suitable for testing, as the main contribution of this paper.

The paper treats a simple SISO control tool that uses classical nonlinear controllers. Description of basic functions and programs and several examples of their use comprise the main part of the paper. The tool forms part of bigger system programmed in C++ and C# for industrial use. The MATLAB models of the control software and controller adjustment algorithms are freely available on the Czech Technical University web pages.

The paper outlines our experience with combined educational exercises consisting of virtual and physical parts and they are suitable for training courses of low cost programmable logical controllers (PLCs). First of all, we introduce our training approach based on utilizing real PLCs connected to software simulations of industrial processes. The simulation offers possibility to select the complexity of a controlled task, e.g. a presence of random malfunctions. Tutors assign proper grades to students according to the quality of their programs but their testing often leads to time-consuming operations. For simple educational tasks, we have made successful experiments with formal methods based on partial search of state space of automata, which we present in the second part of the paper. Finally, we consider possible applications of our approach for a remote learning.

The paper presents a case study based on our practical model of energy saving in a small building equipped by an industrial distributed control system. First, we overview our model built over LonWorks networking platform and then we discuss increasing the reliability of control programs by formal methods. Their possible application is demonstrated by the example of verifying the control program for a solar space heating. We show that some safety verifications are performable without constructing a whole hybrid model. Finally, we discuss the results achieved up to date. The principles presented in this case study are applicable on a general level for other similar systems.

K provedení formální verifikace PLC programu je nutné jeho modelování ve verifikačním nástroji, například SMV nebo Uppaal. K modelování je možné využít převod programu algoritmem APLCTRANS na množinu logických prirazení. Postupem, který využívá tohoto algoritmu, lze modelovat pouze programy, které umí použitý algoritmus zpracovat, to znamená programy, které využívají omezených programovacích možností. Ukazuje se však, že výsledné modely mohou vést na nižší výpočetní nároky na proces verifikace než modely vytvořené obecnejšími postupy založenými na slučování modelů jednotlivých programových elementů (např. instrukcí). Postup se hodí pro modelování a verifikaci krátkých programů nebo dílčích bloků či funkcí rozsáhlejších řídicích algoritmů.

Článek uvádí do automatického prohledávání webových stránek, rozebírá problémy, které nastávají při prohledávání webových stránek, a objasňuje postup výpočtu ohodnocení stránek známé jako page rank.

Článek uvádí do struktury vyhledávače Google a rozebírá problémy optimalizace stránek pro vyhledavače.