Title :
Automated conversion of ST control programs to why for verification purposes
Author_Institution :
Rzeszow Univ. of Technol., Rzeszów, Poland
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;
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
