{"references": ["IEC 61131-3:2013 Programmable controllers \u2013 Part 3: Programming languages, IEC Std., 2013.", "E. Blanco Vi\u00f1uela et al., \u201cUNICOS evolution: CPC version 6,\u201d in Proc. of the 12th Int\u2019l Conf. on Accelerator & Large Experimental Physics Control Systems, 2011, pp. 786\u2013789.", "B. Fern\u00e1ndez Adiego, D. Darvas, J.-C. Tournier, E. Blanco Vi\u00f1uela, and V. M. Gonz\u00e1lez Su\u00e1rez, \u201cBringing automated model checking to PLC program development \u2013 A CERN case study,\u201d in Proc. of the 12th Int\u2019l Workshop on Discrete Event Systems. IFAC, 2014, pp. 394\u2013399.", "IEEE Std 830-1998 Standard, IEEE Computer Society Std., 1998.", "A. van Lamsweerde, \u201cFormal specification: A roadmap,\u201d in Proc. of the Conf. on The Future of Software Engineering. ACM, 2000, pp. 147\u2013159.", "J. C. Knight, C. L. DeJong, M. S. Gibble, and L. G. Nakano, \u201cWhy are formal methods not used more widely?\u201d in 4th NASA Langley Formal Methods Workshop, 1997, pp. 1\u201312.", "D. Harel, \u201cStatecharts: a visual formalism for complex systems,\u201d Science of Computer Programming, vol. 8, no. 3, pp. 231\u2013274, 1987.", "D. Harel, \u201cStatecharts in the making: A personal account,\u201d in Proc. of the Third ACM SIGPLAN Conf. on History of Programming Languages. ACM, 2007, pp. 5\u20131\u20135\u201343.", "M. Heimdahl, N. Leveson, and J. Reese, \u201cExperiences from specifying the TCAS II requirements using RSML,\u201d in Proc. of the 17th AIAA/IEEE/SAE Digital Avionics Systems Conf., vol. 1, 1998, pp. C43/1\u2013C43/8.", "S. Teufl, M. Khalil, and D. Mou, \u201cRequirements for a model-based requirements engineering tool for embedded systems: Systematic literature review and survey,\u201d fortiss GmbH, White Paper, 2013.", "IEC 60848:2013 \u2013 GRAFCET specification language for sequential function charts, International Electrotechnical Commission Std., 2013.", "J. Provost, J.-M. Roussel, and J.-M. Faure, \u201cA formal semantics for Grafcet specifications,\u201d in IEEE Conf. on Automation Science and Engineering, 2011, pp. 488\u2013494.", "O. Ljungkrantz, K. \u00c5kesson, M. Fabian, and C. Yuan, \u201cA formal specification language for PLC-based control logic,\u201d in Proc. of the 8th IEEE Int\u2019l Conf. on Industrial Informatics, 2010, pp. 1067\u20131072."]}

One of the main obstacles of using formal verification for complex PLC (Programmable Logic Controller) programs is the lack of formal requirements. There are no widely used specification methods that could serve as input for formal verification; also that could help the developers to capture the behaviour and handle the complexity of these programs. The goal of this research is to bring formal specification closer to the PLC domain in order to help the development, verification and maintenance. This paper aims to briefly overview the particularities of the PLC domain and the state of the art in formal specification. Then it collects the requirements towards a PLC-specific formal specification language based on general works, comparative case studies and own experiences at CERN. Also, it draws up a sketch of a possible specification method that follows the collected requirements.