NDLI: An overview of model checking practices on verification of PLC software

Content Provider	Springer Nature Link
Author	Ovatman, Tolga Aral, Atakan Polat, Davut Ünver, Ali Osman
Copyright Year	2014
Abstract	Programmable logic controllers (PLCs) are heavily used in industrial control systems, because of their high capacity of simultaneous input/output processing capabilities. Characteristically, PLC systems are used in mission critical systems, and PLC software needs to conform real-time constraints in order to work properly. Since PLC programming requires mastering low-level instructions or assembly like languages, an important step in PLC software production is modelling using a formal approach like Petri nets or automata. Afterward, PLC software is produced semiautomatically from the model and refined iteratively. Model checking, on the other hand, is a well-known software verification approach, where typically a set of timed properties are verified by exploring the transition system produced from the software model at hand. Naturally, model checking is applied in a variety of ways to verify the correctness of PLC-based software. In this paper, we provide a broad view about the difficulties that are encountered during the model checking process applied at the verification phase of PLC software production. We classify the approaches from two different perspectives: first, the model checking approach/tool used in the verification process, and second, the software model/source code and its transformation to model checker’s specification language. In a nutshell, we have mainly examined SPIN, SMV, and UPPAAL-based model checking activities and model construction using Instruction Lists (and alike), Function Block Diagrams, and Petri nets/automata-based model construction activities. As a result of our studies, we provide a comparison among the studies in the literature regarding various aspects like their application areas, performance considerations, and model checking processes. Our survey can be used to provide guidance for the scholars and practitioners planning to integrate model checking to PLC-based software verification activities.
Starting Page	937
Ending Page	960
Page Count	24
File Format	PDF
ISSN	16191366
Journal	Software and Systems Modeling
Volume Number	15
Issue Number	4
e-ISSN	16191374
Language	English
Publisher	Springer Berlin Heidelberg
Publisher Date	2014-12-25
Publisher Place	Berlin, Heidelberg
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Model checking Programmable logic controllers Program verification Software Engineering/Programming and Operating Systems Programming Techniques Software Engineering Programming Languages, Compilers, Interpreters Information Systems Applications (incl. Internet) IT in Business
Content Type	Text
Resource Type	Article
Subject	Modeling and Simulation Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Formal verification of software source code through semi-automatic modeling

Model checking LTL properties over ANSI-C programs with bounded traces

The hidden models of model checking

Procedure-modular specification and verification of temporal safety properties

Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

Model-checking software library API usage rules

Heuristic search for equivalence checking

Automated formal verification of visual modeling languages by model checking

Model aesthetics

An overview of model checking practices on verification of PLC software

Similar Documents

Formal verification of software source code through semi-automatic modeling

Model checking LTL properties over ANSI-C programs with bounded traces

The hidden models of model checking

Procedure-modular specification and verification of temporal safety properties

Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

Model-checking software library API usage rules

Heuristic search for equivalence checking

Automated formal verification of visual modeling languages by model checking

Model aesthetics

An overview of model checking practices on verification of PLC software