Conference item icon

Conference item

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.
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
Publisher copy:
10.1007/978-3-319-33600-8_28

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
Publisher:
Springer Publisher's website
Journal:
5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z May 23-27, 2016 Journal website
Volume:
9675
Pages:
319-325
Series:
Lecture Notes in Computer Science
Host title:
International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z
Publication date:
2016-05-11
DOI:
Source identifiers:
614590
ISBN:
9783319336008
Pubs id:
pubs:614590
UUID:
uuid:00607f15-a96d-414f-9e67-2a4c3ac18e3e
Local pid:
pubs:614590
Deposit date:
2016-04-08

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP