As the advancing autonomy of vehicles requires increasing assistance from the surrounding infrastructure, it becomes clear that the potential for cyberattacks necessitates a sophisticated implementation of resilience, capable of detecting and responding to both internal and external threats. Therefore, threat analysis and risk assessment, including careful modelling of resilience, are essential to prepare against cybersecurity risks. In this context, we extend our method of an automatic discovery of cost-ranked cyberattack scenarios by monitoring/fallback mechanisms. We then demonstrate that this extension allows an analysis of a realistic resilient model of cybersecurity aspects of a level 2 autonomous vehicle in a connected environment.

We present a method for an automatic discovery of cyberattacks in a distributed information system. The method creates a formal model of branching propagation of the attacker from the specification of software and hardware architecture enriched with multi-faceted access control information. The ensuing network of automata, decorated with unitary attack costs, enables a vast range of model checking techniques, in particular the search for the most efficient attack strategies. The model is expressive enough to cover a wide range of attack and defence approaches, like false data injection or redundant data sources.

We present a method for a quantitative formulation of the knowledge of security experts, to be used in an evaluation of attack costs in a cyberphysical system. In order to make the formulation practical, we classify the attacker forms and its attack positions. Applying boiler-plate patterns, like that of an operating system, is also possible. The obtained cost model may allow an exhaustive analysis of hypothetical weaknesses, employed in the design phase of a critical system.

We study the quality of frequency response in a noisy optical network. Such a response can be useful in traditional frequency-domain industrial loop controllers. In particular, we analyse a (step, frequency) response of a simulated computer network, where the stimulus is one of the coefficients which regulate the network’s strategy of packet transmission, and the response is the network’s momentary performance. This way, we find a frequency range, where an instantaneous dependence between the stimulus and the response can direct a self-adaptation scheme of the proposed strategy due to changing network conditions. To stay in the safe limits of the network’s behaviour, we make the stimulus weak. We use a bursty traffic model to test the limits of this approach. We use a model of an optical ring of an experimental NGREEN network developed at NOKIA. The discussed technique was capable of optimising the network’s behaviour.

In traditional model-based engineering (MBE), explicit behavioural models are defined with modelling or domain-specific languages like UML or AADL. These models then refer to corresponding parts of the source code. We propose an alternative scheme, where the application's abstracting code is both the behavioural model and an integral part of the implementation. Together with a special library of explicit objects, like a periodic thread, a running application is able to export its abstracted model. That model can then be refined with our translator from application sources to state machines. As we model cyberphysical systems, the models in question can be probabilistic, non-deterministic and temporal. In order to verify our approach in practice, we have implemented the said library and adapted the translator in question. To demonstrate the potential usage, we refine a model of an application of a robot performing SLAM.

We propose a hierarchical (nested) variant of a recurrent random neural network (RNN) with reinforced learning, introduced by Gelenbe. Each neuron (committee) in a top-level RNN represents a different bottom-level RNN (or sub-committee). The bottom-level RNNs choose the best routing and the top-level RNN chooses the currently best bottom-level RNN. Each of the bottom RNNs is trained in a different way. When they differ in their choice of the best path, several cognitive packets are routed according to the different decisions. In that case, a respective ACK packet trains individual bottom RNNs and not all bottom RNNs at once. An example presents an optimisation of a real-time routing in a dense mesh network of wireless sensors relaying small metering messages between each other, until the messages reach a common gateway. The network is experiencing a periodic electromagnetic interference. The hierarchical variant causes a small increase in the number of smart packets but allows a considerably better routing quality.

We present a model of the edge router between electronic and all optical networks. Arriving electronic packets of variable sizes are stored at a buffer the volume of which is equal to the fixed size of optical packet. When the buffer is filled, its content becomes an optical buffer and dispatched to optical network. To avoid excessive delays, the optical packet is sent also after a specified deadline. The model is based on diffusion approximation and validated by discrete event simulation. Its goal is to determine the probability distribution of the effective optical packet sizes an distribution of their interdeparture times as a function of the interarrival time distribution, distribution of the electronic packet sizes, the value of deadline and the size of buffer. We use real traffic data from the CAIDA (Center for Applied Internet Data Analysis) repositories.

N-GREEN is a cost attractive optical ring network which uses coloured packets. It is normally fit to a predictable traffic with a low burst rate, found e.g. in the metro aggregation. Here we try to adapt the network to other, potentially interesting applications where the traffic is more bursty, by proposing a packet management scheme with adaptive expiration times, determined in response to local and/or global queue sizes. The exact relation is found using a direct optimisation method which uses a simulation. We show that thanks to the regulation of the expiration time, an N-GREEN ring may continuously adapt to a bursty/unpredictable traffic of a varying average load, provided the nodes inform one another about the momentary size of data in their input buffers. The adaptation may considerably decrease the latency of the network.

N-GREEN is a cost attractive optical network which uses coloured optical packets. Its basic component is a ring of novel overdimensioned switch/router nodes, which promises low latency, making it interesting for applications with strict latency requirementslike5G.Nevertheless,itsuffersfromalowefficiency of resources usage, especially when it is used in the Unicast mode popular in the metro aggregation. Here, we try to ensure a better use of network resources by proposing an alternate packet management and transmission method referred to as Ssh-time which could be used in both the Unicast mode and the Broadcastand-Select (Bu0026S) one. We show by simulation that the proposed method improves not only the resources efficiency in case of a metro-aggregation network, but also decreases the mean access delay

