Skip to main content

Applying Category Theory to Derive Engineering Software from Encoded Knowledge

  • Conference paper
  • First Online:

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

Abstract

In an industrial research project, we have demonstrated the feasibility of applying category-theoretic methods to the specification, synthesis, and maintenance of industrial strength software systems. The demonstration used a first-of-its-kind tool for this purpose, Kestrel’s Specware™ software development system. We describe our experiences and discuss broadening the application of such category-theoretic methods in industry.

Although the technology is promising, it needs additional development to make it generally usable. This is not surprising given its mathematical foundation. On the other hand, we believe our demonstration is a turning point in the use of mathematically rigorous approaches in industrial software development and maintenance. We have demonstrated here the capture via mathematical methods not only of software engineering design rationale, but also of the product design and manufacturing process rationale used by different engineering disciplines, and the production of usable software directly from the captured rationale. We feel that that further evolution of the tools for this technology will make formal systems engineering a reality.

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

Buying options

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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. D. Bjorner and C. Jones. Formal Specification and Software Development. Prentice-Hall International, 1982.

    Google Scholar 

  2. L Blaine and A Goldberg. Dtre-a semi-automatic transformation system. In B Moller, editor, Constructing Programs from Specifications. North-Holland, 1991.

    Google Scholar 

  3. T. Gruber et al. An ontology for engineering mathematics. In Proceedings of the Fourth International Conference on Principles of Representation and Reasoning. Morgan Kauffman, 1994.

    Google Scholar 

  4. J. A. Goguen and R. M. Burstall. Some fundamental algebraic tools for the semantics of computation-part 1: Comma categories, colimits, signatures and theories. Theoretical Computer Science, 31(1,2):175–209, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  5. J. A. Goguen and R. M. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39(1):95–146, 1992.

    MATH  MathSciNet  Google Scholar 

  6. R. Jullig and Y. V. Srinivas. Diagrams for software synthesis. In Proceedings of KBSE’ 93: The Eighth Knowledge-Based Software Engineering Conference, pages 10–19. IEEE Computer Society Press, 1993.

    Google Scholar 

  7. J. Meseguer. General logics. In Logic Colloquium’ 87, pages 275–329. Science Publishers B. V. (North-Holland), 1987.

    Google Scholar 

  8. B C Pierce. Basic CategoryThe oryf or Computer Scientists. MIT Press, 1991.

    Google Scholar 

  9. D. Smith. Kids: Akno wledge based software development system. In M. Lowry and R. McCartney, editors, Automating Software Design. MIT Press, 1991.

    Google Scholar 

  10. J. M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, 1992.

    Google Scholar 

  11. Y. V. Srinivas and R. Jullig. specwaretm: Formal support for composing software. In Proceedings of the Conference of Mathematics of Program Construction, 1995.

    Google Scholar 

  12. T. C. Wang and A. Goldberg. A mechanical verifier for supporting the design of reliable reactive systems. In Proceedings of the International Symposium on Software ReliabilityE ngineering, 1991.

    Google Scholar 

  13. K. Williamson and M. Healy. Formally specifyuing engineering design rationale. In Proceedings of the Automated Software Engineering Conference-1997, 1997.

    Google Scholar 

  14. K. Williamson and M. Healy. Deriving engineering software from requirements. Journal of Intelligent Manufacturing, 11(1):3–28, 2000.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Healy, M., Williamson, K. (2000). Applying Category Theory to Derive Engineering Software from Encoded Knowledge. In: Rus, T. (eds) Algebraic Methodology and Software Technology. AMAST 2000. Lecture Notes in Computer Science, vol 1816. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45499-3_34

Download citation

  • DOI: https://doi.org/10.1007/3-540-45499-3_34

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67530-3

  • Online ISBN: 978-3-540-45499-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics