최소 단어 이상 선택하여야 합니다.
최대 10 단어까지만 선택 가능합니다.
다음과 같은 기능을 한번의 로그인으로 사용 할 수 있습니다.
NTIS 바로가기정보과학회논문지. Journal of KIISE. 소프트웨어 및 응용, v.37 no.1, 2010년, pp.54 - 59
Special-purpose microcontrollers PLCs have been widely used in the area of industrial automation. For the research of analysis and verification for PLC programs, first of all we have to specify formal sematics of PLC programming languages. This paper defines formally the operational semantics of LD ...
* AI 자동 식별 결과로 적합하지 않은 문장이 있을 수 있으니, 이용에 유의하시기 바랍니다.
IEC. International Standard IEC 61131-3 Programmable controllers ? Part 3: Programming languageeees 2nd Edition International Electrotechincal Commission, 2003.
S. Shin, M. Kwon, and S. Rho, Whimori CDK: a Control Program Development Kit, The International Conference of COMPUTING in Engineering, Science and Informatics, 2009.
M. Bani Younis and G. Frey. Formalization of existing PLC Programs: A Survey Proceedings of CESA 2003 paper no. S2-R-00-0239, 2003.
O. Rossi, Ph. Schnoebelen. Formal Modelling of Timed Function Blocks for the Automatic Verification of Ladder Diagram Programs 4th Int. Conf. Automation of Mixed Processes: Hybrid Dynamic Systems pp.177-182, 2000.
I. Hatono, K. Baba, M. Umano, H. Tamura. Automatic Generation of Fault Detection Models for Programmable Constroller-Based Manufatureing Systems Using Complementary-Places Petri Nets IFAC World Congress, 1996.
S. Shin and S. Roh. Operational Semantics for Instruction List with Functions Journal of Korea Informaion Processiong Society vol.14-A, no.7, 2007 (in Korean)
Ralf Huuck. Software Verification for Programmable Logic Controllers Ph.D dissertation, Christian- Albrechts-Universitat zu Kiel, 2003.
Ben Lukoschus. Compositional Cerification of Industrial Control Systems Ph.D dissertation, Christian- Albrechts-Universitat zu Kiel, 2005.
Y. Bertot and P. Casteran. Interactive theorem proving and program development: Coq'Art : the calculus of inductive constructions Texts in theo retical computer science, Springer, 2004.
Y. Bertot. Theorem proving support in programming language semantics Research report no.6242, INRIA Sophia Antipous, 2007.
H. Wan, G. Chen, X. Song and M. Gu. Formalization and Verification of PLC Timers in Coq 33rd Annual IEEE International Computer Software and Applications Conference pp.315-323, 2009.
M. Kwon, S. Shin. Translating Ladder Diagrams into Instruction List Using Partial Order Relation KIISE KCC, 2008 (in Korean)
Coq scirpit for Formalization of Ladder Diagram Semantics, http://pllab.kut.ac.kr/Coq/ldsemantics/ldsemantics.html
※ AI-Helper는 부적절한 답변을 할 수 있습니다.