Model-Based Implementation of Real-Time Systems

  • Krzysztof Sacha
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5219)


A method is presented for modeling, verification and automatic programming of PLC controllers. The method offers a formal model of requirements, the means for defining and verifying safe behavior, and a technique for generating program code. The modeling language is UML state machine, which provides a widely accepted means for writing a specification at a suitable high level of abstraction. Such an abstract specification can be validated by the user, verified by means of a model-checker and translated automatically into a program code, which preserves the correctness and safety of the specification. The program code is written in one of the standardized IEC 61131 languages.


Program Code Time Block Input Symbol Time Symbol Output Symbol 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    OMG, Unified Modeling Language: Superstructure, version 2.0, August (2005)Google Scholar
  2. 2.
    Milner, R.: Operational and algebraic semantics of concurrent processes. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 1201–1242. Elsevier, Amsterdam (1990)Google Scholar
  3. 3.
    Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer, Berlin (1995)Google Scholar
  4. 4.
    Alur, R., Dill, D.: Automata-theoretic verification of real-time systems. In: Formal Methods for Real-Time Computing, Trends in Software Series, pp. 55–82. John Wiley & Sons, Chichester (1996)Google Scholar
  5. 5.
    Kaynar, D.K., Lynch, N., Segala, R., Vaandrager, F.: The Theory of Timed I/O Automata, Technical Report MIT-LCS-TR-917a, MIT Lab. for Computer Science (2004)Google Scholar
  6. 6.
    Dierks, H.: PLC-Automata, A New Class of Implementable Real-Time Automata. In: Bertran, M., Rus, T. (eds.) Transformation-Based Reactive Systems Development. LNCS, vol. 1231, pp. 111–125. Springer, Berlin (1997)Google Scholar
  7. 7.
    Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Springer, Berlin (1997)zbMATHGoogle Scholar
  8. 8.
    Sacha, K.: Automatic Code Generation for PLC Controllers. In: Winther, R., Gran, B.A., Dahll, G. (eds.) SAFECOMP 2005. LNCS, vol. 3688, pp. 303–316. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Sacha, K.: Translatable Finite State Time Machine. In: Gaudin, E., Najm, E., Reed, R. (eds.) SDL 2007. LNCS, vol. 4745, pp. 117–132. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  10. 10.
    Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal, Department of Computer Science. Aalborg University (2004)Google Scholar
  11. 11.
    IEC 61131-3, Programmable controllers – part 3: Programming languages, IEC (1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Krzysztof Sacha
    • 1
  1. 1.Warsaw University of TechnologyWarszawaPoland

Personalised recommendations