DocumentCode
555969
Title
Automated conversion of ST control programs to why for verification purposes
Author
Sadolewski, Jan
Author_Institution
Rzeszow Univ. of Technol., Rzeszów, Poland
fYear
2011
fDate
18-21 Sept. 2011
Firstpage
849
Lastpage
854
Abstract
The paper presents a prototype tool ST2Why, which converts a Behavioral Interface Specification Language for ST language from IEC 61131-3 standard to Why code. The specification annotations are stored as special comments, which are close to implementation and readable by the programmer. Further transformation with Why tool into verification lemmas, confirms compliance between specification and implementation. Proving lemmas is performed in Coq, but other provers can be used as well.
Keywords
IEC standards; formal specification; formal verification; specification languages; theorem proving; IEC 61131-3 standard; ST control program; ST language; ST2Why prototype tool; Why code; automated conversion; behavioral interface specification language; lemma proving; specification annotation; verification lemma; verification purpose; Context; Contracts; IEC standards; Java; Libraries; Reactive power; Shape;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer Science and Information Systems (FedCSIS), 2011 Federated Conference on
Conference_Location
Szczecin
Print_ISBN
978-1-4577-0041-5
Electronic_ISBN
978-83-60810-35-4
Type
conf
Filename
6078286
Link To Document