Complex cyber-physical systems can be difficult to analyze for resource adequacy 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. To support the engineers evaluating conceptual designs there is a need for tools that model resources of interest in an abstract manner and allow analyses of changing architectures in a modular and scalable way. This work presents a generic timed automata-based model of a networked IMA system abstracting complex networking and computational elements of an architecture, but representing the communication needs of each application function using UPPAAL templates. The proposed model is flexible and can be modified/extended to represent different types of network topologies and communication patterns. More specifically, the different components of the IMA network, Core Processing Modules, Network End-Systems, and Switches, are represented by different templates. The templates are then instantiated to represent a conceptual design, and fed into a model checker to verify that a given platform instance supports the desired system functions in terms of network bandwidth and buffer size adequacy - in particular, whether messages can reach their final destination on time. The work identifies the limits of the tool used for this evaluation, but the conceptual model can be carried over to other tools for further studies.

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. (C) 2021 The Authors. Published by Elsevier B.V.

Analyzing the resource adequacy of complex cyber-physical systems at concept development stage can be a challenging task since there are a lot of uncertainties about the system at this stage. In Integrated Modular Avionics (IMA) systems, with a life-cycle over several decades and potential functionality changes, we need to estimate resource needs at the early stage but leave capacity to absorb future modifications. Given an envisaged set of functions and a mapping to a candidate platform, one needs to assure that the selected network configuration will provide adequate resources to meet communication timeliness. In particular, whether the set of switches, the topology, and the available bandwidth are sufficient to meet the envisaged needs. In this paper, timeliness requirements are expressed as constraints on the freshness of data and a strict bounding of end-to-end latency. We support generation of UML/MARTE-based specifications by creating a domain-specific meta-model for IMA systems and a resource modelling approach for the study of time-critical systems. The instances of this model then specify the application requirements and various network configurations that can be formally analyzed. We present a tool, M2NC, for automatic derivation of a network calculus model through model transformation, and use the state-of-art NC tools for deriving the bounds for end-to-end timeliness. The approach is illustrated on an example avionics case study, consisting of 91 computational processes that exchange 629 different types of messages. The results of the analysis show that our approach can efficiently provide feedback on configurations that are compliant with the requirements imposed by the application and the toolchain provides a systematic mechanism to quickly identify potential future bottlenecks.

During the concept design of complex networked systems, concept developers have to ensure that the choice of hardware modules and the topology of the target platform will provide adequate resources to support the needs of the application. For example, future -generation aerospace systems need to consider multiple requirements, with many trade-offs, foreseeing rapid technological change and a long period for realization and service. For that purpose, we introduce NetGAP, an automated 3 -phase approach to synthesize network topologies and support the exploration and concept design of networked systems with multiple requirements including dependability, security, and performance. NetGAP represents the possible interconnections between hardware modules using a graph grammar and uses a Monte Carlo Tree Search optimization to generate candidate topologies from the grammar while aiming to satisfy the requirements. We apply the proposed approach to a synthetic version of a realistic avionics application use case. It includes 99 processes and 660 messages. The experiment shows the merits of the solution to support the early -stage exploration of alternative candidate topologies. The method vividly characterizes the topology -related trade-offs between requirements stemming from security, fault tolerance, timeliness, and the "cost'' of adding new modules or links. We also create a scaled -up version of the problem (267 processes, 1887 messages) to illustrate scalability. Finally, we discuss the flexibility of using the approach when changes in the application and its requirements occur.

In this paper, we apply a grammar-based approach to generate computation and communication platforms for avionic applications with mixed classes of time-sensitive communication messages. Then, we propose an evolutionary algorithm to schedule communication in the platform considering the interaction between timetriggered and bandwidth-constrained traffic. Together, the platform generation approach and the scheduling algorithm support the exploration of avionic systems at the concept level.