Formal specification and verification of system of systems using UPPAAL: A case study of a defensive missile systems

Joon Ha Jang, Jin Young Choi

Research output: Contribution to journalArticle

Abstract

In this paper, we specify and verify System of Systems (SoS) using Formal Methods. As software evolved, its size and weight increased. This makes the embedded system more complex. This trend led to the concept of SoS. SoS is an integrated system, which has systems as components. This has a very large system complexity. At this time, the total system complexity is larger than each sum. Due to the complexity of the system it is very difficult to evaluate and develop the SoS appropriately. So we use system engineering. The advantages of system engineering are as follows. First, it is possible to clarify the requirements of the independent systems and the SoS requirements. Second, it is not only possible to demonstrate and evaluate independently the requirements for each system, but also to demonstrate and evaluate requirements in a SoS. At the same time, system engineering has the following challenges. First, it is difficult to simulate and model from the perspective of SoS. Second, it is difficult to verify the time constraints of SoS. In this work we try to solve this challenge using formal methods. We use model checking among Formal Methods. And we model and verify the system using a tool called UPPAAL. The reason for using UPPAAL is because the system definition of it is suitable for SoS. And because UPPAAL is suitable for verifying real-time systems. In this study, we do modelling and verify the behavior of Defensive Missile System(DMS). Through this we objectively verified the time constraints of SoS using formal methods. And we verified interoperability of DMS. And we have verified that the procedures of the DMS are logically error free and the time constraints that the DMS has. The DMS model, an implementation of our study, is reusable and extensible.

Original languageEnglish
Pages (from-to)482-488
Number of pages7
JournalJournal of Communications
Volume12
Issue number8
DOIs
Publication statusPublished - 2017

Fingerprint

Missiles
Formal methods
Systems engineering
System of systems
Formal verification
Formal specification
Model checking
Real time systems
Interoperability
Embedded systems
Computer systems

Keywords

  • Formal methods
  • Formal verification of missile defense system
  • Model checking
  • System engineering
  • Systems of systems
  • UPPAAL

ASJC Scopus subject areas

  • Electrical and Electronic Engineering

Cite this

Formal specification and verification of system of systems using UPPAAL : A case study of a defensive missile systems. / Jang, Joon Ha; Choi, Jin Young.

In: Journal of Communications, Vol. 12, No. 8, 2017, p. 482-488.

Research output: Contribution to journalArticle

@article{1609ecd57ec144bd9d37e2d734251868,
title = "Formal specification and verification of system of systems using UPPAAL: A case study of a defensive missile systems",
abstract = "In this paper, we specify and verify System of Systems (SoS) using Formal Methods. As software evolved, its size and weight increased. This makes the embedded system more complex. This trend led to the concept of SoS. SoS is an integrated system, which has systems as components. This has a very large system complexity. At this time, the total system complexity is larger than each sum. Due to the complexity of the system it is very difficult to evaluate and develop the SoS appropriately. So we use system engineering. The advantages of system engineering are as follows. First, it is possible to clarify the requirements of the independent systems and the SoS requirements. Second, it is not only possible to demonstrate and evaluate independently the requirements for each system, but also to demonstrate and evaluate requirements in a SoS. At the same time, system engineering has the following challenges. First, it is difficult to simulate and model from the perspective of SoS. Second, it is difficult to verify the time constraints of SoS. In this work we try to solve this challenge using formal methods. We use model checking among Formal Methods. And we model and verify the system using a tool called UPPAAL. The reason for using UPPAAL is because the system definition of it is suitable for SoS. And because UPPAAL is suitable for verifying real-time systems. In this study, we do modelling and verify the behavior of Defensive Missile System(DMS). Through this we objectively verified the time constraints of SoS using formal methods. And we verified interoperability of DMS. And we have verified that the procedures of the DMS are logically error free and the time constraints that the DMS has. The DMS model, an implementation of our study, is reusable and extensible.",
keywords = "Formal methods, Formal verification of missile defense system, Model checking, System engineering, Systems of systems, UPPAAL",
author = "Jang, {Joon Ha} and Choi, {Jin Young}",
year = "2017",
doi = "10.12720/jcm.12.8.482-488",
language = "English",
volume = "12",
pages = "482--488",
journal = "Journal of Communications",
issn = "1796-2021",
publisher = "Engineering and Technology Publishing",
number = "8",

}

