Skip to main content
SpringerLink
Log in

Towards MultiMedia Instruction in Safe and Secure Systems

  • Chapter
Mechanizing Mathematical Reasoning

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2605))

  • 1042 Accesses

Abstract

The aim of the MMiSS project is the construction of a multi-media Internet-based adaptive educational system. Its content will initially cover a whole curriculum in the area of Safe and Secure Systems. Traditional teaching materials (slides, handouts, annotated course material, assignments and so on) are to be converted into a new hypermedia format, integrated with tool interactions for formally developing correct software; they will be suitable for learning on campus and distance learning, as well as interactive, supervised, or co-operative self-study. Coherence and consistency are especially emphasised, through extensive semantic linking of teaching elements, and through a process model borrowed from the theory of formal software development, enlarging the knowledge base with the help of version and configuration management, to ensure “sustainable development”, i.e. continuous long-term usability of the contents.

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. Amthor, P.: Structural Decomposition of Hybrid Systems – Test Automation for Hybrid Reactive Systems. PhD thesis. Universität Bremen (1999); Monographs of the Bremen Institute of Safe Systems 13. Shaker

    Google Scholar 

  2. Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P.D., Sannella, D., Tarlecki, A.: Casl: The Common Algebraic Specification Language. Theoretical Computer Science (2003) (to appear)

    Google Scholar 

  3. Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P.D., Sannella, D., Tarlecki., A. (eds.): Casl– the CoFI Algebraic Specification Language: Tutorial Introduction, Language Summary, Formal Definition, Basic Data Types (submitted)

    Google Scholar 

  4. Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.): Algebraic Foundations of System Specification. IFIP State-of-the-Art Reports. Springer, Heidelberg (2000)

    Google Scholar 

  5. Autexier, S., Hutter, D., Mantel, H., Schairer, A.: INKA 5.0: a logic voyager. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 207–211. Springer, Heidelberg (1999), see also www.dfki.de/vse/

  6. Autexier, S., Hutter, D., Mantel, H., Schairer, A.: Towards an Evolutionary Formal Software Development Using Casl. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 73–88. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  7. Autexier, S., Mossakowski, T.: Integrating HOLCASL into the development graph manager MAYA. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol. 2309, pp. 2–17. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Basin, D.A., Klarlund, N.: Automata based symbolic reasoning in hardware verification. Formal Methods in Systems Design 13(3), 255–288 (1998)

    Article  Google Scholar 

  9. Basin, D.A., Krieg-Brückner, B.: Formalization of the Development Process. In: [4], pp. 521–562

    Google Scholar 

  10. Bidoit, M., Kreowski, H.-J., Lescanne, P., Orejas, F., Sannella, D. (eds.): Algebraic System Specification and Development: A Survey and Annotated Bibliography. LNCS, vol. 501. Springer, Heidelberg (1991)

    MATH  Google Scholar 

  11. Broy, M., Jähnichen, S. (eds.): KORSO 1995. LNCS, vol. 1009. Springer, Heidelberg (1995)

    Google Scholar 

  12. Cerioli, M., Gogolla, M., Kirchner, H., Krieg-Brückner, B., Qian, Z., Wolf, M. (eds.): Algebraic System Specification and Development: Survey and Annotated Bibliography, 2nd edn (1977); Monographs of the Bremen Institute of Safe Systems 3. Shaker, Aachen (1998) ISBN 3-8265-4067-0

    Google Scholar 

  13. CoFI. The Common Framework Initiative for algebraic specification and development, electronic archives. Notes and Documents accessible at http://www.cofi.info

  14. CoFI Language Design Task Group. Casl – The CoFI Algebraic Specification Language – Summary. In: [13]

    Google Scholar 

  15. Freericks, C.: Open-Source Standards on Software Process: A Practical Application. In: Jakobs, K. (ed.) IEEE Communications Magazine, vol. 39(4), pp. 116–123 (2001), www.tzi.de/gdpa/

  16. Fröhlich, M.: Inkrementelles Graphlayout im Visualisierungssystem da Vinci. Dissertation. Monographs of the Bremen Institute of Safe Systems 6. Shaker (1998) ISBN 3-8265- 4069-7

    Google Scholar 

  17. Fröhlich, M., Werner, M.: The interactive Graph-Visualization System daVinci – A User Interface for Applications. Informatik Bericht Nr. 5/94, Universität Bremen (1994), Up-to-date documentation: http://www.tzi.de/~daVinci

  18. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International Series in Computer Science (1985)

    Google Scholar 

  19. Kohlhase, M.: OMDoc: Towards an OpenMath representation of mathematical documents. SEKI Report SR-00-02, Fachbereich Informatik, Universität des Saarlandes (2000), http://www.mathweb.org/ilo/omdoc/

  20. Kohlhase, M.: Towards an Internat Standard for the Administration, Distribution and Teaching of Mathematical Knowledge. In: Proc. Artificial Intelligence and Symbolic Computation. LNCS (LNAI). Springer, Heidelberg (2000)

    Google Scholar 

  21. Krieg-Brückner, B., Peleska, J., Olderog, E.-R., Baer, A.: The UniForM Workbench, a Universal Development Environment for Formal Methods. In: Woodcock, J.C.P., Davies, J., Wing, J.M. (eds.) FM 1999. LNCS, vol. 1709, pp. 1186–1205. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  22. Krieg-Brückner, B.: Seven Years of COMPASS. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 1–13. Springer, Heidelberg (1996)

    Google Scholar 

  23. Melis, E., Andres, E., Goguadse, G., Libbrecht, P., Pollet, M., Ulrich, C.: ActiveMath: System description. In: Moore, J.D., Redfield, C., Johnson, W.L. (eds.) Artificial Intelligence in Education, pp. 580–582. IOS Press, Amsterdam (2001)

    Google Scholar 

  24. Meyer, O.: Structural Decomposition of Timed CSP and its Application in Real- Time Testing. PhD thesis. Universität Bremen (2001); (To appear in Monographs of the Bremen Institute of Safe Systems. Logos Verlag.)

    Google Scholar 

  25. Mossakowski, T.: Casl: From Semantics to Tools. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 93–108. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  26. Mossakowski, T., Kolyang, Krieg-Brückner, B.: Static semantic analysis and theorem proving for Casl. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 333–348. Springer, Heidelberg (1998), http://www.tzi.de/cofi

    Google Scholar 

  27. Mosses, P.D.: CoFI: The Common Framework Initiative for Algebraic Specification and Development. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 115–137. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  28. Reichel, H., Mossakowski, T., Roggenbach, M., Schröder, L.: CoCASL – Proof support for co-algebraic specification. In: Recent Trends in Algebraic Development Techniques, 16th International Workshop, WADT 2002, LNCS. Springer, Heidelberg (accepted for presentation)

    Google Scholar 

  29. Roggenbach, M.: CSP-CASL – A new Integration of Process Algebra and Algebraic Specification. In: Recent Trends in Algebraic Development Techniques, 16th International Workshop, WADT 2002. LNCS. Springer, Heidelberg (accepted for presentation)

    Google Scholar 

  30. Roggenbach, M., Mossakowski, T.: What is a good Casl specification? In: Recent Trends in Algebraic Development Techniques, 16th International Workshop, WADT 2002. LNCS. Springer, Heidelberg (accepted for presentation)

    Google Scholar 

  31. Roggenbach, M., Schröder, L.: Towards Trustworthy Specifications I: Consistency Checks. In: Cerioli, M., Reggio, G. (eds.) WADT 2001 and CoFI WG Meeting 2001. LNCS, vol. 2267, pp. 305–327. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  32. Roggenbach, M., Schröder, L.: Towards Trustworthy Specifications II: Testing by Proof. In: Recent Trends in Algebraic Development Techniques, 16th International Workshop, WADT 2002. LNCS. Springer, Heidelberg (accepted for presentation)

    Google Scholar 

  33. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International Series in Computer Science (1998)

    Google Scholar 

  34. Schröder, L., Mossakowski, T.: HasCASL: Towards integrated specification and development of Haskell programs. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, p. 99. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  35. Forschergruppe SofTecNRW. Studie über Softwaretechnische Anforderungen an multimediale Lehr- und Lernsysteme (September 1999), See also: http://www.uvm-nw.de [36]

  36. Engels, G., Kelter, U., Depke, R., Mehner, K.: Unterstützende Angebote der Softwarebegleitgruppe. In: Doberkat, E.E., et al. (eds.) Multimedia in der wirtschaftswissenschaftlichen Lehre – Erfahrungsbericht, pp. 27–56. LIT Verlag, Münster (2000)

    Google Scholar 

  37. Tej, H., Wolf, B.: A Corrected Failure-Divergence Model for CSP in Isabelle/HOL. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 318–337. Springer, Heidelberg (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Bremen Institute of Safe and Secure Systems, Universität Bremen, Postfach 330440, D-28334, Bremen

    Bernd Krieg-Brückner

Authors
  1. Bernd Krieg-Brückner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DFKI, Stuhlsatzenhausweg 3, D-66123, Saarbrücken, Germany

    Dieter Hutter

  2. German Research Center for Artificial Intelligence, DFKI GmbH,  

    Werner Stephan

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Krieg-Brückner, B. (2005). Towards MultiMedia Instruction in Safe and Secure Systems. In: Hutter, D., Stephan, W. (eds) Mechanizing Mathematical Reasoning. Lecture Notes in Computer Science(), vol 2605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32254-2_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-32254-2_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-25051-7

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation