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 language | English |
|---|---|
| Pages (from-to) | 482-488 |
| Number of pages | 7 |
| Journal | Journal of Communications |
| Volume | 12 |
| Issue number | 8 |
| DOIs | |
| Publication status | Published - 2017 |
Fingerprint
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 journal › Article
}
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 -