Advertisement

Modeling and Formal Verification of Production Automation Systems

  • Jürgen Ruf
  • Roland J. Weiss
  • Thomas Kropf
  • Wolfgang Rosenstiel
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3147)

Abstract

This paper presents the real-time model checker RAVEN and related theoretical background. RAVEN augments the efficiency of traditional symbolic model checking with possibilities to describe real-time systems. These extensions rely on multi-terminal binary decision diagrams to represent time delays and time intervals. The temporal logic CCTL is used to specify properties with time constraints. Another noteworthy feature of our model checker is its ability to compose a system description out of communicating modules, so called I/O-interval structures. This modular approach to system description alleviates the omnipresent state explosion problem common to all model checking tools.

The case study of a holonic material transport system demonstrates how such a production automation system can be modeled in our system. We devise a detailed model of all components present in the described system. This model serves as basis for checking real-time properties of the system as well as for computing key properties like system latencies and minimal response times. A translation of the original model also allows application of another time bounded property checker for verification of the holonic production system. Finally, we present an approach combining simulation and formal verification that operates on the same system model. It enables verification of larger designs at the cost of reduced coverage. Only critical states detected during simulation runs are further subjected to exhaustive model checking. We contrast the runtimes and results of our different approaches.

Keywords

Model Check Temporal Logic Linear Temporal Logic Symbolic Execution Kripke Structure 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Clarke, E.M., Grumberg, O., Peled, D.E.: Model Checking. The MIT Press, Cambridge (1999)Google Scholar
  2. 2.
    Vardi, M.Y.: Branching vs. linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 1. Springer, Heidelberg (2001) (invited paper)CrossRefGoogle Scholar
  3. 3.
    Ruf, J., Kropf, T.: Symbolic verification and analysis of discrete timed systems. Journal on Formal Methods in System Design 23(1), 67–108 (2003)zbMATHCrossRefGoogle Scholar
  4. 4.
    Emerson, E.A., Mok, A.K., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 136–145. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  5. 5.
    Ruf, J., Kropf, T.: Modeling and checking networks of communicating real-time process. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 256–279. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  6. 6.
    Ruf, J., Hoffmann, D.W., Kropf, T., Rosenstiel, W.: Simulation-guided property checking based on a multi-valued AR-automata. [30] 742–748Google Scholar
  7. 7.
    Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Journal on Formal Methods in System Design 19(1), 45–80 (2001)zbMATHCrossRefGoogle Scholar
  8. 8.
    Object Management Group (OMG): Unified Modeling Language (UML), Version 1.5. Document formal/03-03-01 (2003), http://www.omg.org
  9. 9.
    Klose, J., Kropf, T., Ruf, J.: A visual approach to validating system level designs. In: 15th International Symposium on Systems Synthesis, pp. 186–191. ACM Press, New York (2002)CrossRefGoogle Scholar
  10. 10.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: 21st International Conference on Software Engineering, pp. 411–420. ACM Press, New York (1999)CrossRefGoogle Scholar
  11. 11.
    Flake, S., Müller, W., Ruf, J.: Structured english for model checking specification. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen. 3. GI/ITG/GMM Workshop, pp. 99–108. VDE Verlag (2002)Google Scholar
  12. 12.
    Flake, S., Müller, W., Ruf, J.: A UML/OCL extension for state-oriented temporal properties with applications for manufacturing systems. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 206–226. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. 13.
    Reif, W., Schellhorn, G., Vollmer, T., Ruf, J.: Correctness of efficient real-time model checking. Journal of Universal Computer Science, Special Issue on Tools for System Design and Verification 7(2), 194–209 (2001)zbMATHGoogle Scholar
  14. 14.
    Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3), 293–318 (1992)CrossRefGoogle Scholar
  15. 15.
    Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. In: Proceedings of the 1993 IEEE/ACM International Conference on CAD, pp. 188–191. IEEE Computer Society Press, Los Alamitos (1993)Google Scholar
  16. 16.
    Grötker, T., Liao, S., Martin, G., Swan, S.: System Design with SystemC. Kluwer Academic Publishers, Dordrecht (2002)Google Scholar
  17. 17.
    Müller, W., Ruf, J., Hoffmann, D.W., Gerlach, J., Kropf, T., Rosenstiel, W.: The simulation semantics of SystemC. [30] 64–70Google Scholar
  18. 18.
    Ruf, J., Peranandam, P.M., Kropf, T., Rosenstiel, W.: Bounded property checking with symbolic simulation. In: Forum on Specification and Design Languages (2003)Google Scholar
  19. 19.
    Ruf, J.: RAVEN: Real-time analyzing and verification. Technical Report WSI 2000-3, University of Tübingen (2000)Google Scholar
  20. 20.
    Campos, S.V., Clarke, E.M.: Real-time symbolic model checking for discrete time models. In: Rus, T., Rattray, C. (eds.) Theories and Experiences for Real-Time System Development. Amast Series In Computing, vol. 2, pp. 129–145. World Scientific Publishing Corporation, Inc., River Edge (1994)Google Scholar
  21. 21.
    Iwashita, H., Nakata, T.: Forward model checking techniques oriented to buggy designs. In: Proceedings of the 1997 IEEE/ACM International Conference on CAD, pp. 400–404. ACM and IEEE Computer Society Press (1997)Google Scholar
  22. 22.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. In: Zelkowitz, M. (ed.) Highly Dependable Software. Advances in Computers, vol. 58, Academic Press, London (2003)Google Scholar
  23. 23.
    ISO/IEC: Programming Languages – C++. 2. edn. Number 14882:2003 in JTC1/SC22 – Programming languages, their environment and system software interfaces. International Organization for Standardization (2003) Google Scholar
  24. 24.
    VA Software Corporation, Open SystemC Initiative: Open SystemC Initiative (2004), www.systemc.org
  25. 25.
    Krebs, A., Ruf, J.: Optimized temporal logic compilation. Journal of Universal Computer Science, Special Issue on Tools for System Design and Verification 9(2), 120–137 (2003)Google Scholar
  26. 26.
    Flake, S., Müller, W.: A UML profile for MFERT. Technical Report 4, C-LAB Paderborn (2002) Google Scholar
  27. 27.
    Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) Hybrid Systems III: Verification and Control, pp. 232–243. Springer, Heidelberg (1996)Google Scholar
  28. 28.
    Yovine, S.: KRONOS: A verification tool for real-time systems. International Journal on Software Tools for Technology Transfer (STTT) 1(1-2), 123–133 (1997)zbMATHCrossRefGoogle Scholar
  29. 29.
    Campos, S.V.A., Clarke, E.M., Minea, M.: The Verus tool: A quantitative approach to the formal verification of real-time systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 452–455. Springer, Heidelberg (1997)Google Scholar
  30. 30.
    Nebel, W., Jerraya, A. (eds.): Design, Automation and Test in Europe, DATE 2001. IEEE Press, Los Alamitos (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Jürgen Ruf
    • 1
  • Roland J. Weiss
    • 1
  • Thomas Kropf
    • 1
  • Wolfgang Rosenstiel
    • 1
  1. 1.Wilhelm-Schickard-Institut für InformatikUniversität TübingenTübingenGermany

Personalised recommendations