Dp 194 en
Verification by SMV
Author: Šprdlík Otakar
Formal verification methods check properties of miscelaneous systems. For example, they can be used for validation of Programmable Logic Controller (PLC) programs. Verification of PLC programs can be done by their modelling in a universal verification tool as SMV or Uppaal. This diploma thesis proposes a modelling procedure which creates a SMV model of PLC program given as system of logical equations got by the APLCTRANS algorithm. The automaton described by this equation system is an abstraction suitable for modelling in the mentioned tools. The aim of the thesis was extended to modelling in Uppaal. Procedure can model timers in Uppaal too. 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 particular models of program elements (for instance instructions). The procedure is suitable for modelling and verification of short control programs or program fragments and functions.
- Šprdlík Otakar, mailto:sprdlo1@fel.cvut.cz
- Šusta Richard, mailto:susta@control.felk.cvut.cz
