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:
-
-
(Preview, Accepted manuscript, pdf, 317.5KB, Terms of use)
-
- Publisher copy:
- 10.1007/978-3-319-33600-8_28
Authors
- Publisher:
- Springer
- Host title:
- International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z
- Journal:
- 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z May 23-27, 2016 More from this journal
- Volume:
- 9675
- Pages:
- 319-325
- Series:
- Lecture Notes in Computer Science
- Publication date:
- 2016-05-11
- DOI:
- ISBN:
- 9783319336008
- Pubs id:
-
pubs:614590
- UUID:
-
uuid:00607f15-a96d-414f-9e67-2a4c3ac18e3e
- Local pid:
-
pubs:614590
- Source identifiers:
-
614590
- Deposit date:
-
2016-04-08
- ARK identifier:
Terms of use
- Copyright holder:
- © Springer International Publishing Switzerland 2016
- Copyright date:
- 2016
- Notes:
-
© Springer International Publishing Switzerland 2016. This is the author accepted manuscript following peer review version of the article. The final version is available online from Springer at: 10.1007/978-3-319-33600-8_28.
This is a conference paper presented at the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, 23-27 May 2016
If you are the owner of this record, you can report an update to it here: Report update to this record