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.

Verification of PLC programs can be done by their modelling in a universal verification tool as SMV or Uppaal. This paper proposes a modelling procedure which creates a SMV or Uppaal model of PLC program given as system of logical assignments got by the APLCTRANS algorithm. The automaton described by this assignment system is an abstraction suitable for modelling in the mentioned tools. Proposed procedure is able to model only programs, which can be proceeded by APLCTRANS, that means all programming facilities cannot be used in the modelled program. Obtained model can lead to lower computational burden than models derived from particularmodels of program elements (for instance instructions). The procedure is suitable for modelling and verification of short control programs or program fragments and functions.

The article introduces into automatic searching of web pages. It describes the problems that are encountered while crawling web pages and it explains the calculation of page rank valuation of the pages.

The article introduces into structure of searching engine Google and problem with SEO (search engine optimization).