The inclusion problem is one of the common problems in real-time systems. The general form of this problem is undecidable; however, the time-bounded verification of inclusion problem is decidable for timed automata. In this study, we propose a new discretization technique to verify the inclusion problem. The proposed technique is applied to a non-Zeno timed automaton with an upper bound that does not contain a non-reachable space for each transition. The new approach is based on the generation of timed bounded discretized language that represents an abstraction of timed words in the form of a set of a countable number of discrete timed words. A discrete timed word aggregates all timed words that share the same actions and their execution times that create the time continuous intervals. The lower and the upper bounds of an interval in a discrete timed word is defined by the minimum and maximum execution times associated to a given transition-run. In addition, we propose the verification schema of the inclusion between two timed bounded discretized languages generated by two non-Zeno timed automata.

In many security applications, system behaviors must be kept secret (opaque) to outside observers (intruders). Opacity was first studied for discrete event systems, and then it was extended to real-time systems. One of the challenges of real-time systems is the difficulty to guarantee their opacity against a potential attacker. In general, this property is undecidable for systems modeled by timed automata. A secret location, S, of a system is timed opaque to an intruder having partial observability of the system, if the intruder can never infer from the observation of any execution that the system has reached any secret location. In the present study, the static partial observability for systems modeled by nondeterministic timed automata is investigated. Thus, it focuses on systems where the timing of secret state reachability is bounded. The first contribution of this study is to define the bounded timed opacity property wherein, its complexity is proved. The second contribution is to consider systems where the secret should be kept hidden for a certain period referred to as the Δ-duration bounded opacity property. Also, a formal definition is proposed and its complexity is proved. In addition, the proposed properties are verified using timed bounded model checking. A case study ”Exchange in the Cloud system” is modeled by timed automaton to verify the proposed properties using SpaceEx tool.

The increasing adoption of Reinforcement Learning in safety-critical systems domains such as autonomous vehicles, health, and aviation raises the need for ensuring their safety. Existing safety mechanisms such as adversarial training, adversarial detection, and robust learning are not always adapted to all disturbances in which the agent is deployed. Those disturbances include moving adversaries whose behavior can be unpredictable by the agent, and as a matter of fact harmful to its learning. Ensuring the safety of critical systems also requires methods that give formal guarantees on the behaviour of the agent evolving in a perturbed environment. It is therefore necessary to propose new solutions adapted to the learning challenges faced by the agent. In this paper, first we generate adversarial agents that exhibit flaws in the agent's policy by presenting moving adversaries. Secondly, We use reward shaping and a modified Q-learning algorithm as defense mechanisms to improve the agent's policy when facing adversarial perturbations. Finally, probabilistic model checking is employed to evaluate the effectiveness of both mechanisms. We have conducted experiments on a discrete grid world with a single agent facing non-learning and learning adversaries. Our results show a diminution in the number of collisions between the agent and the adversaries. Probabilistic model checking provides lower and upper probabilistic bounds regarding the agent's safety in the adversarial environment.

TTEthernet has been proposed as an improvement of the Ethernet network protocol to ensure communication of critical systems. Some of these systems, such as avionics systems, are complex and evolving ones. Therefore, they are designed iteratively by integrating in each iteration some components of the system. Adding new functionalities may induce substantial additional costs of reconfiguration of the system in order to meet the real-time requirements. Based on the constraint programming techniques, we develop in this paper a cost optimisation approach that meets the TTEthernet specification and validates the latencies requirements in an accurate way. We illustrate our approach on a case study with the MiniZinc tool (Nethercote et al., 2007).

A system satisfies opacity if its secret behaviors cannot be detected by any user of the system. Opacity of distributed systems was originally set as a boolean predicate before being quantified as measures in a probabilistic setting. This paper considers a different quantitative approach that measures the efforts that a malicious user has to make to detect a secret. This effort is measured as a distance w.r.t a regular profile specifying a normal behavior. This leads to several notions of quantitative opacity. When attackers are passive that is, when they just observe the system, quantitative opacity is brought back to a language inclusion problem, and is PSPACE-complete. When attackers are active, that is, interact with the system in order to detect secret behaviors within a finite depth observation, quantitative opacity turns to be a two-player finite-state quantitative game of partial observation. A winning strategy for an attacker is a sequence of interactions with the system leading to a secret detection without exceeding some profile deviation measure threshold. In this active setting, the complexity of opacity is EXPTIME-complete.

On a partially observed system, a secret φ is opaque if an observer cannot ascertain that its trace belongs to φ. We consider specifications given as Constraint Markov Chains (CMC), which are underspecified Markov chains where probabilities on edges are required to belong to some set. The nondeterminism is resolved by a scheduler, and opacity on this model is defined as a worst case measure over all implementations obtained by scheduling. This measures the information obtained by a passive observer when the system is controlled by the smartest scheduler in coalition with the observer. When restricting to the subclass of Linear CMC, we compute (or approximate) this measure and prove that refinement of a specification can only improve opacity.