Continuous time Markov chains (CTMC) are one of the formalisms for building models. This paper discusses OLYMP2 - a system for solving big CTMC models (exceeding $$10^9$$ states), described with a standard programming language - Java. OLYMP2 is primarily aimed at modelling of computer networks, so its formalism comes from networking concepts, like queueing systems. Using Java as a model description allows for greater flexibility in comparison to model-checker specific languages that often do not employ complete features of an object-oriented programming. Using Java also makes the parsing of models relatively fast, due to optimised Java run-time environment. Introducing dedicated compression of transition matrices allows for keeping memory usage at reasonable level even for large models.

The high demand for more bandwidth and high speed networks stimulates research in the design, optimization and performance evaluation of IP over all-optical networks. In this paper we study optical packet filling algorithm applied at ingress nodes of an all-optical network. Arriving electronic packets of variable sizes are stored at a buffer the volume of which is equal to the fixed size of optical packet. When the available space in the buffer is less than the size of an arriving packet, the stored already content of the buffer is sent inside the optical packet and the electronic packet is rescheduled for the next filling cycle. To avoid excessive delays, the optical packet is dispatched also after a specified deadline whatever is the (non-null) content of the buffer. The performance metrics we consider comprises the filling of optical packets (that means the ratio of blocks in the packet to the actual constant size of the packet) and the distribution of optical packets interdeparture times. The paper demonstrates that the variability of the size of arriving packets and the self-similarity of the input traffic have a visible impact on the both parameters.

We present different ways of an approximate extrapolation of an optimal policy of a small model to that of a large equivalent of the model, which itself is too large to find its exact policy directly using probabilistic model checking (PMC). In particular, we obtain a global optimal resolution of n on-Cdeterminism in several small Markov Decision Processes (MDP) or its extensions like Stochastic Multi-player Games (SMG) using PMC. We then use that resolution to form a hypothesis about an analytic decision boundary representing a respective policy in an equivalent large MDP/SMG. The resulting hypothetical decision boundary is then statistically approximately verified, if it is locally optimal and if it indeed represents a “good enough” policy. The verification either weakens or strengthens the hypothesis. The criterion of the optimality of the policy can be expressed in any modal logic that includes a version of the probabilistic operator P~p[·], and for which a PMC method exists.

The article presents a queueing model of a computer network which is installed at a branch of the largest Polish insurance company. The network is used to store and use documents related to company clients. Our model concentrates on the database server and applications used to retrieve and modify the documents. The model is based on measurements gathered in this system. Our goal is twofold: (i) elaborate a tool that is able to predict the performance of the system in case of modifications (more terminals, more servers) (ii) compare the usefulness of several analytical methods implemented in this case-study.

Delays in routers are an important component of end-to-end delay and therefore have a significant impact on quality of service. While the other component, the propagation time, is easy to predict as the distance divided by the speed of light inside the link, the queueing delays of packets inside routers depend on the current, usually dynamically changing congestion and on the stochastic features of the flows. We use a Markov model taking into account the distribution of the size of packets and self-similarity of incoming flows to investigate their impact on the queueing delays and their dynamics.

. We describe a GPGPU–based Monte Carlo simulator integrated with Prism . It supports Markov chains with discrete or continuous time and a subset of properties expressible in PCTL, CSL and their variants extended with rewards. The simulator allows an automated statistical verification of results obtained us-ing Prism ’s formal methods.

Mixed reality systems overlay real data with virtual information in order to assist users in their current task. They generally combine several hardware components operating at different time scales, and software that has to cope with these timing constraints. MIRELA, for MIxed REality LAnguage, is a framework aimed at modelling, analysing and implementing systems composed of sensors, processing units, shared memories and rendering loops, communicating in a well-defined manner and submitted to timing constraints. The framework is composed of (i) a language allowing a high level, and partially abstract, specification of a concurrent real–time system, (ii) the corresponding semantics, which defines the translation of the system to concrete networks of timed automata, (iii) a methodology for analysing various real-time properties, and (iv) an implementation strategy. We present here a summary of several of our papers about this framework, as well as some recent extensions concerning probability and non–deterministic choices.

We investigate the use of Markov chains in modeling the queues inside IP routers. The model takes into account the measured size of packets, i.e. collected histogram is represented by a linear combination of exponentially distributed phases. We discuss also the impact of the distribution of IP packets size on the loss probability resulting from the limited size of a router memory buffer. The model considers a self similar traffic generated by on-off sources. A special interest is paid to the duration of a queue transient state following the changes of traffic intensity as a function of traffic Hurst parameter and of the utilization of the link. Our goal is to see how far, taking into account the known constraints of Markov models (state explosion) we are able to refine the queueing model.

MIRELA is a high-level language and a rapid prototyping framework dedicated to systems where virtual and digital objects coexist in the same environment and interact in real time. Its semantics is given in the form of networks of timed automata, which can be checked using symbolic methods. This paper shows how to detect various kinds of indefinite waitings in the components of such systems. The method is experimented using the PRISM model checker.