Online monitoring and model-based validation are commonly accepted quality assurance measures for mission critical systems. We propose an integrated approach where the Multi-Fragment Markov Models (MFMM) are used for specifying the system reliability and security related behavior on high-level of abstraction, and the more concrete state and timing constraints related with MFMM are speci ed explicitly using Uppaal Probabilistic Timed Automata (UPTA). To interrelate these two model classes we demonstrate how the MFMM is mapped to UPTA. The second contribution is the test case selection mechanism for online testing where the test cases are prioritized by probabilities of execution modes. The hypotheses on which mode the system switches next are provided by MFMM and the hypotheses are tested using UPTA models that specify the mode behavior forming a test suite for online conformance testing of modes. The approach is illustrated with the Bon re Multi-Processor System-on-Chip.
The spacecraft systems are inherently mission critical. Their veri cation can be
undertaken during several di erent stages [
Following from the results presented in [
Online monitoring and model-based validation techniques are commonly
accepted quality assurance measures for mission critical systems. Online testing is
considered to be the most appropriate technique for MBT of embedded systems
where the implementation under test (IUT) is modeled using nondeterministic
models [
If the critical system behavior is complex it is hard or practically impossible to predict all potential causes why the system can deviate from its speci ed behavior, e.g. would it be due to the bugs, hardware faults or cyber-attacks, unexpected load pro les or other reasons that have impact on systems QoS. Therefore, in model-based approaches the causal relations are often approximated with probabilistic ones. On the other hand, for error detection and correction the online veri cation of design correctness should explore the more concrete state space for explicit conditions under which the faults expose.
We propose an integrated approach with Multi-Fragment Markov Models
(MFMM) [
The second contribution is the test case selection mechanism for online testing which prioritizes the test cases by probabilities of modes to be con rmed by online testing. The hypotheses on which mode the system switches next are provided by MFMM and the hypotheses are tested by running conformance tests against the UPTA models that specify the mode to be identi ed.
The approach is illustrated with the Bon re Multi-Processor System-on-Chip
(MPSoC) example maintained as an open-source project, available at [
Markov chains is a well established model-based analytical tool for understanding
stochastic systems behavior [
Related to the integration of Markov models and system MBT approaches,
several works exist for improving the testing e ciency. For example one of the
rst works presented a method for statistical testing based on a Markov chain
model of software usage [
Corresponding testing methodology for the automotive domain is presented
by Siegl et al. [
All the aforementioned works are concerned with o ine MBT while our approach is targeting online MBT. This provides the mechanism of e cient veri cation by conformance testing the hypothesis about system current mode predicted by the Markov model. To the best of authors' knowledge this is the rst work to combine Markov models and UPTA for model checking and online MBT. 3
The state-based explosion problem experienced by many model-based o ine test generation methods is avoided by the online techniques because only a limited part of the state-space needs to be kept track of when a test is running. However, exhaustive planning would be di cult on-the- y because of the limitations of computational resources at the time of test execution. Thus, developing a planning strategy for online testing should address the trade-o between reaction time and online planning depth to reach the practically feasible test cases.
The simplest approach to on-the- y selection of test stimuli in online MBT
is to apply so called random-walk strategy where no computation sequence of
IUT has an advantage over the others. The test is performed usually to discover
violations of input/output conformance relation IOCO [
In order to overcome the de ciencies of long lasting testing usually additional
heuristics, e.g. \reactive planning tester" [
Another option for reducing the online test generation and planning overhead is to partition the test models into smaller ones where the test cases do not need the full blown model coverage. Following this idea we de ne in this paper the test models by system availability modes so that each of the test models re nes only one state (availability mode) of the abstract Markov model. By reducing the size of test models in this way we can apply simple random-walk strategy instead of those that require computationally expensive state space exploration. 4
Kharchenko et al. [
For the work in this paper we are concerned with scenarios SC3 and SC4. The availability model corresponding to these scenarios is presented in Fig. 1. The model includes a set of states and transitions caused by failures and repairs of hardware and software and possibilities of failure detection and system repair. There is a tree-like graph of transitions; the type of transition depends on the type of event occurred: detecting of fault or start of veri cation process. The graph models for scenarios SC3 and SC4 are equal; scenario SC4 models additionally the degradation of system functions. Thus, the probability of transition into the state of veri cation (and detecting of fault) may be higher for scenario SC4. In Fig. 1 failure rate of both software and hardware is represented by .
The availability model for the Bon re MPSoC inspired by this Markov-chain based availability model will be presented and discussed in Section 6. 5
Uppaal Timed Automata (UTA) [
Uppaal Probabilistic Timed Automata (UPTA) [
The Bon re MPSoC employs a Network-on-Chip with a 2D mesh topology. Each router uses wormhole switching equipped with fault tolerant mechanisms. A processor is connected to each router via a network interface. The router comprises of an input bu er, a routing computation unit, a switch allocator granting requests to the same output based on Round-Robin policy and a crossbar switch to forward the packets. An abstract view of Bon re is presented in Fig. 2. a. For this paper we are considering an instantiation of the platform with four processors and four routers. Since the routing mesh of Bon re is the IUT the availability of which is studied in this paper, the test interface (denoted by dashed line in Fig 2. a) is de ned by the interfaces between the network interfaces and routers, i.e., the processors constitute an environment for the IUT.
The availability model for Bon re is shown in Fig. 2. b. Note that for simplicity we do not present a Multi-Fragment Markov model. Naturaly the multiple fragments expand to the right of the rst fragment after software corrections. It is assumed that the right-most fragment would not include any software faults. The single fragment model of Fig. 2. b is adequate to be used for the presentation of our integrated approach in this paper. The area within the dashed lines in Fig. 2. b corresponds to the part of the Markov model which will be mapped to UPTA for modeling of the mode switching and for stochastic model checking.
Initially the system implements all functions according to the speci cation and stays at the S0, normal operational mode. Due to possible hardware (physical) faults the system can transit to modes S1 and S2 which model the degraded and low operational modes we have de ned for this case study. State S3 models the System Down mode where the system is not operable anymore. Due to possible recovery functions the system operation can be restored from other states. Moreover, in each operational mode, system failure might occur due to software (design) fault causing the system to transit to state S4. This transition is executed when the process of online MBT (which is applicable in each operational mode) has detected a software fault. The online MBT process corresponds to the veri cation process shown in the lower part of Fig. 1. For clarity it is not shown explicitly in Fig. 2. b. We assume that the system software can be corrected by some means, e.g. software update (not shown in Fig. 2. b), and the system can then transit back to any of the operational modes where the fault occured.
The UPTA model corresponding to the Markov Bon re model is presented in Fig. 3. a. The transitions of the Markov model in Fig. 2. b are mapped to probabilistic transitions (denoted by dotted line and labeled with probabilities) of UPTA shown in Fig. 3. a. The probabilities of UPTA are computed based on failure rates of Fig. 2. b. They specify the probabilities of events that cause transition from one mode to another. The probabilities of events that trigger transitions are normalized with respect to the model time unit denoted by tu. Combining the probabilities with explicit clock constraints in the model of Fig. 3.a is needed for SMC of timing properties.
The UPTA automata that interface the abstract availability model in Fig. 3.a with detailed mode behavior models are shown in Fig. 3.b. Initially all automata are in location Passive waiting for synchronisation from the Mode switching automaton. Upon synchronisation they will either return back to the Passive location or the relevant internal behavior of a mode will be triggered. Locations Actions of Mn, Actions of Md and Actions of Ml represent respectively each mode which are elaborated in the next subsections. 7
We have created the models of the main components of the Bon re MPSoC platform, namely, the processor and the router considering an instantiation of the platform with four processors and four routers. These models can be used for online MBT for each di erent operational mode of the system. The processor component model comprises the behavioral view that is assumed to be unchanging throughout the modes and the router component models comprise the behaviors in normal, degraded and low mode that represent respectively functioning under ideal conditions, the reliability and security views. Here by views we mean design views which should be consistent with each other to ensure the soundness of design.
The reliability view concerns the probability of data packet transmission failure on any link between processors and routers as well as between the routers. The security view concerns the possibility of cyber attack to some processor after which the attack should be detected by the tra c pattern generated by this processor and the attacked processor should be blocked. Note that the timing view is implicitly conjoined with the aforementioned views due to the modeling formalism. Thus, in this paper the behavioral view of Bon re relates to the normal operational mode of the system, the reliability view relates to the degraded mode with all processors still operating and the security view relates to the low mode. If more than one processors are blocked then the system is shut down. 7.1
The UPTA templates representing the behavioral view of the processors and routers are shown in Fig. 4 a and Fig. 4 b, respectively. The environment to the routing system consists of four processors which are instantiated with four processes, each sending and receiving frames to and from the routing system. The routing system is modeled as UPTA processes parameterized with source and destination router id-s respectively. The router template speci es (i) the case where there is no frame in its input queue (the edge from W ait location down) and (ii) the case where there is at least one frame in the input queue to be forwarded to the next router (the edge from W ait location to right and its subsequent edges and locations reachable before return to location W ait).
The composed model of the behavioral view represents design assumptions A1 to A10 and guarantees G1 to G3 of routing as follows. A1 - Processors are indexed clock-wise from 0 to 3 in the mesh and denoted respectively with Pi, where i : [0; 3]. The same holds for local routers Ri; A2 - Processors communicate by sending and receiving frames; A3 - Any processor Pi can send at most one frame per tu to its local router Ri; A4 - Any pair of neighbor routers has direct communication link in two directions, a link(i; j) denotes a link from Ri to Rj and link(j; i) a link from Rj to Ri, where each link link(i; j) has a bu er buf (i; j) to store the frame postponed due to congestion; A5 - An oldest element in the bu er buf (i; j) is forwarded along the link link(i; j); A6 - Bu er emptiness is checked and content sent once at any tu; A7 - A frame is written by router Ri to bu er buf (i; j) of its outgoing link link(i; j) during the same tu when it is read from some of its incoming link link(k; i); A8 - Congestion rises when the frames of di erent incoming links link(i; j) and link(k; j) of router Rj arriving in the same tu need to be forwarded along the same outgoing link link(j; l); A9 - The congestion can rise at most between two incoming links in one tu; A10 The frames are identi ed by their source and destination processor id-s.
The explicit design guarantees for the processors and routers are as follows. G1 - Any frame sent from a processor Pi does not have congestion on any link with some other frame sent from the same processor Pi; G2 - The frames once routed along link(i; j) are never routed backwards along link(j; i); G3 - In the routing system satisfying assumptions A1 to A10 any frame can be routed to its destination with at most three hops, i.e. one along local link and two along links between routers while the congestion can occur in inter router link only. We additionally assume that the frames are never sent to the processor itself and reading a frame by processor from the routing system never blocks.
Each router in normal mode implements the design assumptions A4 A7 and provides the guarantees G2, G3 and ensures that no package loss occurs. 7.2
The UPTA template for the reliability view of the system is presented in the upper part of Fig. 5. While the processor template remains the same, the routing template for the reliability view extends the behavioral view assumptions with the assumptions about the correct delivery of the frame over the link between routers is p and frame transmission failure with probability 1 p. The re nement of the edge with label \Forward the frame" with two alternative outcomes - one for successful and the other for failure of transmission between a pair of routers introduces probabilities p and 1 p respectively of these options. The guarantees G2 and G3 still hold. The probability of packet delivery with two hops and with the same upper time bound as in behavioral view is p2. 7.3
The UPTA model template for the security view of the system is presented in the lower part of Fig. 5. The assumptions of the security view maintain the assumptions of the behavioral view regarding writing and reading frames to and from processors. The assumptions are extended with the possibility of cyber attack resulting in the corruption of processor code in one of the processors P0 P3. We have to introduce a new guarantee G4 which ensures that the detection of the attack occurs at latest during r tu after corrupted code is activated in a processor Px. The detection is implemented by monitoring the tra c between a processor Px and its local router Rx, i.e the frames sent over link(x; x) (see edge < s1 1; s1 2 > in the template).
Another guarantee related to attacks is G5 which ensures that the processor Px under attack (with corrupted code) should not interfere with the functioning of the routing system including Rx. This is implemented as follows: when the number of consecutive sends from processor Px to some processor Pj exceeds a threshold value r then Boolean variable attack is assigned the value true causing the link link(x; x) from Px to Rx to be blocked for further communication with Px (edge < W ait; s1 1 > is not enabled). Note that router Rx can still forward packages from other routers. 7.4
Proving the correctness of the model of the IUT means that the guarantees of the routing system design need to be veri ed provided the assumptions A1 to A10 are properly implemented and represented in the design models as of Fig 4 to Fig 5. In the following we introduce some examples of integral QoS related assume-guarantee properties that rely on above mentioned design assumptions and guarantees.
For the behavioral view, property i) states that any frame sent from processor Pi to Pj for i; j = 0; :::; M 1 where i 6= j, will reach its destination at most with t k time units. Property ii) states that under given environment assumptions (including the contention mode) the length of message queue buf (i; j) at any link(i; j) does not exceed the bu er size BS.
For the reliability view, property i) states that any frame sent from processor Pi to Pj for i; j = 0; :::; M 1 where i 6= j, will reach its destination during k time units with probability p k. Property ii) states that under given environment assumptions (message loss rate) the length of message queue buf (i; j) at any link (i; j) does not exceed the bu er size BS with probability p l.
For the security view, property i) states that the maximum time of cyber attack detection and mitigation (processor blocking) has upper bound. Property ii) states that in case of attack the maximum package delivery time of remaining routing system does not drop below t k time units. 7.5
Let us elaborate on the veri cation of the interrelated properties regarding the sending of data frames to their destination address of the views that could interfere. Similar reasoning holds for the veri cation of the interrelated properties regarding the bu er size for the behavioral and reliability views.
For verifying property i) of the behavioral view we construct a property recognizing automaton by applying a \Stopwatch" UPTA template (see Fig. 6) and compose it with the behavioral model by synchronizing Stopwatch start action with frame send action from processor Pi to router Ri and stop action with receive action when the frame is sent to link Rj Pj . There are several veri cation assumptions as follows. Since the routing architecture is North-South and East-West symmetric, the maximum transport delay can be measured from any processor Pi to processor Pj where i 6= j and Pi and Pj are in the mesh opposite diagonal corners. Veri cation of Pi to Pj transport delay can be done w.r.t. any generated single frame separately without considering the full ow from same Pi because of G1. Frame generation time instant T gen at Pi can vary from 0 to load stabilization time in the routing system. Time out T out, i.e the upper time bound we check can be 6 since due to the topology maximum 2 hops should be performed to reach the destination and each hop may have one congestion at most due to G2 (to one link i; j, where i 6= j only Pi and Ri can compete). To identify the receive event for model checking end-to-end transfer time we have to encode also the sender address Pi in the traceable frame. So we use encoding of frames as a pair of constants where the rst corresponds to source address and the second to destination address. AB means P0 sends to P1, DB means P3 sends to P1, etc.
Stopwatch automaton is used for verifying the guarantee that the end-toend delay upper bound is T out. This is proven by model checking MB j= A Stopwatch:P ass.
In addition to the veri cation scheme for property i) of the behavioral view, property i) of the reliability view for successful end-to-end delivery needs to be calculated by adding an update: p route = p route pij , to each router process transition labeled with \Forward the frame" where pij denotes the probability of successful transmission over link(i; j) provided the link is on the route. Under the assumptions of the given view the validity of the guarantee of the property is veri ed by checking MRel j= A Stopwatch:P ass && p route >= p k.
Similarly to verifying property i) of the behavioral view, the model checking task for verifying interrelated property ii) of the security view is MSec j= A Stopwatch:P ass. 8
In the case of online test generation the model is executed in lock step with the
IUT. The communication between the model and the IUT involves controllable
inputs of the IUT and observable outputs of the IUT. For UPTA there exists the
online MBT tool Uppaal Tron [
The overall test setup used in the context of MBT with Uppaal Tron as the test engine and dTron [1] as the adapter generation framework is given in Fig. 7. The test model represents symbolically the interaction between IUT and its environment components. The test adapter is responsible for translating symbolic I/O of the test model to frames passed to the routing system and mapping the frames received at the destination processor back to model symbolic output. The dTron layer allows the adapters to be distributed over the routing system ports while ensuring that measuring the model time is in synchrony with physical clocks at I/O ports.
The test con guration used in the current work consists of test execution environment dTron and one test adapter per processor-router link that transforms abstract input/output symbols of the model to input/output data of the IUT. The setup is outlined in Fig. 7. Uppaal Tron is used as a primary test execution engine which simulates symbolic interactions between the IUT and its environment. The interactions are monitored during model execution. When the environment (one of the processors in the model) initiates an input action i Tron triggers input data generation in the adapter and the actual test data is written to the IUT (implemented routers) interface. In response to that, the receive event at destination processor port produces output data that is transformed back to symbolic output o. Thereafter, the equivalence between the real output returned and the output o speci ed in the model is checked. The run continues if there is no conformance violation, i.e. there exists an enabled transition in the model with parameters equivalent to those passed by the IUT. In addition to input/output conformance, the real-time input/output conformance is checked by Uppaal Tron. 9
In this paper we have addressed the online monitoring and model-based validation techniques for mission critical systems. We propose an integrated approach where the MFMM are used for specifying the system reliability and security related behavior on high-level of abstraction relevant for Markov analysis, and the more concrete state and timing constraints related with MFMM are speci ed explicitly using UPTA for stochastic modeling and model-based test generation. To interrelate these two model classes we have shown the mapping from MFMM to UPTA. The second contribution is the test case selection mechanism for online testing where the test cases are prioritized by the probabilities of modes. The hypotheses on which mode the system switches next are provided by MFMM and the hypothesis are tested by conformance tests using UPTA models that specify the mode behavior. The approach is illustrated with the Bon re MPSoC where the probabilistic model checking of high-level mode switching scenarios is applied on MFMM. A set of UPTA models that re nes the behavior of MFMM modes is applied thereafter as a test suite for model-based conformance testing to con rm the hypothesis of being in the given mode.
As future work, more practical experiments are planned for quantitative analysis to estimate how much the probability guided online testing shortens the time of identifying system availability mode in time-critical applications. Acknowledgements This research was supported by the Estonian Ministry of Education and Research institutional research grant no. IUT33-13 and in part by projects H2020 RIA IMMORTAL, H2020 TWINN TUTORIAL and by European Union through the European Structural and Regional Development Funds. 1. dTron, https://cs.ttu.ee/dtron/