A Super Industrial Application of PSGraph

Yuhui Lin, Gudmund Grov, Colin O'Halloran, G. Priiya

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

2 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationAbstract State Machines, Alloy, B, TLA, VDM, and Z
Subtitle of host publication5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings
EditorsM. Butler, K.-D. Schewe, A. Mashkoor, M. Biro
PublisherSpringer International Publishing
Pages319-325
Number of pages7
ISBN (Electronic)9783319336008
ISBN (Print)9783319335995
DOIs
Publication statusPublished - 2016
Event5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z 2016 - Linz, Australia
Duration: 23 May 201627 May 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
Volume9675
ISSN (Print)0302-9743

Conference

Conference5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z 2016
CountryAustralia
CityLinz
Period23/05/1627/05/16

Cite this

Lin, Y., Grov, G., O'Halloran, C., & Priiya, G. (2016). A Super Industrial Application of PSGraph. In M. Butler, K-D. Schewe, A. Mashkoor, & M. Biro (Eds.), Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings (pp. 319-325). (Lecture Notes in Computer Science; Vol. 9675). Springer International Publishing. https://doi.org/10.1007/978-3-319-33600-8_28