Dependability Analysis of Logic Controller Based On Formal Verification Procedures

Authors

  • Saifulza Alwi Faculty of Electrical Engineering, Universiti Teknikal Malaysia Melaka, Hang Tuah Jaya, Melaka, Malaysia.
  • Nurrafidah Jaafar Faculty of Electrical Engineering, Universiti Teknikal Malaysia Melaka, Hang Tuah Jaya, Melaka, Malaysia.

Keywords:

Binary Decision Diagram (BDD), Computation Tree Logic (CTL), Programmable Logic Controllers (PLCs),

Abstract

Dependability of an automation system requires engineers to implement formal verification procedures in order to eliminate the causes of hazardous conditions. These conditions may vary from case to case and will jeopardize the dependability of manufacturing lines and operators. Therefore, dependability analysis of the control systems to check the possibility of state transitions from safe to unsafe states, for instance, is essential. Formal verification by using model checking procedure is proven as an effective method and widely used in practice for automatic verification of correctness properties against a finite model of a system. Therefore, in the present paper, we introduce a novel method of model checking for logic control design. A Binary Decision Diagram (BDD) based model checking method is used to analyze and design a dependable controller that meets the requirement of certain properties, defined by specified predetermined functions.

Downloads

Published

2018-01-22

How to Cite

Alwi, S., & Jaafar, N. (2018). Dependability Analysis of Logic Controller Based On Formal Verification Procedures. Journal of Telecommunication, Electronic and Computer Engineering (JTEC), 10(1-3), 153–158. Retrieved from https://jtec.utem.edu.my/jtec/article/view/3503

Issue

Vol. 10 No. 1-3: Moving Towards Industry 4.0 II

Section

Articles

License

TRANSFER OF COPYRIGHT AGREEMENT

The manuscript is herewith submitted for publication in the Journal of Telecommunication, Electronic and Computer Engineering (JTEC). It has not been published before, and it is not under consideration for publication in any other journals. It contains no material that is scandalous, obscene, libelous or otherwise contrary to law. When the manuscript is accepted for publication, I, as the author, hereby agree to transfer to JTEC, all rights including those pertaining to electronic forms and transmissions, under existing copyright laws, except for the following, which the author(s) specifically retain(s):

  1. All proprietary right other than copyright, such as patent rights
  2. The right to make further copies of all or part of the published article for my use in classroom teaching
  3. The right to reuse all or part of this manuscript in a compilation of my own works or in a textbook of which I am the author; and
  4. The right to make copies of the published work for internal distribution within the institution that employs me

I agree that copies made under these circumstances will continue to carry the copyright notice that appears in the original published work. I agree to inform my co-authors, if any, of the above terms. I certify that I have obtained written permission for the use of text, tables, and/or illustrations from any copyrighted source(s), and I agree to supply such written permission(s) to JTEC upon request.