Safety & Security Analysis of a Manufacturing System using Formal Verification and Attack-Simulation

Eun Young Kang*, Simon Hacks

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


Key to reliable manufacturing systems is ensuring the trustworthiness of the decision-making and control mechanisms that supplant human control, i.e., systems need to remain safe while being resilient against functional failures, unpredictable changes, and cyber-security threats. We present a correct-by-construction approach to identify and analyze essential requirements that ensure the safety and security of a manufacturing system using a combination of System Theoretic Process Analysis (STPA)-based verification and attack simulation. This approach utilizes formal modeling and analysis to remove ambiguities in the requirement and specify safety properties that should be satisfied in system design. Potential safety hazards are identified using STPA-based model checking and possible cyber-security threats are diagnosed through attack simulation. Additional safety and security constraints inhibiting the hazards and threats are generated to improve the system design accordingly. Our approach is demonstrated on an autonomous assembly line system case study.

Original languageEnglish
Title of host publication2023 12th Mediterranean Conference on Embedded Computing (MECO)
Number of pages8
Publication date2023
ISBN (Electronic)9798350322910
Publication statusPublished - 2023
Event12th Mediterranean Conference on Embedded Computing, MECO 2023 - Budva, Montenegro
Duration: 6. Jun 202310. Jun 2023


Conference12th Mediterranean Conference on Embedded Computing, MECO 2023
SeriesMediterranean Conference on Embedded Computing, MECO


  • Attack simulation
  • Formal verification
  • Safety
  • Security
  • STPA


Dive into the research topics of 'Safety & Security Analysis of a Manufacturing System using Formal Verification and Attack-Simulation'. Together they form a unique fingerprint.

Cite this