Skip to main content

Formal methods and customized visualization: A fruitful symbiosis

  • Selected Papers
  • Conference paper
  • First Online:
Services and Visualization Towards User-Friendly Design

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1385))

Abstract

Formal methods and visualization techniques are central for the realization of user-centered computing environments: they are responsible for ensuring correctness and comfort of tool usage in application-level development scenarios. Their synergy is the key to a wide acceptance and improved productivity. We illustrate here on a case study how even elaborate formal methods can be profitably used by non experts, providing that they are fully automatable and supported by powerful visualization aids, and how formal methods are the key to a flexible ‘look and feel’ of the presentation-layer, which becomes a customizable commodity within a user-specific configuration space. This way, an application development tool becomes really capable to evolve together with the application, the project, and single user's needs.

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

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. V. Braun, T. Maxgaxia, B. Steffen, H. Yoo, T. Rychly: Safe Service Customization, Proc. IN'97, IEEE Communication Soc. Workshop on Intelligent Network, Colorado Springs, CO (USA), 4–7 May 1997, IEEE Comm. Soc. Press

    Google Scholar 

  2. M. von der Beeck, V. Braun, A. Claßen, A. Dannecker, C. Friedrich, D. Koschützki, T. Margaria, F. Schreiber and B. Steffen: Graphs in METAFrame: The Unifying Power of Polymorphism, Proc. TACAS'97, Enschede (NL), April 1997, LNCS 1217, Springer Verlag, pp. 112–129.

    Google Scholar 

  3. Bozga M., Fernandez J.-C, Kerbrat A., Mounier L., Protocol verification with the ALDEBARAN toolset, Int. Journ. on Software Tools for Technology Transfer, Vol.1 No. 1/2, Springer Verlag, Nov. 1997.

    Google Scholar 

  4. R.E. Bryant: Graph-based algorithms for boolean function manipulation, IEEE Trans. Computing, vol. C-35(8), August 1986, pp. 677–691.

    Google Scholar 

  5. da Vinci is available at ftp://ftp.uni-bremen.de/pub/graphics/daVinci

    Google Scholar 

  6. H. Garavel: An Overview of the Eucalyptus Toolbox. Proc. of the COST 247 Int. Workshop on Applied Formal Methods in System Design, University of Maribor (SLO), June 1996, pp. 76–88.

    Google Scholar 

  7. J. Henriksen, J. Jensen, M. JØrgensen N. Klarlund, R. Paige, T. Rauhe, A. Sandholm: Mona: Monadic second-order logic in practice, Proc. of TACAS'95, århus (DK), May 1995, LNCS 1019, Springer Verlag, pp. 89–110.

    Google Scholar 

  8. P. Kelb, T. Margaria, M. Mendier, C. Gsottberger: Mosel: A Flexible Toolset for Monadic Second-Order Logic,” TACAS'97, Enschede (NL), April 1997, LNCS 1217, Springer Verlag, pp. 183–202.

    Google Scholar 

  9. P. Kelb, T. Margaria, M. Mendier, C. Gsottberger: Mosel: A sound and efficient tool for M2L(Str),” Proc. CAV'97, Haifa (Israel), Juli 1997, LNCS, Springer Verlag.

    Google Scholar 

  10. D. Kozen: Results on the Propositional Μ-Calculus, Theoretical Computer Science, Vol. 27, 1983, pp. 333–354.

    Article  MATH  MathSciNet  Google Scholar 

  11. T. Margaria: Fully Automatic Verification and Error Detection for Parameterized Iterative Sequential Circuits, Proc. TACAS'96, Passau (D), March 1996, LNCS N. 1055, Springer Verlag, pp. 258–277.

    Google Scholar 

  12. T. Margaria: Verification of Systolic Arrays in M2L(Str), Techn. Rep. MIP-9613, Universität Passau, Juli 1996.

    Google Scholar 

  13. T. Margaria, M. Griva, R. Tesio: Semantic Extraction for the Automatic Verification of VHDL Descriptions, Techn. Rep. MIP 94-11, Univ. of Passau (D), October 1994, 21 pp.

    Google Scholar 

  14. T. Margaria, B. Steffen: Backtracking-free Design Planning by Automatic Synthesis in METAFrame Proc. FASE'98, Lisbon (P), April 1998, LNCS, Springer Verlag.

    Google Scholar 

  15. B. Steffen, T. Margaria, V. Braun: The Electronic Tool Integration Platform: Concepts and Design, Int. Journ. on Software Tools for Technology Transfer, Vol.1 No.1/2, Springer Verlag, Nov. 1997. See also http://eti.cs.uni-dortmund.de.

    Google Scholar 

  16. B. Steffen, T. Margaria, A. Claßen: Heterogeneous Analysis and Verification for Distributed Systems, In “SOFTWARE: Concepts and Tools”, vol. 17, N.1, pp. 13–25, Springer Verlag, 1996.

    Google Scholar 

  17. B. Steffen, T. Margaria, A. Claßen, V. Braun: The MetaFrame '95 Environment, Proc. CAV'96, Int. Conf. on Computer-Aided Design, Juli–Aug. 1996, New Brunswick, NJ, USA, LNCS, pp. 450–453, Springer Verlag.

    Google Scholar 

  18. B. Steffen, T. Margaria, A. Claßen, V. Braun, M. Reitenspieß: An Environment for the Creation of Intelligent Network Services, in “Intelligent Networks: IN/AIN Technologies, Operations, Services, and Applications — A Comprehensive Report” Int. Engineering Consortium, Chicago IL, 1996, pp. 287–300 — reprinted in Annual Review of Communications, IEC, 1996, pp. 919–935.

    Google Scholar 

  19. P. Wolper: Where is the algorithmic support? Strategic Directions in Computing Research, Concurrency Work. Group, Pos. Statement, ACM Computing Surveys, 28A(4), Dec. 1996,http://www.montefiore.ulg.ac.be/ pw/sdcr/concurrency.html

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Tiziana Margaria Bernhard Steffen Roland Rückert Joachim Posegga

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Margaria, T., Braun, V. (1998). Formal methods and customized visualization: A fruitful symbiosis. In: Margaria, T., Steffen, B., Rückert, R., Posegga, J. (eds) Services and Visualization Towards User-Friendly Design. Lecture Notes in Computer Science, vol 1385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0053506

Download citation

  • DOI: https://doi.org/10.1007/BFb0053506

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64367-8

  • Online ISBN: 978-3-540-69760-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics