Formal methods for reconfigurable cyber-physical systems in production

被引：15

作者：

Grochowski, Marco ^{[2
]}

Simon, Hendrik ^{[2
]}

Bohlender, Dimitri ^{[2
]}

Kowalewski, Stefan ^{[2
]}

Loecklin, Andreas ^{[1
]}

Mueller, Timo ^{[1
]}

Jazdi, Nasser ^{[1
]}

Und, Andreas Zeller ^{[1
]}

Weyrich, Michael ^{[1
]}

机构：

[1] Univ Stuttgart, Inst Automatisierungstech & Softwaresyst, Pfaffenwaldring 47, D-70569 Stuttgart, Germany

[2] Rhein Westfal TH Aachen, Lehrstuhl Informat Embedded Software 11, Ahornstr 55, D-52074 Aachen, Germany

来源：

AT-AUTOMATISIERUNGSTECHNIK | 2020年 / 68卷 / 01期

关键词：

formal verification; CPS; CPPS; reconfiguration; VERIFICATION; SOFTWARE; MODEL;

D O I：

10.1515/auto-2019-0115

中图分类号：

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

学科分类号：

0812 ;

摘要：

Due to the increasing agility in the development process, shorter life cycles, and changing customer and legislator requirements, production systems must be adaptable. In addition to the ability to react flexibly to changing production requirements, the behavior of the production system must be reassured after a change. Formal verification methods are suitable for safeguarding safety-critical functions. However, this requires a high modeling effort, which inhibits the use of formal verification methods in practice. For reliable verification results, the quality and correctness of the models is decisive. Therefore, it is reasonable to analyze the underlying models. This paper presents two promising and mutually complementing approaches for the lifecycle-spanning safeguarding of production systems to overcome the challenges for the verification that a reconfiguration of the production systems brings with it during operation.

引用

页码：3 / 14

页数：12

共 34 条

[1]

Al-Safi Y, 2007, LECT NOTES ARTIF INT, V4659, P114

[2] Presentation of the 9th Edition of the Model Checking Contest [J].

Amparore, Elvio ;

Berthomieu, Bernard ;

Ciardo, Gianfranco ;

Dal Zilio, Silvano ;

Galla, Francesco ;

Hillah, Lom Messan ;

Hulin-Hubard, Francis ;

Jensen, Peter Gjol ;

Jezequel, Loig ;

Kordon, Fabrice ;

Le Botlan, Didier ;

Liebke, Torsten ;

Meijer, Jeroen ;

Miner, Andrew ;

Paviot-Adet, Emmanuel ;

Srba, Jiri ;

Thierry-Mieg, Yann ;

van Dijk, Tom ;

Wolf, Karsten .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, 2019, 11429 :50-68

[3]

[Anonymous], CYBER PHYS SYSTEMS C

[4]

Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1

[5] A Survey of Symbolic Execution Techniques [J].

Baldoni, Roberto ;

Coppa, Emilio ;

D'Elia, Daniele Cono ;

Demetrescu, Camil ;

Finocchi, Irene .

ACM COMPUTING SURVEYS, 2018, 51 (03) :1-39

[6]

Beckert Bernhard, 2015, Formal Methods and Software Engineering. 17th International Conference on Formal Engineering Methods (ICFEM 2015). Proceedings: LNCS 9407, P234, DOI 10.1007/978-3-319-25423-4_15

[7]

Bettenhausen K., 2013, TECHNICAL REPORT

[8]

Beyer D., 2017, LNCS, V10629, P99, DOI [DOI 10.1007/978-3-319-70389-3_7, 10.1007/978-3-319-70389-37, DOI 10.1007/978-3-319-70389-37, 10.1007/978-3-319-70389-3_7]

[9]

Beyer D, 2007, LECT NOTES COMPUT SC, V4590, P504

[10]

Biallas S, 2012, IEEE INT CONF AUTOM, P338, DOI 10.1145/2351676.2351741

← 1 2 3 4 →