Edinburgh Research Explorer

A Super Industrial Application of PSGraph

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

Related Edinburgh Organisations

Open Access permissions

Open

Documents

https://link.springer.com/chapter/10.1007%2F978-3-319-33600-8_28
Original languageEnglish
Title of host publicationAbstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings
PublisherSpringer, Cham
Pages319-325
Number of pages7
ISBN (Electronic)978-3-319-33600-8
ISBN (Print)978-3-319-33599-5
DOIs
Publication statusPublished - 11 May 2016
EventAbstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference - Linz, Austria
Duration: 23 May 201627 May 2016
https://dl.acm.org/citation.cfm?id=2990689&picked=prox

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
Volume9675
ISSN (Print)0302-9743

Conference

ConferenceAbstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference
Abbreviated titleABZ 2016
CountryAustria
CityLinz
Period23/05/1627/05/16
Internet address

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.

Event

Download statistics

No data available

ID: 41132860