|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.|
|||"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)