Achieving delta description for the system software of an automated production evolution based on partially inferenced model (bibtex)
by Cha, Suhyun, Weigl, Alexander, Ulbrich, Mattias, Beckert, Bernhard and Vogel-Heuser, Birgit
Abstract:
Automated production systems are run for a long time with continuous and incremental changes, however, the models for aPS have not been maintained along with these system changes or, even, have not been properly generated. Even though the regression verification technique reduces the effort of applying formal verification on the automation system evolution, there still remains what should be provided in a formal form for the verification: delta, which is the difference of the two versions of the software. In this paper, we propose a method for generating a formal model from preexisting software in IEC 61131-3 Sequential Function Chart language. Based on this, the developer is able to achieve delta description by revising it to reflect the change request and this formal description of delta could facilitate verifying delta formally.
Reference:
Achieving delta description for the system software of an automated production evolution based on partially inferenced model (Cha, Suhyun, Weigl, Alexander, Ulbrich, Mattias, Beckert, Bernhard and Vogel-Heuser, Birgit), In 14th IEEE International Conference on Automation Science and Engineering (CASE), 2018.
Bibtex Entry:
@inproceedings{ChWeUl2018,
title = {Achieving delta description for the system software of an automated production evolution based on partially inferenced model},
author = {Cha, Suhyun and Weigl, Alexander and Ulbrich, Mattias and Beckert, Bernhard and Vogel-Heuser, Birgit},
year = 2018,
month = August,
address = {Munich, Germany},
booktitle = {14th IEEE International Conference on Automation Science and Engineering (CASE)},
abstract = {Automated production systems are run for a long time with continuous and incremental changes, however, the models for aPS have not been maintained along with these system changes or, even, have not been properly generated. Even though the regression verification technique reduces the effort of applying formal verification on the automation system evolution, there still remains what should be provided in a formal form for the verification: delta, which is the difference of the two versions of the software. In this paper, we propose a method for generating a formal model from preexisting software in IEC 61131-3 Sequential Function Chart language. Based on this, the developer is able to achieve delta description by revising it to reflect the change request and this formal description of delta could facilitate verifying delta formally.},
}
Powered by bibtexbrowser