A Super Industrial Application of PSGraph

Yuhui Lin, Gudmund Grov, Colin O'Halloran, Priiya G.
Digital Printed Abstract View Cite
Type
Short Paper
Publication
5th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'16)

Abstract

The ClawZ toolset has been successful in verifying that Ada code is correctly generated from Simulink models in an industrial setting, using the Z notation. D-RisQ is now extending this technique to new domains of the C programming language, which requires changes to their highly complex proof technique. In this paper, we present initial results in the technology transfer of the graphical PSGraph language to support this extension, and show feasibility of PSGraph for industrial use with strong maintainability requirements.

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{LinGOG16,
  author       = {Yuhui Lin and
                  Gudmund Grov and
                  Colin O'Halloran and
                  Priiya G.},
  editor       = {Michael J. Butler and
                  Klaus{-}Dieter Schewe and
                  Atif Mashkoor and
                  Mikl{\'{o}}s Bir{\'{o}}},
  title        = {A Super Industrial Application of PSGraph},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 5th International
                  Conference, {ABZ} 2016, Linz, Austria, May 23-27, 2016, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9675},
  pages        = {319--325},
  publisher    = {Springer},
  year         = {2016},
  url          = {https://doi.org/10.1007/978-3-319-33600-8\_28},
  doi          = {10.1007/978-3-319-33600-8\_28},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/LinGOG16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'16

Related