Integrated modular avionics architectures complemented with time-triggered ethernet (TTEthernet) provides a strong platform to support the design and deployment of distributed avionic software systems. The complexity of the design and continuous integration of such systems can be managed using a model-based methodology. In this paper, we present an extension for the AADL modeling language to support modeling TTEthernet-based distributed systems. This extension consists essentially in a metamodel of the TTEthernet standard and the implementation of its corresponding concrete syntax. Furthermore, we leverage model transformations to enable undertaking the verification of the system models expressed using our AADL extension. In particular, we propose to transform the system model to a model suitable for a simulation using the discrete event system specification formalism. We illustrate the proposed approach using an example of a navigation and guidance system and we use this example to show the verification of the contention-freed property of TTEthernet schedule.

The Integrated Modular Avionics (IMA) architecture and the Time-Triggered Ethernet (TTEthernet) network have emerged as the key components of a typical architecture model for recent civil aircrafts. In this paper, we present a first approach to model and verify avionic systems embedded in the Integrated Modular Architecture (IMA) connected through the TTEthernet Network, by using TTCC, a real-time concurrent constraint process calculus with an operator to define infinite periodic behaviors specific to IMA and TTEthernet. We argue that the operational constructs for interacting processes with one another of TTCC provide a suitable language to describe the time triggered architecture while the declarative aspects of this calculus provide a simple and elegant way to specify requirements of avionic systems. We also illustrate how TTCC may provide a unified framework for the analysis of avionic systems embedded in the IMA connected through the TTEthernet by modeling, specifying and verifying a case study developed in collaboration with an industrial partner, the landing gear system.

The SAE standard Time-triggered Ethernet defines a strong networking infrastructure, which supports the engineering of avionic systems. Avionic functions are often designed independently and integrated to form the avionic system. The iterative integration approach helps in controlling the design complexity of evolving avionic systems and aims at minimizing the cost associate with the reconfiguration of scheduling parameters of already integrated parts. On the other hand, the iterative approach requires to specify and manage a huge set of constraints, which are then solved to compute the optimal scheduling parameters. In this paper, we focus on this issue of manual specification of these constraints by the system engineer. We propose a model-driven approach, which provides the required abstractions and automation to support the system engineer in using effectively the iterative integration approach. The abstractions consist in a metamodel, which describes the system at a given integration step and a metamodel for the constraints. The automation consists in a model transformation which enables generating automatically the relevant constraints at integration step.

Given a probabilistic transition system (PTS) A partially observed by an attacker, and an ω-regular predicate φ over the traces of A, measuring the disclosure of the secret φ in A means computing the probability that an attacker who observes a run of A can ascertain that its trace belongs to φ. We consider specifications given as Interval Markov Chains (IMCs), which are underspecified Markov chains where probabilities on edges are only required to belong to intervals. Scheduling an IMC S produces a concrete implementation as a PTS and we define the worst case disclosure of secret φ in S as the maximal disclosure of φ over all PTSs thus produced. We compute this value for a subclass of IMCs and we prove that simulation between specifications can only improve the opacity of implementations.

The combination of the SAE Time Triggered Ethernet (TTEthernet) standard with the Integrated Modular Avionics (IMA) architectures supports the design, deployment and integration of mixed-critical avionic applications.In order to cope with the complexity of these tasks, we advocate for a model-driven engineering methodology.The key element of such methodology is the modeling language, which enables producing relevant models of the system.In this paper, we present a metamodel, which captures the main features and concepts defined in the SAE TTEthernet standard.We discuss how a combination of the TTEthernet metamodel with an IMA metamodel can be used to extend the AADL modeling language to model avionic applications deployed a TTEthernet-networked IMA platform.Finally, we present a case study to illustrate our approach.

The Integrated Modular Avionics (IMA) architec- ture and the Time-Triggered Ethernet (TTEthernet) network have emerged as the key components of a typical architecture model for recent civil aircrafts. We propose a real-time constraint-based calculus targeted at the analysis of such concepts of avionic embedded systems. We show our framework at work on the modelisation of both the (IMA) architecture and the TTEthernet network, illustrating their behavior by the well-known Flight Management System (FMS).

To build reliable avionic applications, we interconnect Integrated Modular Avionics (IMA) architectures with Time- Triggered Ethernet (TT-Ethernet). These systems have direct impacts on human lives where the failure is unacceptable. Therefore, verification is an important issue to ensure the safety and the performance of the system. The integration of IMA architectures is a very complex and challenging engineering task. To cope with complexity and to perform verification, a model-based approach, which endows engineering teams with a methodology and an adequate tooling is of a paramount importance. To design IMA architectures interconnected with TT-Ethernet, we have proposed an extension of the AADL language in previous works. In this paper, we present a simulation-based verification of our extension and show how it can be simulated using a discrete event simulation environment called DEVS Suite. The main advantage of this technique is to perform cycle-accurate simulation of the complex avionics systems, which cannot be undertaken by model checking techniques. The tool demonstration video is available at: http://youtu.be/hwgN-a-7rzw.

