Fixed-Point Arithmetic Modeled in B Software Using Reals

Jérôme Guéry, Olivier Rolland, Joris Rehm
Digital Printed Abstract View Cite
Type
Short Paper
Publication
4th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'14)

Abstract

This paper demonstrates how to introduce a fixed point arithmetic in software developed with the classical B method. The properties of this arithmetic are specified with real numbers in the AtelierB formal tool and linked to an implementation written in Ada programming language. This study has been conducted to control the loss of precision and possible overflow due to the use of fixed point arithmetic in the critical software part of a communication based train control system.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{GueryRR14,
  author       = {J{\'{e}}r{\^{o}}me Gu{\'{e}}ry and
                  Olivier Rolland and
                  Joris Rehm},
  editor       = {Yamine A{\"{\i}}t Ameur and
                  Klaus{-}Dieter Schewe},
  title        = {Fixed-Point Arithmetic Modeled in {B} Software Using Reals},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 4th International
                  Conference, {ABZ} 2014, Toulouse, France, June 2-6, 2014. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {8477},
  pages        = {298--302},
  publisher    = {Springer},
  year         = {2014},
  url          = {https://doi.org/10.1007/978-3-662-43652-3\_28},
  doi          = {10.1007/978-3-662-43652-3\_28},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/GueryRR14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'14

Related