Skip to main content
SpringerLink
Log in

Verifying χ Models of Industrial Systems with Spin

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2006)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4260))

Included in the following conference series:

  • 630 Accesses

Abstract

The language χ has been developed for modeling of industrial systems. Its simulator has been successfully used in many industrial areas for obtaining performance measures. For functional analysis simulation is less applicable and such analysis can be done in other environments. The purpose of this paper is to describe an automatic translator from χ to Promela, the input language of the well known model-checker Spin. We highlight the differences between the two languages and show, in a step by step manner, how some of them can be resolved. We conclude by giving a translation scheme and apply the translator in a small industrial case study.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. van Beek, D.A., van der Ham, A., Rooda, J.E.: Modelling and control of process industry batch production systems. In: 15th Triennial World Congress of the International Federation of Automatic Control, Barcelona, Spain (2002)

    Google Scholar 

  2. Blom, S., Fokkink, W., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.C.: μCRL: A toolset for analysing algebraic specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 250–254. Springer, Heidelberg (2001)

    Google Scholar 

  3. Bortnik, E., Trčka, N., Wijs, A.J., Luttik, S.P., van de Mortel-Fronczak, J.M., Baeten, J.C.M., Fokkink, W.J., Rooda, J.E.: Analyzing a χ model of a turntable system using SPIN, CADP and UPPAAL. Journal Of Logic and Algebraic Programming 65, 51–104 (2005)

    Google Scholar 

  4. Bos, V., Kleijn, J.J.T.: Automatic verification of a manufacturing system. Robotics and Computer Integrated Manufacturing 17, 185–198 (2001)

    Article  Google Scholar 

  5. Bošnački, D.: Enhancing State Space Reduction Techniques for Model Checking. PhD thesis, Eindhoven University of Technology (2001)

    Google Scholar 

  6. van Campen, E.J.J.: Design of a Multi-Process Multi-Product Wafer Fab. PhD thesis, Eindhoven University of Technology (2000)

    Google Scholar 

  7. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  8. Fey, J.J.H.: Design of a Fruit Juice Blending and Packaging Plant. PhD thesis, Eindhoven University of Technology (2000)

    Google Scholar 

  9. Gerth, R.: Concise Promela reference. Obtainable from: http://spinroot.com/spin/Man/Quick.html

  10. Govaarts, J.A.: Efficiency in a lean assembly line: a case study at NedCar born. Master Thesis (October 1997)

    Google Scholar 

  11. Havelund, K., Lowry, M., Penix, J.: Formal analysis of a space-craft controller using SPIN. IEEE Trans. on Software Engineering 27(8), 749–765 (2001)

    Article  Google Scholar 

  12. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  13. Holzmann, G.J.: The SPIN model checker. Addison-Wesley, Reading (2003)

    Google Scholar 

  14. Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Engineering 23(5), 279–295 (1997); Special issue on Formal Methods in Software Practice

    Article  MathSciNet  Google Scholar 

  15. Kernighan, B.W., Ritchie, D.M.: The C Programming Language, 2nd edn. Prentice-Hall, Englewood Cliffs (1988)

    Google Scholar 

  16. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. Journal on Software Tools for Technology Transfer 1(1-2), 134–152 (1997)

    Google Scholar 

  17. Luttik, B., Trčka, N.: Stuttering congruence for χ. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 185–199. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  18. Meijer, R.: χ to Promela translator. Obtainable from the TIPSy project web site: http://www.cwi.nl/~wijs/TIPSy/main.htm

  19. Schiffelers, R.R.H., Man, K.L.: Formal Specification and Analysis of Hybrid Systems. PhD thesis, Eindhoven University of Technology (2006)

    Google Scholar 

  20. Stirling, C.: Modal and Temporal Properties of Processes. Springer, Heidelberg (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, Eindhoven University of Technology, P.O. Box 513, NL-5600 MB, Eindhoven, The Netherlands

    Nikola Trčka

Authors
  1. Nikola Trčka
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. International Institute of Software Technology, United Nations University, Macau, China

    Zhiming Liu

  2. Software Engineering Institute, East China Normal University, 200062, Shanghai, China

    Jifeng He

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Trčka, N. (2006). Verifying χ Models of Industrial Systems with Spin . In: Liu, Z., He, J. (eds) Formal Methods and Software Engineering. ICFEM 2006. Lecture Notes in Computer Science, vol 4260. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901433_8

Download citation

  • DOI: https://doi.org/10.1007/11901433_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-47460-9

  • Online ISBN: 978-3-540-47462-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation