WYPIWYE automation systems - an intelligent manufacturing system case study

被引：0

作者：

Park, HeeJong ^{[1
]}

Malik, Avinash ^{[1
]}

Salcic, Zoran ^{[1
]}

机构：

[1] Univ Auckland, Dept Elect & Comp Engn, Auckland 1, New Zealand

来源：

2014 IEEE EMERGING TECHNOLOGY AND FACTORY AUTOMATION (ETFA) | 2014年

关键词：

manufacturing automation; design flow; verification; SystemJ; GALS; VERIFICATION;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We present a novel approach for design of manufacturing automation systems with formal verification of selected properties based on the use of Globally Asynchronous Locally Synchronous programming language SystemJ and industrial-proof verification tools. By being able to prove properties of the automation control logic that consists of multiple concurrent controllers, represented by FSMs that correspond to asynchronous processes of SystemJ program, using Spin model checker, we demonstrate that the program features can be formally verified. Moreover, by also guaranteeing preservation of features and GALS model of the SystemJ program after compilation (correct by construction specification), we actually close the design process within What You Prove Is What You Execute (WYPIWYE) Paradigm.

引用

页数：8

共 26 条

[1]

[Anonymous], 1999, 65240CD IEC

[2]

[Anonymous], 2000, 614992 IEC

[3]

Berry G., 1993, Program Design Calculi. Proceedings of the NATO Advanced Study Institute, P361

[4]

Berry G., 1989, IFIP C

[5] Worst Case Reaction Time Analysis of Concurrent Reactive Programs [J].

Boldt, Marian ;

Traulsen, Claus ;

von Hanxleden, Reinhard .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 203 (04) :65-79

[6] Lessons from Stuxnet [J].

Chen, Thomas M. ;

Abu-Nimeh, Saeed .

COMPUTER, 2011, 44 (04) :91-93

[7]

CHRISTENSEN JH, 2000, P FACHT VERT AUT MAG, P55

[8]

Dai W., 2010, IEEE INT C EMERG, P1

[9]

Dubinin V., 2006, 2006 4th IEEE International Conference on Industrial Informatics, P6, DOI 10.1109/INDIN.2006.275709

[10]

Frey G, 2000, IEEE SYS MAN CYBERN, P2431, DOI 10.1109/ICSMC.2000.884356

← 1 2 3 →