Using MathLang to check the correctness of specifications in object-Z

David Feller, Fairouz Dib Kamareddine, Lavinia Burski

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The importance of thoroughly checking software specifications is widely recognised in the software industry, particularly for software involved in dealing with safety critical systems. The Math Lang project has been successfully used to check large mathematical texts for correctness in a stepwise fashion. Currently Math Lang is being tested for checking the correctness of formal specifications written in Z. Since object-orientation is a vital concept for software specification, it is important that the tools available for thoroughly checking specifications can be used with a language powerful enough to express specifications for object-oriented software. This paper aims to test the usefulness of Math Lang for the computerisation of formal specifications written in Object-Z.

Original languageEnglish
Title of host publicationModern Mathematical Methods and High Performance Computing in Science and Technology
Subtitle of host publicationM3HPCST, Ghaziabad, India, December 2015
EditorsVinai K. Singh, H. M. Srivastava, Ezio Venturino, Michael Resch, Vijay Gupta
PublisherSpringer
Pages45-70
Number of pages26
ISBN (Electronic)9789811014543
ISBN (Print)9789811014536
DOIs
Publication statusPublished - 2016
Event1st International Conference on Modern Mathematical Methods and High Performance Computing in Science and Technology 2015 - Ghaziabad, India
Duration: 27 Dec 201529 Dec 2015

Publication series

NameSpringer Proceedings in Mathematics & Statistics
PublisherSpringer
Volume171
ISSN (Print)2194-1009

Conference

Conference1st International Conference on Modern Mathematical Methods and High Performance Computing in Science and Technology 2015
CountryIndia
CityGhaziabad
Period27/12/1529/12/15

Keywords

  • MathLang
  • Object-oriented design
  • Object-Z
  • Software specification and correctness

ASJC Scopus subject areas

  • Mathematics(all)

Fingerprint Dive into the research topics of 'Using MathLang to check the correctness of specifications in object-Z'. Together they form a unique fingerprint.

  • Cite this

    Feller, D., Kamareddine, F. D., & Burski, L. (2016). Using MathLang to check the correctness of specifications in object-Z. In V. K. Singh, H. M. Srivastava, E. Venturino, M. Resch, & V. Gupta (Eds.), Modern Mathematical Methods and High Performance Computing in Science and Technology: M3HPCST, Ghaziabad, India, December 2015 (pp. 45-70). (Springer Proceedings in Mathematics & Statistics; Vol. 171). Springer. https://doi.org/10.1007/978-981-10-1454-3_5