A Super Industrial Application of PSGraph

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

doi:10.1007/978-3-319-33600-8_28

A Super Industrial Application of PSGraph

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 language	English
Title of host publication	Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings
Publisher	Springer, Cham
Pages	319-325
Number of pages	7
ISBN (Electronic)	978-3-319-33600-8
ISBN (Print)	978-3-319-33599-5
DOIs	https://doi.org/10.1007/978-3-319-33600-8_28
Publication status	Published - 11 May 2016
Event	Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference - Linz, Austria Duration: 23 May 2016 → 27 May 2016 https://dl.acm.org/citation.cfm?id=2990689&picked=prox

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer, Cham
Volume	9675
ISSN (Print)	0302-9743

Conference

Conference	Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference
Abbreviated title	ABZ 2016
Country	Austria
City	Linz
Period	23/05/16 → 27/05/16
Internet address	https://dl.acm.org/citation.cfm?id=2990689&picked=prox

Access to Document

10.1007/978-3-319-33600-8_28

A Super Industrial Application of PSGraph-1Accepted author manuscript, 513 KB

https://link.springer.com/chapter/10.1007%2F978-3-319-33600-8_28

Fingerprint Dive into the research topics of 'A Super Industrial Application of PSGraph'. Together they form a unique fingerprint.

1 Finished

The integration and interaction of multiple mathematical Reasoning Processes
Bundy, A., Aspinall, D., Colton, S., Fleuriot, J., Gow, J., Grov, G., Ireland, A., Jackson, P., Mcneill, F., Michaelson, G. & Smaill, A.
EPSRC
1/11/15 → 31/10/19
Project: Research

Cite this

@inproceedings{69d11c85e6e94fe38570cc972c001f99,

title = "A Super Industrial Application of PSGraph",

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.",

author = "Yuhui Lin and Gudmund Grov and Colin O'Halloran and Priiya G.",

year = "2016",

month = may,

day = "11",

doi = "10.1007/978-3-319-33600-8_28",

language = "English",

isbn = "978-3-319-33599-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Cham",

pages = "319--325",

booktitle = "Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings",

note = "Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016 ; Conference date: 23-05-2016 Through 27-05-2016",

url = "https://dl.acm.org/citation.cfm?id=2990689&picked=prox",

}

Lin, Y, Grov, G, O'Halloran, C & G., P 2016, A Super Industrial Application of PSGraph. in Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9675, Springer, Cham, pp. 319-325, Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, Linz, Austria, 23/05/16. https://doi.org/10.1007/978-3-319-33600-8_28

A Super Industrial Application of PSGraph. / Lin, Yuhui; Grov, Gudmund; O'Halloran, Colin; G., Priiya.

Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings. Springer, Cham, 2016. p. 319-325 (Lecture Notes in Computer Science; Vol. 9675).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A Super Industrial Application of PSGraph

AU - Lin, Yuhui

AU - Grov, Gudmund

AU - O'Halloran, Colin

AU - G., Priiya

PY - 2016/5/11

Y1 - 2016/5/11

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-33600-8_28

DO - 10.1007/978-3-319-33600-8_28

M3 - Conference contribution

SN - 978-3-319-33599-5

T3 - Lecture Notes in Computer Science

SP - 319

EP - 325

BT - Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings

PB - Springer, Cham

T2 - Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference

Y2 - 23 May 2016 through 27 May 2016

ER -

A Super Industrial Application of PSGraph

Abstract

Publication series

Conference

Access to Document

The integration and interaction of multiple mathematical Reasoning Processes

Cite this