Covert channels represent a security problem for information systems, since they permit illegal flows and sometimes leaks of classified data. Although numerous descriptions have been given at a concrete level, relatively few work has been carried out at a more abstract level. In this paper, we propose a definition for covert channels based on encoding and decoding binary messages with transducers, in a finite transition system, and we explain why this definition is different from a similar notion of so called iterated interference. We also show that covert channels can be detected using a restricted class of transducers.

Non-interference (NI) is a property of systems stating that confidential actions should not cause effects observable by unauthorized users. Several variants of NI have been studied for many types of models, but rarely for true concurrency or unbounded models. This work investigates NI for High-level Message Sequence Charts (HMSC), a scenario language for the description of distributed systems, based on composition of partial orders. We first propose a general definition of security properties in terms of equivalence among observations, and show that these properties, and in particular NI are undecidable for HMSCs. We hence consider weaker local properties, describing situations where a system is attacked by a single agent, and show that local NI is decidable. We then refine local NI to a finer notion of causal NI that emphasizes causal dependencies between confidential actions and observations, and extend it to causal NI with (selective) declassification of confidential events. Checking whether a system satisfies local and causal NI and their declassified variants are PSPACE-complete problems.

Given a probabilistic transition system (PTS) A partially observed by an attacker, and an ω-regular predicate ϕ over the traces of A, measuring the disclosure of the secret ϕ in A means computing the probability that an attacker who observes a run of A can ascertain that its trace belongs to ϕ. In the context of refinement, we consider specifications given as Interval-valued Discrete Time Markov Chains (IDTMCs), which are underspecified Markov chains where probabilities on edges are only required to belong to intervals. Scheduling an IDTMC S produces a concrete implementation as a PTS and we define the worst case disclosure of secret ϕ in S as the maximal disclosure of ϕ over all PTSs thus produced. We compute this value for a subclass of IDTMCs and we prove that refinement can only improve the opacity of implementations.

The Integrated Modular Avionics (IMA) architecture and the Time-Triggered Ethernet (TTEthernet) network have emerged as the key components of a typical architecture model for recent civil aircrafts. It has recently been proposed to model both the (IMA) architecture and the TTEthernet network in the constraint-based TTCC calculus. In this paper, we show how the declarative aspects of this calculus can provide a simple and elegant way to specify requirements of time-triggered systems. We illustrate our approach on a complete model of a sub-system of the flight management system.

Opacity is a general language-theoretic framework in which several security properties of a system can be expressed. Its parameters are a predicate, given as a subset of runs of the system, and an observation function, from the set of runs into a set of observables. The predicate describes secret information in the system and, in the possibilistic setting, it is opaque if its membership cannot be inferred from observation. In this paper, we propose several notions of quantitative opacity for probabilistic systems, where the predicate and the observation function are seen as random variables. Our aim is to measure (i) the probability of opacity leakage relative to these random variables and (ii) the level of uncertainty about membership of the predicate inferred from observation. We show how these measures extend possibilistic opacity, we give algorithms to compute them for regular secrets and observations, and we apply these computations on several classical examples. We finally partially investigate the non-deterministic setting.

The design of avionic systems is a complex engineering activity. The iterative integration approach helps in controlling the complexity of such activity. On the other hand, using such approach to design evolving systems requires the reconfiguration of scheduling parameters of already integrated parts. This reconfiguration results in a recertification process having a cost that depends on the criticality level of the affected application. We propose a new approach which helps the system designer at each integration step in establishing the new scheduling parameters that minimize such cost. In this work, we focus on the Integrated Modular Avionic (IMA) architecture connected through a Time-Triggered Ethernet (TTEthernet) network. We present a formal model for such systems and we use this model to define a set of constraints that ensure the real-time requirements. These constraints are expressed using an SMTbased language and we used the SMT-solver YICES to find automatically a feasible scheduling parameters that minimize the cost of integration. We show our framework at work by analyzing the iterative integration of some functionalities of the Flight Management System.

Information flow properties express the capability for an agent to infer information about secret behaviours of a partially observable system. In a language-theoretic setting, where the system behaviour is described by a language, we define the class of rational information flow properties (RIFP), where observers are modeled by finite transducers, acting on languages in a given family $\mathcal{L}$. This leads to a general decidability criterion for the verification problem of RIFPs on $\mathcal{L}$, implying PSPACE-completeness for this problem on regular languages. We show that most trace-based information flow properties studied up to now are RIFPs, including those related to selective declassification and conditional anonymity. As a consequence, we retrieve several existing decidability results that were obtained by ad-hoc proofs.