TY - JOUR

T1 - Formal specification and verification of system of systems using UPPAAL

T2 - A case study of a defensive missile systems

AU - Jang, Joon Ha

AU - Choi, Jin Young

PY - 2017

Y1 - 2017

N2 - In this paper, we specify and verify System of Systems (SoS) using Formal Methods. As software evolved, its size and weight increased. This makes the embedded system more complex. This trend led to the concept of SoS. SoS is an integrated system, which has systems as components. This has a very large system complexity. At this time, the total system complexity is larger than each sum. Due to the complexity of the system it is very difficult to evaluate and develop the SoS appropriately. So we use system engineering. The advantages of system engineering are as follows. First, it is possible to clarify the requirements of the independent systems and the SoS requirements. Second, it is not only possible to demonstrate and evaluate independently the requirements for each system, but also to demonstrate and evaluate requirements in a SoS. At the same time, system engineering has the following challenges. First, it is difficult to simulate and model from the perspective of SoS. Second, it is difficult to verify the time constraints of SoS. In this work we try to solve this challenge using formal methods. We use model checking among Formal Methods. And we model and verify the system using a tool called UPPAAL. The reason for using UPPAAL is because the system definition of it is suitable for SoS. And because UPPAAL is suitable for verifying real-time systems. In this study, we do modelling and verify the behavior of Defensive Missile System(DMS). Through this we objectively verified the time constraints of SoS using formal methods. And we verified interoperability of DMS. And we have verified that the procedures of the DMS are logically error free and the time constraints that the DMS has. The DMS model, an implementation of our study, is reusable and extensible.

AB - In this paper, we specify and verify System of Systems (SoS) using Formal Methods. As software evolved, its size and weight increased. This makes the embedded system more complex. This trend led to the concept of SoS. SoS is an integrated system, which has systems as components. This has a very large system complexity. At this time, the total system complexity is larger than each sum. Due to the complexity of the system it is very difficult to evaluate and develop the SoS appropriately. So we use system engineering. The advantages of system engineering are as follows. First, it is possible to clarify the requirements of the independent systems and the SoS requirements. Second, it is not only possible to demonstrate and evaluate independently the requirements for each system, but also to demonstrate and evaluate requirements in a SoS. At the same time, system engineering has the following challenges. First, it is difficult to simulate and model from the perspective of SoS. Second, it is difficult to verify the time constraints of SoS. In this work we try to solve this challenge using formal methods. We use model checking among Formal Methods. And we model and verify the system using a tool called UPPAAL. The reason for using UPPAAL is because the system definition of it is suitable for SoS. And because UPPAAL is suitable for verifying real-time systems. In this study, we do modelling and verify the behavior of Defensive Missile System(DMS). Through this we objectively verified the time constraints of SoS using formal methods. And we verified interoperability of DMS. And we have verified that the procedures of the DMS are logically error free and the time constraints that the DMS has. The DMS model, an implementation of our study, is reusable and extensible.

KW - Formal methods

KW - Formal verification of missile defense system

KW - Model checking

KW - System engineering

KW - Systems of systems

KW - UPPAAL

UR - http://www.scopus.com/inward/record.url?scp=85028468625&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85028468625&partnerID=8YFLogxK

U2 - 10.12720/jcm.12.8.482-488

DO - 10.12720/jcm.12.8.482-488

M3 - Article

AN - SCOPUS:85028468625

VL - 12

SP - 482

EP - 488

JO - Journal of Communications

JF - Journal of Communications

SN - 1796-2021

IS - 8

ER -