e-Informatica Software Engineering Journal Conversion of ST Control Programs to ANSI C for Verification Purposes

Conversion of ST Control Programs to ANSI C for Verification Purposes

Jan Sadolewski
Abstract
The paper presents a Behavioral Interface Specification Language for control programs written in ST language of IEC 61131-3 standard. The specification annotations are stored as special comments in ST code. The code and comments are then converted into ANSI C form for further transformation with Caduceus and Why tools. Verification of compliance between specification and code is performed in Coq.
[1]Jan Sadolewski, "Conversion of ST Control Programs to ANSI C for Verification Purposes", In e-Informatica Software Engineering Journal, vol. 5, pp. 65–76, 2011. DOI: 10.2478/v10233-011-0031-3.

Get article (PDF)View article entry (BibTeX)

©2015 e-Informatyka.pl, All rights reserved.

Built on WordPress Theme: Mediaphase Lite by ThemeFurnace.