Search

In this paper, we propose and evaluate the performance of fountain codes (FCs) based secure transmission protocols in multiple-input-multiple-output (MIMO) wireless systems, in presence of a passive eavesdropper. In the proposed protocols, a source selects its best antenna to transmit fountain encoded packets to a destination that employs selection combining (SC) or maximal ratio combing (MRC) to enhance reliability of the decoding. The transmission is terminated when the destination has a required number of the encoded packets to reconstruct the original data of the source. Similarly, the eavesdropper also has the ability to recover the source data if it can intercept a sufficient number of the encoded packets. To reduce the number of time slots used, the source can employ non-orthogonal multiple access (NOMA) to send two encoded packets to the destination at each time slot. For performance analysis, exact formulas of average number of time slots (TS) and intercept probability (IP) over Rayleigh fading channel are derived and then verified by Monte-Carlo simulations. The results presented that the protocol using NOMA not only reduces TS but also obtains lower IP at medium and high transmit signal-to-noise ratios (SNRs), as compared with the corresponding protocol without using NOMA.

The notion of contract was introduced to component-based software development in order to facilitate the semantically correct composition of components. We extend the form of this notion which is based on designs to capture probabilistic requirements on execution time. We show how reasoning about such requirements can be done in an infinite-interval-based system of probabilistic duration calculus.

Duration Calculus of Weakly Monotonic Time (WDC) is an extension of DC to allow description of discrete processes where several steps of computation can occur at the same time point. In this paper, we introduce Linear Occurrence Invariants (LOI) using WDC and give an algorithm to check real-time automata for LOI by solving integer programming problems. LOI can be used effectively to specify system requirements in some cases including when the system is considered under the true synchrony assumption. We also extend WDC probabilistically to express dependability requirements of real-time systems and develop a technique to check deterministic probabilistic real-time automata for a class of probabilistic WDC formulas.

Localization always plays a critical role in wireless sensor networks for a wide range of applications including military, healthcare, and robotics. Although the classical multidimensional scaling (MDS) is a conventionally effective model for positioning, the accuracy of this method is affected by noises from the environment. In this paper, we propose a solution to attenuate noise effects to MDS by combining MDS with a Kalman filter. A model is built to predict the noise distribution with regard to additive noises to the distance measurements following the Gaussian distribution. From that, a linear tracking system is developed. The characteristics of the algorithm are examined through simulated experiments and the results reveal the advantages of our method over conventional works in dealing with the above challenges. Besides, the method is simplified with a linear filter; therefore it suits small and embedded sensors equipped with limited power, memory, and computational capacities well.

In this paper, the problem of checking a timed automaton for a Duration Calculus formula of the form Temporal Duration Property is addressed. It is shown that Temporal Duration Properties are in the class of discretisable real-time properties of Timed Automata. and an algorithm is given to solve the problem based on linear programming techniques and the depth-first search method in the integral region graph of the automaton. The complexity of the algorithm is in the same class as that of the solution of the reachability problem of timed automata.

It is proved in this paper that checking a timed automaton ℳ with respect to a linear duration property ⊅ can be done by investigating only the integral timed states of ℳ. An equivalence relation is introduced in this paper to divide the infinite number of integral timed states into finite number of equivalence classes. Based on this, a method is proposed for checking whether ℳ satisfies ⊅. In some cases, the number of equivalence classes is too large for a computer to manipulate. A technique for reducing the search-space for checking linear duration property is also described. This technique is more, suitable for the case in this paper than those in the literature because most of those techniques are designed for reachability analysis.

This paper proposes a method for specification and verification of distributed real-time systems using timed traces. The key idea of the proposed method is to extend distributed transition systems and linear temporal logic over Foata configurations with time. We show that systems are easily specified and verified with this method. The system behaviors are specified by a distributed duration transition system and the system properties are specified by a formula of our proposed timed logic over timed traces. We give an algorithm for solving the verification problem automatically. We also give an example to illustrate how our algorithm work.

In this paper, we introduce an extension of Duration Calculus called Simple Probabilistic Duration Calculus (SPDC) to express dependability requirements for real-time systems, and address the problem to decide if a probabilistic timed automaton satisfies a SPDC formula. We prove that the problem is decidable for a class of SPDC called probabilistic linear duration invariants, and provide a model checking algorithm for solving this problem.

