Name
Abstract | ||
|---|---|---|
Programmable logic controllers (PLCs) are widely used in embedded systems. Timers play a pivotal role in PLC real-time applications. The formalisation of timers is of great importance. The study presents a formalisation of PLC timers in the theorem proving system Coq, in which the behaviours of timers are characterised by a set of axioms at an abstract level. The authors discuss how to model timers at a proper and sound abstract level. PLC programs with timers are modelled. As a case study, a quiz machine problem with a timer is investigated. This work demonstrates the complexity of formal timer modelling. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1049/iet-sen.2010.0002 | Software, IET |
Keywords | Field | DocType |
formal verification,programmable controllers,PLC,PLC formalisation,PLC verification,abstract level,embedded system,formal timer modelling,programmable logic controllers timer,theorem proving system | Computer science,Axiom,Automated theorem proving,Theorem Proving System,Proof theory,Real-time computing,Programmable logic controller,Timer,Formal verification,Embedded system | Journal |
Volume | Issue | ISSN |
5 | 1 | 1751-8806 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hai Wan | 1 | 30 | 11.84 |
| Gang Chen | 2 | 20 | 5.21 |
| Xiaoyu Song | 3 | 318 | 46.99 |
| Ming Gu | 4 | 554 | 74.82 |