Skip to main content
SpringerLink
Log in
Book cover

Concurrent Engineering Approaches for Sustainable Product Development in a Multi-Disciplinary Environment pp 145–156Cite as

Formal Analysis Meets 3D-Visualization

  • Conference paper
  • First Online:

  • 2511 Accesses

Abstract

This paper strikes two technical aspects that have become commonly applied in engineering, but, nevertheless, barely benefit from each other, at least what today’s concurrent engineering is concerned. One of them has to do with 3D-Visualization, be it as an output of a CAD-system, or even photo-realistic rendered/ray traced images and animations of the product or production line under consideration, and the other deals with Formal Analysis, i.e., the verification of (safety) properties against a suitable formal model of the scenario. In this paper we bring both these aspects together. We show how behaviors of a system deduced from verification results can be visualized as animations in the 3D model of the system. We also discuss how modifications of the 3D scene like positioning and adding or removing of objects can be reflected in the formal model of the system. As formal basis we use the language of hybrid automata, as 3D modeling language we use XML3D.

This is a preview of subscription content, 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   259.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   329.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   329.99
Price excludes VAT (USA)
  • Durable hardcover 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Sons K, Klein F, Rubinstein D, Byelozyorov S, Slusallek P. XML3D – Interactive 3D Graphics for the Web. In Web3D ‘10: Proceedings of the 15th International Conference on Web 3D Technology. Los Angeles: ACM; 2010. p. 175-184.

    Google Scholar 

  • XML3D.ORG - The official XML3D website. [Online]. Available from: xml3d.org.

    Google Scholar 

  • Alur R, Courcoubetis C, Henzinger TA. Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In Grossman RL, Nerode A, Ravn and H. AP, Rischel H, editors. Lecture Notes in Computer Science: Hybrid Systems.: Springer Verlag; 1993. p. 209-229.

    Google Scholar 

  • Henzinger TA. The theory of hybrid automata. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science; 1996; Washington, DC,: IEEE Computer Society. p. 278.

    Google Scholar 

  • Henzinger TA, Ho PH, Wong-Toi H. HYTECH: a model checker for hybrid systems. In International Journal on Software Tools for Technology Transfer (STTT); 1997: Springer Berlin/Heidelberg. p. 110-122.

    Google Scholar 

  • Frehse G. PHAVer: algorithmic verification of hybrid systems past HyTech. In Int. J. Softw. Tools Technol. Transf.; 2008; Berlin, Heidelberg: Springer-Verlag. p. 263–279.

    Google Scholar 

  • SmartFactory-KL. [Online]. Available from: smartfactory-kl.de.

    Google Scholar 

  • ISReal BMB + F Project. [Online]. Available from: www-ags.dfki.uni-sb.de/~ klusch/isreal/.

    Google Scholar 

  • CINEMA 4D. [Online]. Available from: maxon.net/products/cinema-4d-studio/who-should-use-it.html.

    Google Scholar 

  • Nonnengart A. A deductive model checking approach for hybrid systems. Research Report. Saarbrücken: Max-Planck-Institut für Informatik; 1999.

    Google Scholar 

  • Nonnengart A. Hybrid systems verification by location elimination. In Lynch N, Krogh BH, editors. Proceedings of the 3rd International Workshop HSCC 2000; 2000: Springer Verlag. p. 352-365.

    Google Scholar 

  • Alur R, Henzinger TA, Ho PH. Automatic Symbolic Verification of Embedded Systems. In IEEE Transactions on Software Engineering; 1996. p. 181-201.

    Google Scholar 

  • Henzinger TA, Rusu V. Reachability verification for hybrid automata in. In Proceedings of the First International Workshop on Hybrid Systems: Computation and Control, Lecture Notes in Computer Science; 1998: Springer Verlag. p. 190-204.

    Google Scholar 

  • Henzinger TA, Ho PH, Wong-Toi H. HYTECH: a model checker for hybrid systems. International Journal on Software Tools for Technology Transfer (STTT). 1997; 1(1): p. 110-122.

    Google Scholar 

  • Simulink : Simulation und Model-Based Design. [Online]. Available from: mathworks.de/products/simulink/.

    Google Scholar 

  • d/dt. [Online]. Available from: www-verimag.imag.fr/~ tdang/Tool-ddt/ddt.html.

    Google Scholar 

  • Frehse G. PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 2008 May; 10(3): p. 263-279.

    Google Scholar 

  • Larsen KG, Pettersson P, Yi W. Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer (STTT). 1997; 1: p. 134-152.

    Google Scholar 

  • Milner R, Parrow J, Walker D. A calculus of mobile processes, I. Inf. Comput. 1992 sep; 100: p. 1–40.

    Google Scholar 

  • Radio-frequency identification - Wikipedia, the free encyclopedia. [Online]. Available from: http://en.wikipedia.org/wiki/Radio-frequency_identification.

Download references

Author information

Authors and Affiliations

  1. DFKI Saarbrücken, Campus D 3.2, 66123, Saarbrücken, Germany

    Christopher Krauß & Andreas Nonnengart

Authors
  1. Christopher Krauß
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andreas Nonnengart
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. PROSTEP AG, Dolivostr. 11, Darmstadt, 64293, Germany

    Josip Stjepandić

  2. University of Applied Science Trier, Schneidershof, Trier, 54293, Germany

    Georg Rock

  3. , School of Aerospace, Mechanical and Manu, RMIT University, Plenty Road, Bundoora, 3083, Victoria, Australia

    Cees Bil

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag London

About this paper

Cite this paper

Krauß, C., Nonnengart, A. (2013). Formal Analysis Meets 3D-Visualization. In: Stjepandić, J., Rock, G., Bil, C. (eds) Concurrent Engineering Approaches for Sustainable Product Development in a Multi-Disciplinary Environment. Springer, London. https://doi.org/10.1007/978-1-4471-4426-7_13

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-4426-7_13

  • Published:

  • Publisher Name: Springer, London

  • Print ISBN: 978-1-4471-4425-0

  • Online ISBN: 978-1-4471-4426-7

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation