Home
Author Guide
Editor Guide
Reviewer Guide
Special Issues
Special Issue Introduction
Special Issues List
Topics
Published Issues
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2010
2009
2008
2007
2006
journal menu
Aims and Scope
Editorial Board
Indexing Service
Article Processing Charge
Open Access Policy
Publication Ethics
Digital Preservation Policy
Editorial Process
Subscription
Contact Us
General Information
ISSN:
1796-2021 (Online); 2374-4367 (Print)
Abbreviated Title:
J. Commun.
Frequency:
Monthly
DOI:
10.12720/jcm
Abstracting/Indexing:
Scopus
;
DBLP
;
CrossRef
,
EBSCO
,
Google Scholar
;
CNKI,
etc.
E-mail questions
or comments to
editor@jocm.us
Acceptance Rate:
27%
APC:
800 USD
Average Days to Accept:
88 days
3.4
2023
CiteScore
51st percentile
Powered by
Article Metrics in Dimensions
Editor-in-Chief
Prof. Maode Ma
College of Engineering, Qatar University, Doha, Qatar
I'm very happy and honored to take on the position of editor-in-chief of JCM, which is a high-quality journal with potential and I'll try my every effort to bring JCM to a next level...
[Read More]
What's New
2024-08-20
Vol. 19, No. 8 has been published online!
2024-07-22
Vol. 19, No. 7 has been published online!
2024-06-20
Volume 19, No. 4 has been indexed by Scopus.
Home
>
Published Issues
>
2017
>
Volume 12, No. 8, August 2017
>
Formal Specification and Verification of System of Systems Using UPPAAL: A Case Study of a Defensive Missile Systems
Joon-Ha Jang
1
and Jin-Young Choi
2
1. Department of Computer Science and Engineering, Korea University, Seoul Korea
2. Graduate School of Information Security, Korea University, Seoul Korea
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.
Index Terms
—Systems of systems, system engineering, model checking, formal verification of missile defense system, UPPAAL, formal methods
Cite: Joon-Ha Jang and Jin-Young Choi, "Formal Specification and Verification of System of Systems Using UPPAAL: A Case Study of a Defensive Missile Systems," Journal of Communications, vol. 12, no. 8, pp. 482-488, 2017. Doi: 10.12720/jcm.12.8.482-488.
7-ICACTE 2018 AE007
PREVIOUS PAPER
Towards an IIoT-Based Architecture for Baggage Handling Systems
NEXT PAPER
Last page