Name
Abstract | ||
|---|---|---|
Programmable logic controllers (PLCs) represent a typical class of embedded software systems. They are widely used in safety-critical industrial applications, such as railways, automotive applications, etc. The paper presents a novel method to specify and verify PLC software systems with the theorem proving system Coq. Dependent inductive data types are harnessed to represent the component specifications. Modular and parameterized specification and verification are proposed. An illustrative example demonstrates the effectiveness of the method. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1109/TASE.2010.12 | TASE |
Keywords | Field | DocType |
plc systems,novel method,illustrative example,embedded software system,plc software system,parameterized specification,component specification,dependent inductive data type,programmable logic controller,safety-critical industrial application,automotive application,programming,formal specification,theorem proving,generators,embedded software,programmable controllers,systems analysis,software systems,embedded systems,construction industry,plc,data type | Programming language,Computer science,Systems analysis,Theorem Proving System,Formal specification,Software system,Real-time computing,Data type,Software,Programmable logic controller,Modular design | Conference |
Citations | PageRank | References |
1 | 0.39 | 3 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hai Wan | 1 | 30 | 11.84 |
| Xiaoyu Song | 2 | 318 | 46.99 |
| Ming Gu | 3 | 554 | 74.82 |