Semantic characterization of programmable logic controller programs

被引：11

作者：

Xiao, Litian ^{[1
,2
,3
,4
]}

Wang, Rui ^{[1
,2
,3
,4
]}

Gu, Ming ^{[1
,2
,4
]}

Sun, Jiaguang ^{[1
,2
,4
]}

机构：

[1] Natl Lab Informat Sci & Technol, Beijing 100084, Peoples R China

[2] Minist Educ, Key Lab Informat Syst Secur, Beijing 100084, Peoples R China

[3] Dept Comp Sci & Technol, Beijing 100084, Peoples R China

[4] Tsinghua Univ, Sch Software, Beijing 100084, Peoples R China

来源：

MATHEMATICAL AND COMPUTER MODELLING | 2012年 / 55卷 / 5-6期

关键词：

PLC programs; Extended lambda-calculus; Program modeling; Denotational semantics;

D O I：

10.1016/j.mcm.2011.11.038

中图分类号：

TP39 [计算机的应用];

学科分类号：

081203 ; 0835 ;

摘要：

PLC is widely used in the field of automatic control. To use formal methods to verify the correctness of PLC programs, semantic characterization of PLC programs are needed. Based on the extended lambda-calculus definition, this paper presents a novel semantic modeling of PLC programs. The results lay the solid underpinnings for theorem proving and modeling checking for PLC systems. (C) 2011 Elsevier Ltd. All rights reserved.

引用

页码：1819 / 1824

页数：6

共 10 条

[1]

[Anonymous], 1981, Lecture Notes in Computer Science, DOI DOI 10.1007/BFB0025774

[2]

[Anonymous], COQ TOOLK

[3] PROVING THEOREMS ABOUT LISP FUNCTIONS [J].

BOYER, RS ;

MOORE, JS .

JOURNAL OF THE ACM, 1975, 22 (01) :129-144

[4]

John K. H., 2001, 611313 IEC

[5]

Kang B, 2005, Third ACIS International Conference on Software Engineering Research, Managment and Applications, Proceedings, P160

[6]

Lamport L., 1977, IEEE T SOFTWARE ENG

[7]

Lee E. A., 2001, P IEEE INSTR MEAS TE, P100

[8]

OWRE S, 1996, LNCS, V1102, P411

[9]

Queille J.P., 1982, LNCS, V137, P216

[10]

Zipori H., 2005, EMBEDDED SYSTEM DESI, V35, P30

← 1 →