Click on a search word OR use the drop-down choices to search for a paper.
2016
Newell, Joshua; Pang, Linna; Tremaine, David; Wassyng, Alan; Lawford, Mark
Formal Translation of IEC 61131-3 Function Block Diagrams to PVS with Nuclear Application Proceedings Article
In: NASA Formal Methods: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings, pp. 206–220, Springer 2016.
BibTeX | Tags: formal specification, function block diagrams, IEC 61131-3, PVS, safety critical systems, tabular expressions
@inproceedings{newell2016formal,
title = {Formal Translation of IEC 61131-3 Function Block Diagrams to PVS with Nuclear Application},
author = {Newell, Joshua and Pang, Linna and Tremaine, David and Wassyng, Alan and Lawford, Mark},
year = {2016},
date = {2016-01-01},
booktitle = {NASA Formal Methods: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings},
volume = {9690},
pages = {206--220},
organization = {Springer},
keywords = {formal specification, function block diagrams, IEC 61131-3, PVS, safety critical systems, tabular expressions},
pubstate = {published},
tppubtype = {inproceedings}
}
2015
Pang, Linna
An Engineering Methodology for the Formal Verification of Function Block Based Systems PhD Thesis
McMaster University, 2015.
Abstract | Links | BibTeX | Tags: function blocks (FBs), IEC 61131-3, PLCs
@phdthesis{Pang2015c,
title = {An Engineering Methodology for the Formal Verification of Function Block Based Systems},
author = {Pang, Linna},
url = {https://www.mcscert.ca/thesis_linna-pang-phd2015/},
year = {2015},
date = {2015-09-24},
school = {McMaster University},
abstract = {Many industrial control systems use programmable logic controllers (PLCs) since they provide a highly reliable, off-the-shelf hardware platform. On the programming side, function blocks (FBs) are reusable PLC components that can be composed to implement the required system behaviour. A higher quality system may be realized if the FBs are pre-certified to be compliant with an international standard such as IEC 61131-3. Unfortunately, the set of programming notations defined in IEC 61131-3 lack well-defined formal semantics. As a result, tool vendors and users of PLCs may have inconsistent interpretations of the expected system behaviour. To address this issue, we propose an engineering method for formally verifying the conformance of candidate implementations of FBs (and their compositions) to their high-level, input-output requirements. The proposed method is sufficiently general to handle FBs supplied by IEC 61131-3, and industrial FB applications involving real-time requirements. Our method involves several steps. First, we use tabular expressions to ensure the completeness and disjointness of the requirements for the FB. Second, we formalize the candidate implementation(s) of the FB in question. Third, we state and prove theorems regarding the consistency and correctness of the FB. All three steps are performed using the Prototype Verification Systems (PVS) proof assistant. As a first case study, we apply our approach to the IEC 61131-3 standard to examine the entire library of FBs and their supplied implementations described in structured text (ST) and function block diagrams (FBDs). As a second case study, we apply our approach to two realistic sub-systems taken from the nuclear domain. Applying the proposed method, we identified three kinds of issues: ambiguous behavioural descriptions, missing assumptions, and erroneous implementations. Furthermore, we suggest solutions to these issues.},
keywords = {function blocks (FBs), IEC 61131-3, PLCs},
pubstate = {published},
tppubtype = {phdthesis}
}
Pang, Linna; Wang, Chen-Wei; Lawford, Mark; Wassyng, Alan
Formal verification of function blocks applied to IEC 61131-3 Journal Article
In: Science of Computer Programming, vol. 113, no. Part 2, pp. 149–190, 2015.
BibTeX | Tags: critical systems, formal verification, function blocks, IEC 61131-3, tabular expression
@article{pang2015formalb,
title = {Formal verification of function blocks applied to IEC 61131-3},
author = {Pang, Linna and Wang, Chen-Wei and Lawford, Mark and Wassyng, Alan},
year = {2015},
date = {2015-01-01},
journal = {Science of Computer Programming},
volume = {113},
number = {Part 2},
pages = {149--190},
publisher = {Elsevier},
keywords = {critical systems, formal verification, function blocks, IEC 61131-3, tabular expression},
pubstate = {published},
tppubtype = {article}
}
Pang, Linna; Wang, Chen-Wei; Lawford, Mark; Wassyng, Alan; Newell, Josh; Chow, Vera; Tremaine, David
Formal Verification of Real-Time Function Blocks Using PVS Proceedings Article
In: 4th International Workshop on Engineering Safety and Security Systems 2015 (ESSS’15), pp. 65–79, Electronic Proceedings in Theoretical Computer Science 2015.
BibTeX | Tags: formal verification, function blocks, IEC 61131-3, safety-critical systems, software certification
@inproceedings{pang2015formal,
title = {Formal Verification of Real-Time Function Blocks Using PVS},
author = {Pang, Linna and Wang, Chen-Wei and Lawford, Mark and Wassyng, Alan and Newell, Josh and Chow, Vera and Tremaine, David},
year = {2015},
date = {2015-01-01},
booktitle = {4th International Workshop on Engineering Safety and Security Systems 2015 (ESSS’15)},
volume = {184},
pages = {65--79},
organization = {Electronic Proceedings in Theoretical Computer Science},
keywords = {formal verification, function blocks, IEC 61131-3, safety-critical systems, software certification},
pubstate = {published},
tppubtype = {inproceedings}
}