Modern automation systems are complicated structures. Designing the control of these systems has similarities with traditional software development. Successful control design is based on a high-quality design process and strict testing policy. This thesis deals with the use of formal methods in PLC program development. A reason for using the formal methods is the need for good quality PLC programs with fewer errors.

Advantages of simulation have a big role in the thesis. Simulation is a powerful tool for many different cases. In this thesis simulation is introduced as a discrete event model. Discrete event simulation has been widely used to describe production processes. In many cases simulation tools have shown their strength by solving production problems. A successful simulation project is co-operation of simulation experts and people who know the process of the company. The thesis describes the basic structure of a simulation project step by step.

Verification and validation (V&V) are discussed from the software development point of view. It is also described how the terms V&V are associated with PLC programs and simulation models. The connection between PLC-programs and 3D simulation modes is shown in practice. A practical case of the thesis is a system in which students can practice and test their PLC-programs with a virtual (simulated) model of a real system. The system was designed for Lahti University of Applied Sciences, Faculty of Technology

@mastersthesis{Koukka2010:INSSI40097,
  author = {Koukka, Henri},
  title = {Using 3D simulation models for verification of PLC-programs},
  year = {2010},
  school = {Helsinki University of Technology},
  address = {Espoo, Finland},
  abstract = {Nykyaikaiset automaatiojärjestelmät ovat monimutkaisia
    kokonaisuuksia, joiden ohjaussuunnittelussa on samoja piirteitä kuin
    perinteisessä ohjelmistosuunnittelussa. Onnistuneen ohjaussuunnittelun
    perustana on laadukas tuotantoprosessi ja hyvin suunniteltu
    testauskäytäntö. Työssä tutustutaan formaalien menetelmien käyttöön
    PLC-ohjelmistojen kehityksessä. Formaalien menetelmien tavoitteena on
    tuottaa laadukkaampia ohjelmia, joissa virheiden määrä on karsittu
    minimiin.
    
    Oma tärkeä roolinsa työssä on simuloinnin hyödyntämisellä. Simulointi on
    menetelmä, jolla on monia käyttötarkoituksia. Tässä työssä simulointi
    esitetään tapahtumapohjaisen mallin mukaisena työkaluna. Tapahtumapohjaista
    simulointia on totuttu käyttämään tuotannollisten prosessien kuvaamiseen.
    Simulointityökaluja on hyödynnetty järjestelmien kehittämisessä ja
    prosessien ongelmakohtien löytämiseen. Onnistunut simulointiprojekti on
    asiaan vihkiytyneiden ammattilaisten ja yrityksen prosessin tuntevien
    ihmisten yhteistoimintana syntynyt lopputulos. Simulointiprojekti on
    monivaiheinen tehtävä ja työssä käydään simulointiprojektin toteutus läpi
    vaihe vaiheelta.
    
    Työssä käsitellään lyhyesti verifiointia ja validointia ohjelmistotuotannon
    näkökulmasta, mutta kuvataan myös kuinka kyseiset termit liittyvät
    PLC-ohjelmien ja simulointimallien testaukseen ja hyväksymiseen.
    Simuloinnin ja PLC-ohjelmoinnin yhteyttä käsitellään työn käytännön
    osiossa, jossa raportoidaan Lahden ammattikorkeakoulun Tekniikan alalle
    toteutetun 3D-simulointia hyödyntävän PLC-ohjelmoinnin testaus- ja
    kehitysympäristön kehitysvaiheita}
}