Name
Abstract | ||
|---|---|---|
In this paper, we developed a format for the specification of PLC systems using the specification language TLA+. Correctness properties for TLA+ specifications can be verified using the TLC model checker. The format we propose clearly distinguishes between user actions, system actions, and plant feedback. The different categories of actions are specified separately by TLA+ action formulas, which are then composed to form the overall specification. This separation makes us confident that we avoided overspecification, in particular of the environment. Working in a high-level language such as TLA+ allows a designer to focus on the essential features of a system specification. It also helps to avoid low-level encodings, which combined with parameterization leads to configurable and concise specifications. The resulting models can nevertheless be analyzed by the TLA+ model checker in a reasonable amount of time. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1016/j.camwa.2010.05.017 | Computers & Mathematics With Applications |
Keywords | Field | DocType |
programmable controllers,programmable logic controller,tla+,verifying plc systems,configurable specification,system action,finite instance,model checking,specification languages,specification language,model checker tlc,plc,high-level language,temporal logic of actions,concrete case study,system specification,case study,action formulas,tla+ specification,structuring mechanism,tlc model checker,temporal logic,user action,correctness properties,ship dock,cycle mechanism,formal specification,plant feedback,plc system,high level language,feedback,valves,logic,writing,reactive power,software engineering,data mining,embedded software,formal specifications | Specification language,Control theory,Programming language,Temporal logic of actions,Model checking,Computer science,Real-time computing,Formal specification,Programmable logic controller,Temporal logic,System requirements specification | Conference |
Volume | Issue | ISSN |
60 | 3 | 0898-1221 |
ISBN | Citations | PageRank |
978-0-7695-3757-3 | 1 | 0.45 |
References | Authors | |
2 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hehua Zhang | 1 | 109 | 12.65 |
| Stephan Merz | 2 | 741 | 59.44 |
| Ming Gu | 3 | 554 | 74.82 |