Towards Industrial Formal Specification of Programmable Safety Systems

被引：9

作者：

Ljungkrantz, Oscar ^{[1
]}

Akesson, Knut ^{[1
]}

Yuan, Chengyin ^{[2
]}

Fabian, Martin ^{[1
]}

机构：

[1] Chalmers Univ Technol, Dept Signals & Syst, SE-41296 Gothenburg, Sweden

[2] GM Corp, Res & Dev, Warren, MI 48090 USA

来源：

IEEE TRANSACTIONS ON CONTROL SYSTEMS TECHNOLOGY | 2012年 / 20卷 / 06期

关键词：

Formal specification; manufacturing automation software; programmable logic controller (PLC); safety logic; software requirements and specifications; VERIFICATION;

D O I：

10.1109/TCST.2011.2169262

中图分类号：

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

学科分类号：

0812 ;

摘要：

Formal methods for specification and verification are promising in developing programmable logic controller (PLC) programs inmanufacturing industry. Particularly this holds for safety PLCs, used to protect humans and equipment from injuries and damages. An important challenge though, is the development of formal specifications, typically a tough task for control engineers. This brief proposes a systematic work procedure that can be used as a first step of developing formal specifications of safety PLC programs in industry. The work procedure intends to facilitate the development of relevant formal properties for safety PLC program components. The formal specifications can be used for automatic formal verification of the components, using model checking techniques. This brief shows how the work procedure has been applied to industrial safety components, resulting in relevant and nontrivial specifications.

引用

页码：1567 / 1574

页数：8

共 50 条

[1] A formal component concept for the specification of industrial control systems
Braatz, Benjamin
Klein, Markus
Schröter, Gunnar
Bengel, Matthias
[J]. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2004, 3147 : 69 - 88
[2] A formal component concept for the specification of industrial control systems
Braatz, B
Klein, M
Schröter, G
Bengel, M
[J]. INTEGRATION OF SOFTWARE SPECIFICATION TECHNIQUES FOR APPLICATIONS IN ENGINEERING, 2004, 3147 : 69 - 88
[3] Towards a Formal Specification Framework for Manufacturing Execution Systems
Witsch, Maria
Vogel-Heuser, Birgit
[J]. IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS, 2012, 8 (02) : 311 - 320
[4] A Survey of Formal Specification Application to Safety Critical Systems
Nanda, Smruti Priyambada
Grant, Emanuel S.
[J]. 2019 IEEE 2ND INTERNATIONAL CONFERENCE ON INFORMATION AND COMPUTER TECHNOLOGIES (ICICT), 2019, : 296 - 302
[5] Towards a formal specification for the AgentComponent
Meier, P
Wirsing, M
[J]. OBJECTS, AGENTS, AND FEATURES, 2004, 2975 : 175 - 188
[6] Contract-based formal specification of safety critical systems
Dong, W
Wang, J
[J]. Proceedings of the 29th Annual International Computer Software and Applications Conference, Workshops and Fast Abstracts, 2005, : 7 - 8
[7] Safety analysis in formal specification
Sere, K
Troubitsyna, E
[J]. FM'99-FORMAL METHODS, VOL II, 1999, 1709 : 1564 - 1583
[8] Discrete event dataflow as a formal approach to specification of industrial vision systems
Semeniuta, Oleksandr
Falkman, Petter
[J]. 2015 INTERNATIONAL CONFERENCE ON AUTOMATION SCIENCE AND ENGINEERING (CASE), 2015, : 849 - 854
[9] From the specification of multiagent systems by statecharts to their formal analysis by model checking: Towards safety-critical applications
Stolzenburg, F
Arai, T
[J]. MULTIAGENT SYSTEM TECHNOLOGIES, PROCEEDINGS, 2003, 2831 : 131 - 143
[10] Towards Formal Security Analysis of Industrial Control Systems
Rocchetto, Marco
Tippenhauer, Nils Ole
[J]. PROCEEDINGS OF THE 2017 ACM ASIA CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (ASIA CCS'17), 2017, : 114 - 126

← 1 2 3 4 5 →