Abstraction models for verifying resource adequacy of IMA systems at concept level

摘要

Complex cyber-physical systems can be difficult to analyze for resource adequacy (e.g., bandwidth and buffer size) at the concept development stage since relevant models are hard to create. During this period, details about the functions to be executed or the platforms in the architecture are partially unknown. This is especially true for Integrated Modular Avionics (IMA) systems, for which life-cycles span over several decades, with potential changes to functionality in the future. This work aims to identify abstractions for representing data exchanges among functions realized in networked IMA systems and investigates how these can be represented in formal models and analyzed with exact guarantees. Timed automata (TA) are a relevant choice for modeling since communication resource adequacy is directly related to potential network delays. We explore two alternatives in modeling with TA, a direct one representing every process using a TA template, and a more abstract one representing every computation device with a TA template. While the first approach represents process-to-process data exchanges, the modified approach reduces the state space by representing all processes currently allocated to a single computing element to obtain scalability gains. Both approaches are flexible since the templates presented can be instantiated to represent different types of network topologies and communication patterns. The instantiated TA models are used to illustrate an use case and analyzed with the UPPAAL model checker to verify that a given platform instance supports the desired system functions in terms of network bandwidth and buffer size adequacy, thereby messages reaching their final destination with freshness guarantees. Both abstraction levels are shown to be suitable for verifying the intended properties, but the more abstract one demonstrates a 67% improvement in verification time and a 66% reduction in state space during verification. The more abstract approach is also applied to a real-world example from an earlier publication, with a much larger state space and a more complex structure, to illustrate the ability to reuse the approach in multiple use cases.