Advertisement

Model Based Formal Verification of Distributed Production Control Systems

  • Martin Kardos
  • Franz-J. Rammig
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3147)

Abstract

The design of software for distributed production control systems (DPCS) is an error prone task. Ensuring the correctness of the design at the earliest stage possible is a major challenge in any software development process. In this context, formal verification is a very appealing approach in addition to simulation and testing, since it implies an exhaustive exploration of all possible behaviours of a system. In this paper, we present an approach towards model based formal verification for DPCS by means of model checking. The presented work is a part of the ISILEIT project that aims at the development of a seamless methodology for the integrated design, analysis and validation of distributed production control systems.

A prerequisite for model based formal verification is the existence of a formal model of the designed system. According to the ISILEIT design methodology a system is specified and modelled using an integrative specification language that combines modeling concepts taken from two different specification languages, namely the UML and the SDL languages. However, supporting formal verification for such a heterogeneous language implies requirements on formal unification and semantic integration of the adopted modeling concepts. In our approach the Abstract State Machines (ASM) formalism represents the formal platform for the unification and semantic integration. We show how the ASMs, in particular the AsmL language, have been successfully applied for creating a rigorous unified semantic model that integrates the semantics of UML State Machines, SDL Block Diagrams and Story Diagrams which form the core of the integrative specification language used in ISILEIT.

Besides the integration purpose, the ASMs serve as a basis for the application of model checking techniques. Therefore, the rest of the paper presents the work on adoption of state-of-the-art model checking techniques in order to support model checking of the ASM (AsmL) models.

Keywords

State Machine Semantic Model Formal Verification Abstract State Machine Model Check Technique 
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.
    Integrative Specification of Distributed Control Systems for the Flexible Automated Manufacturing (ISILEIT), German Research Foundation (DFG) program “integrative specification of engineering applications”, http://www.upb.de/cs/isileit/
  2. 2.
    Schäfer, W., Wagner, R., Gausemeier, J., Eckes, R.: An Engineer’s Workstation to support Integrated Development of Flexible Production Control 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. 48–68. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison-Wesley, Reading (1999)Google Scholar
  4. 4.
    ITU-T Recommendation Z.100, Specification and Description Language (SDL), International Telecommunication Union (ITU), Geneva, 1994 + Addendum 1996 Google Scholar
  5. 5.
    Fischer, T., Niere, J., Torunski, L., Zündorf, A.: Story Diagrams: A new Graph Rewrite Language based on the Unified Modelling Language and Java. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) TAGT 1998. LNCS, vol. 1764, pp. 296–309. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  6. 6.
    Gurevich, Y.: Evolving Algebras 1993: Lipari Guide. In: Börger, E. (ed.) Specification and Validation Methods, Oxford University Press, Oxford (1995)Google Scholar
  7. 7.
    Abstract State Machines home page, http://www.eecs.umich.edu/gasm/
  8. 8.
    Gurevich, Y., Schulte, W., Campbell, C., Grieskamp, W.: AsmL: The Abstract State Machine Language Version 2.0., http://research.microsoft.com/foundations/AsmL/default.html
  9. 9.
  10. 10.
    Eschbach, R., Glässer, U., Gotzhein, R., von Löwis, M., Prinz, A.: Formal Definition of SDL 2000 - Compiling and Running SDL Specifications as ASM Models. Journal of Universal Computer Science, J.UCS (October 2001)Google Scholar
  11. 11.
    Giese, H., Kardos, M., Nickel, U.: Integrating Verification in a Design Process for Distributed Production Control Systems. In: Second International Workshop on Integration of Specification Techniques for Applications in Engineering (INT 2002), Grenoble, France (April 2002)Google Scholar
  12. 12.
    Bhat, G., Cleaveland, R., Groce, A.: Efficient model checking via Buchi tableau automata. Technical report, Department of Computer Science, SUNY, Stony Brook (2000)Google Scholar
  13. 13.
    Schäfer, T., Knapp, A., Merz, S.: Model Checking UML State Machines and Collaborations. In: Proc. Wsh. Software Model Checking, Paries. Elect. Notes Theo. Comp. Sci., vol. 55(3) (2001)Google Scholar
  14. 14.
    Knapp, A., Merz, S., Rauh, C.: Model Checking Timed UML State Machines and Collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 395–416. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  15. 15.
    Diethers, K., Goltz, U., Huhn, M.: Model Checking UML Statecharts with Time. In: Proc. of the Workshop on Critical Systems Development with UML (2002)Google Scholar
  16. 16.
    David, A., Möller, M., Yi, W.: Formal Verification of UML Statecharts with Real-Time Extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 218–232. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  17. 17.
    Gnesi, S., Latella, D.: Model Checking UML Statechart Diagrams using JACK. In: Proc. Fourth IEEE International Symposium on High Assuarance Systems Enginering, IEEE Press, Los Alamitos (1999)Google Scholar
  18. 18.
    del Castillo, G., Winter, K.: Model checking support for the ASM high-level language. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 331–346. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  19. 19.
    Winter, K.: Model Checking Abstract State Machines, Ph.D. thesis, Technical University of Berlin, Germany (2001)Google Scholar
  20. 20.
    Gargantini, A., Riccobene, E., Rinzivillo, S.: Using Spin to Generate Tests from ASM Specifications. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) Proc. of 10th International Workshop on Abstract State Machines 2003, Taormina, Italy, March 3-7 (2003)Google Scholar
  21. 21.
    McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Boston (1993)zbMATHGoogle Scholar
  22. 22.
    Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering (May 1997)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Martin Kardos
    • 1
  • Franz-J. Rammig
    • 1
  1. 1.Heinz Nixdorf InstituteDesign of Parallel SystemsPaderbornGermany

Personalised recommendations