Name
Abstract | ||
|---|---|---|
We report on a method for formally specifying and verifying programmable logic controllers (PLCs) in the specification language TLA^+. The specification framework is generic. It separates the description of the environment from that of the controller itself and its structure is consistent with the scan cycle mechanism used by PLCs. Specifications can be parameterized with the number of replicated components. In our experience, the structuring mechanisms of TLA^+ help to obtain clear, well-organized, and configurable specifications, finite instances of which are verified by the TLA^+ model checker TLC. We have validated our approach on a concrete case study, a controller for fire fighting equipment in a ship dock, and report on the results obtained for this case study. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1016/j.camwa.2010.05.017 | Computers & Mathematics with Applications |
Keywords | Field | DocType |
programmable logic controller,plc,formal specification,model checking,specification framework,case study,concrete case study,verifying plc system,ship dock,cycle mechanism,model checker tlc,finite instance,tla+,specification language,configurable specification | Specification language,Mathematical optimization,Control theory,Parameterized complexity,Model checking,Programming language,Computer science,Formal specification,Real-time computing,Programmable logic controller,Structuring | Journal |
Volume | Issue | ISSN |
60 | 3 | Computers and Mathematics with Applications |
Citations | PageRank | References |
1 | 0.38 | 2 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hehua Zhang | 1 | 109 | 12.65 |
| Stephan Merz | 2 | 741 | 59.44 |
| Ming Gu | 3 | 554 | 74.82 |