In this chapter we will present selected central elements in the theory of Duration Calculus and we will give examples of applications. The chapter will cover syntax, semantics and proof system for the basic logic. Furthermore, results on decidability, undecidability and model-checking will be presented. A few extensions of the basic calculus will be described, in particular, Hybrid Duration Calculus and Duration Calculus with iterations. Furthermore, a case study: the biphase mark protocol, is presented. We will not attempt to be exhaustive in our coverage of topics; but we will provide references for further study.

Many extensions of Duration Calculus (DC) have been proposed for handling different aspects of real-time systems. For each extension several different semantics are defined for different time structures which are suitable for different applications and achieve low complexity for the decidability of some properties. Hence, different proof systems have to be developed for reasoning in different calculi. We demonstrate that with temporal propositional letters, many useful time structures and operators can be completely described in the original DC with continuous time. Hence, we can use the proof system for original DC and the specification of the specific time structure to reason in that time structure without the need of introducing a new calculus.

A component-based realtime system is a simple model for the server-client relation with time constraints. This paper presents an efficient algorithm, called a blackbox testing algorithm, for detecting the emptiness of a component-based realtime system. This algorithm was originally proposed in [5], but with a certain flaw. We improve it and correct the flaw by using urgency [2] of transitions.

In this paper we propose a simple model for component based real-time systems using duration automata. For this simple model we propose an algorithm for solving the emptiness problem using black-box testing for components which is in the same complexity class as for solving the emptiness problem for untimed component based systems. Furthermore, the verification of behavioural real-time properties in this model can be done with techniques from duration Calculus.

In the paper, the problem of determining the global properties of distributed systems is addressed. At each moment during the execution of a system, every process has its knowledge about the system. By message passing the processes can exchange their knowledge. We present a general algorithm for a process to synthesize the knowledge that it obtains, and to maintain its consistent view about the system. Depending on different interpretations the algorithm can be used for distributed snapshots, for verification and design of stabilizing protocols, etc. >

The paper presents a model of Biphase Mark Protocols (BMP) using Duration Calculus, which seems to be more general and more intuitive than the others in the literature (J.S. Moore, 1994). With Duration Calculus we can model the behaviour of the bus in a natural way and in more detail. The model makes it possible to specify and verify BMP using PVS/DC/sup -/ tool (Mao Xiaoguang et al., 1996). The mechanical verification not only ensures the correctness of the protocol, but also helps engineers to choose the optimal values for the parameters given the ratio between the clock rates of the sender and the receiver and the time for changing the signal from high to low and low to high.

In this paper we present a syntactical approach for deriving real-time programs from a formal specification of the requirements of real-time systems. The main idea of our approach is to model discretization at state level by introducing the discrete states approximating the continuous ones, and then derive a specification of the control program over discrete states. Then the control program is derived from its specification using an extension of Hoare triples to real-time.

The major problem of checking a parallel composition of real-time systems for a real-time property is the explosion of untimed states and time regions. To attack this problem, one can use bisimulation equivalence w.r.t. the property to be checked to minimise the system state space. In this paper, we define such equivalence for the integrated linear duration properties of real-time automaton networks with shared variables. To avoid exhaustive state space exploration, we define a compatibility relation, which is a one-direction simulation relation between configurations. Based on this technique, we develop an algorithm for checking a real-time automaton network with shared variables w.r.t. a linear duration property. Our algorithm can avoid exhaustive state space exploration significantly when applied to Fischer’s mutual exclusion protocol.

In this paper, we consider the problem of checking hybrid systems modelled by hybrid automata for a class of real-time properties represented by linear duration invariants, which are constructed from linear inequalities of integrated durations of system states. Based on linear programming, an algorithm is developed for solving the problem for a class of hybrid automata.

The paper gives a systematic way for the development of hybrid control systems, i.e. to refine specifications written in DC (Duration Calculus) into automata models. Firstly, DC formulas are extended with iteration form and a technique for deriving plant automata from DC formulas is presented. Then, a specification of control automata can be synthesized from plant automata with respect to requirements, based on a necessary and sufficient condition for a plant automaton and a requirement to have a control automaton. Water tank and Gas burner examples are demonstrated to illustrate our method.