Abstract | ||
---|---|---|
The paper presents a tool architecture which supports the formal verification of logic controllers for processing systems. The tool's main intention is to provide a front-end for modelling the controller as well as the processing systems. The models are automatically transformed into representations which can be analysed by existing model checking algorithms. While the first part of the paper gives an overview of the complete architecture, the second part introduces a newly developed modelling interface: Process Control Event Diagrams (PCEDs) are formally defined as a suitable means to represent the flow of information in controlled processes. The transformation of PCEDs into verifiable code is described, and the whole procedure of modelling, model transformation and verification is illustrated with a simple processing system. |
Year | Venue | Keywords |
---|---|---|
2001 | JOURNAL OF UNIVERSAL COMPUTER SCIENCE | model checking,formal verification,logic controller,process control event diagram,tool development |
Field | DocType | Volume |
Applications architecture,Software engineering,Computer science,Software architecture description,Resource-oriented architecture,Software architecture,Reference architecture,Software verification and validation,Software construction,Software verification | Journal | 7 |
Issue | ISSN | Citations |
1 | 0948-695X | 2 |
PageRank | References | Authors |
0.46 | 1 | 4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Heinz Treseler | 1 | 21 | 4.61 |
Olaf Stursberg | 2 | 458 | 58.41 |
Paul W. H. Chung | 3 | 195 | 29.38 |
Shuanghua Yang | 4 | 377 | 46.40 |