| 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. |
| 2011 | |
| [1] | , "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. Download article (PDF)Get article BibTeX file |