Automated verification of function block-based industrial control systems
| Autor: | Norbert Völker, Bernd J. Krämer |
|---|---|
| Rok vydání: | 2002 |
| Předmět: |
High-level verification
Correctness Functional verification Higher order logic business.industry Computer science Runtime verification Safety-critical control systems IEC 61131-3 Intelligent verification Compositional verification PLC programming Verification and validation of computer simulation models Verification Software engineering business Dependable software Theorem proving Algorithm Software Software verification |
| Zdroj: | Science of Computer Programming. 42:101-113 |
| ISSN: | 0167-6423 |
| DOI: | 10.1016/s0167-6423(01)00028-4 |
| Popis: | The international standard IEC 61131-3, which supports Brad Cox’ concept of “Software-ICs” for industrial control programming, is increasingly being used in safety-related application domains. They include safety-instrumented functions, such as burner management, emergency shutdown and gas leak detection, but also complex automation processes controlling, e.g., chemical production plants. For such highly dependable applications, code inspection and testing, the predominant quality assurance techniques used in practice today, are, in general, not sufficient to demonstrate the functional correctness and safety of an application. This paper presents a theorem prover-based verification technique as a supplementary validation measure. The verification task is separated into the a priori verification of reusable function blocks, which are usually maintained in domain-specific libraries, and a separate compositional proof of individual application programs. Core concepts of the standardized languages, their semantic embedding into higher order logic, and the verification approach are illustrated with a small example. Some design ideas for a verification tool usable by automation engineers and safety licensing authorities conclude the contribution. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect