Abstract
G4LTL-ST automatically synthesizes control code for industrial Programmable Logic Controls (PLC) from timed behavioral specifications of input-output signals. These specifications are expressed in a linear temporal logic (LTL) extended with non-linear arithmetic constraints and timing constraints on signals. G4LTL-ST generates code in IEC 61131-3-compatible Structured Text, which is compiled into executable code for a large number of industrial field-level devices. The synthesis algorithm of G4LTL-ST implements pseudo-Boolean abstraction of data constraints and the compilation of timing constraints into LTL, together with a counterstrategy-guided abstraction-refinement synthesis loop. Since temporal logic specifications are notoriously difficult to use in practice, G4LTL-ST supports engineers in specifying realizable control problems by suggesting suitable restrictions on the behavior of the control environment from failed synthesis attempts.
Chapter PDF
Similar content being viewed by others
References
International Electrotechnical Commission IEC 61131-3 Ed. 3.0: Programmable Controllers – Part 3: Programming languages. International Electrotechnical Commission, Geneva, Switzerland (2013)
Recommendations for implementing the strategic initiative - INDUSTRIE 4.0. German National Academy of Science and Engineering (AcaTech) (April 2013)
Die Deutsche Normungs-Roadmap - INDUSTRIE 4.0. DKE German Commission for Electrical, Electronic & Information Technologies (December 2013)
Bohy, A., Bruyère, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 652–657. Springer, Heidelberg (2012)
Cheng, C.-H., Ruess, H., Shankar, N.: JBernstein - a validity checker for generalized polynomial constraints. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 656–661. Springer, Heidelberg (2013)
Cheng, C.-H., Huang, C.-H., Ruess, H., Stattlemann, S.: G4LTL-ST: Automated Generation of PLC Programs (full version). arXiv:1405.2409 (2014)
Cheng, C.-H., Shankar, N., Ruess, H., Bensalem, S.: EFSMT: A Logical Framework for Cyber-Physical Systems. arXiv:1306.3456 (2013)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD, pp. 117–124. IEEE (2006)
Henzinger, T.A., Jhala, R., Majumdar, R.: Counterexample-Guided Control. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 886–902. Springer, Heidelberg (2003)
Ljungkrantz, O., Akesson, K., Fabian, M., Yuan, C.: Formal Specification and Verification of Industrial Control Logic Components. IEEE Tran. on Automation Science and Engineering 7(3), 538–548 (2010)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 36–50. Springer, Heidelberg (2005)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190. ACM (1989)
Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE (1977)
Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 474–488. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Cheng, CH., Huang, CH., Ruess, H., Stattelmann, S. (2014). G4LTL-ST: Automatic Generation of PLC Programs. In: Biere, A., Bloem, R. (eds) Computer Aided Verification. CAV 2014. Lecture Notes in Computer Science, vol 8559. Springer, Cham. https://doi.org/10.1007/978-3-319-08867-9_36
Download citation
DOI: https://doi.org/10.1007/978-3-319-08867-9_36
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08866-2
Online ISBN: 978-3-319-08867-9
eBook Packages: Computer ScienceComputer Science (R0)