Conference icon

Conference

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
Version:
Accepted Manuscript

Actions


Access Document


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

Authors


More by this author
Institution:
University of Oxford
Department:
Oxford, MPLS, Computer Science
Role:
Author
More from this funder
Grant:
EP/J001058
EP/K503915
EP/M018407
EP/N014758
Publisher:
Springer Publisher's website
Volume:
9675
Pages:
319-325
Series:
Lecture Notes in Computer Science
Publication date:
2016-05-11
DOI:
URN:
uuid:00607f15-a96d-414f-9e67-2a4c3ac18e3e
Source identifiers:
614590
Local pid:
pubs:614590
ISBN:
9783319336008

Terms of use


Metrics


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