Formal Specification and Verification of System of Systems Using UPPAAL: A Case Study of a Defensive Missile Systems

摘要

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 verily 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.