Verification of floating point programs

In this thesis we present an approach to automated verification of floating point programs. Existing techniques for automated generation of correctness theorems are extended to produce proof obligations for accuracy guarantees and absence of floating point exceptions. A prototype automated real number theorem prover is presented, demonstrating a novel application of function interval arithmetic in the context of subdivision-based numerical theorem proving. The prototype is tested on correctness theorems for two simple yet nontrivial programs, proving exception freedom and tight accuracy guarantees automatically. The prover demonstrates a novel application of function interval arithmetic in the context of subdivision-based numerical theorem proving. The experiments show how function intervals can be used to combat the information loss problems that limit the applicability of traditional interval arithmetic in the context of hard real number theorem proving.

Polynomial function intervals for floating-point software verification

The focus of our work is the verification of tight functional properties of numerical programs, such as showing that a floating-point implementation of Riemann integration computes a close approximation of the exact integral. Programmers and engineers writing such programs will benefit from verification tools that support an expressive specification language and that are highly automated. Our work provides a new method for verification of numerical software, supporting a substantially more expressive language for specifications than other publicly available automated tools. The additional expressivity in the specification language is provided by two constructs. First, the specification can feature inclusions between interval arithmetic expressions. Second, the integral operator from classical analysis can be used in the specifications, where the integration bounds can be arbitrary expressions over real variables. To support our claim of expressivity, we outline the verification of four example programs, including the integration example mentioned earlier. A key component of our method is an algorithm for proving numerical theorems. This algorithm is based on automatic polynomial approximation of non-linear real and real-interval functions defined by expressions. The PolyPaver tool is our implementation of the algorithm and its source code is publicly available. In this paper we report on experiments using PolyPaver that indicate that the additional expressivity does not come at a performance cost when comparing with other publicly available state-of-the-art provers. We also include a scalability study that explores the limits of PolyPaver in proving tight functional specifications of progressively larger randomly generated programs. © 2014 Springer International Publishing Switzerland.

Time complexity and convergence analysis of domain theoretic Picard method

We present an implementation of the domain-theoretic Picard method for solving initial value problems (IVPs) introduced by Edalat and Pattinson [1]. Compared to Edalat and Pattinson's implementation, our algorithm uses a more efficient arithmetic based on an arbitrary precision floating-point library. Despite the additional overestimations due to floating-point rounding, we obtain a similar bound on the convergence rate of the produced approximations. Moreover, our convergence analysis is detailed enough to allow a static optimisation in the growth of the precision used in successive Picard iterations. Such optimisation greatly improves the efficiency of the solving process. Although a similar optimisation could be performed dynamically without our analysis, a static one gives us a significant advantage: we are able to predict the time it will take the solver to obtain an approximation of a certain (arbitrarily high) quality.

On bandwidth request mechanism with piggyback in fixed IEEE 802.16 networks

This paper investigates the random channel access mechanism specified in the IEEE 802.16 standard for the uplink traffic in a Point-to-MultiPoint (PMP) network architecture. An analytical model is proposed to study the impacts of the channel access parameters, bandwidth configuration and piggyback policy on the performance. The impacts of physical burst profile and non-saturated network traffic are also taken into account in the model. Simulations validate the proposed analytical model. It is observed that the bandwidth utilization can be improved if the bandwidth for random channel access can be properly configured according to the channel access parameters, piggyback policy and network traffic.

Performance comparison of OFDM bandwidth request schemes in fixed IEEE 802.16 networks

IEEE 802.16 standard specifies two contention based bandwidth request schemes working with OFDM physical layer specification in point-to-multipoint (PMP) architecture, the mandatory one used in region-full and the optional one used in region-focused. This letter presents a unified analytical model to study the bandwidth efficiency and channel access delay performance of the two schemes. The impacts of access parameters, available bandwidth and subchannelization have been taken into account. The model is validated by simulations. The mandatory scheme is observed to perform closely to the optional one when subchannelization is active for both schemes.

Modeling contention based bandwidth request scheme for IEEE 802.16 networks

IEEE 802.16 standard specifies a contention based bandwidth request scheme for best-effort and non-real time polling services in Point-to-MultiPoint (PMP) architecture. In this letter we propose an analytical model for the scheme and study how the performances of bandwidth efficiency and channel access delay change with the contention window size, the number of contending subscriber stations, the number of slots allocated for bandwidth request and data transmission. Simulations validate its high accuracy. © 2007 IEEE.

An accurate and scalable analytical model for IEEE 802.15.4 slotted CSMA/CA networks

In this paper a Markov chain based analytical model is proposed to evaluate the slotted CSMA/CA algorithm specified in the MAC layer of IEEE 802.15.4 standard. The analytical model consists of two two-dimensional Markov chains, used to model the state transition of an 802.15.4 device, during the periods of a transmission and between two consecutive frame transmissions, respectively. By introducing the two Markov chains a small number of Markov states are required and the scalability of the analytical model is improved. The analytical model is used to investigate the impact of the CSMA/CA parameters, the number of contending devices, and the data frame size on the network performance in terms of throughput and energy efficiency. It is shown by simulations that the proposed analytical model can accurately predict the performance of slotted CSMA/CA algorithm for uplink, downlink and bi-direction traffic, with both acknowledgement and non-acknowledgement modes.

Unified model for performance analysis of IEEE 802.11 ad hoc networks in unsaturated conditions

IEEE 802.11 standard has achieved huge success in the past decade and is still under development to provide higher physical data rate and better quality of service (QoS). An important problem for the development and optimization of IEEE 802.11 networks is the modeling of the MAC layer channel access protocol. Although there are already many theoretic analysis for the 802.11 MAC protocol in the literature, most of the models focus on the saturated traffic and assume infinite buffer at the MAC layer. In this paper we develop a unified analytical model for IEEE 802.11 MAC protocol in ad hoc networks. The impacts of channel access parameters, traffic rate and buffer size at the MAC layer are modeled with the assistance of a generalized Markov chain and an M/G/1/K queue model. The performance of throughput, packet delivery delay and dropping probability can be achieved. Extensive simulations show the analytical model is highly accurate. From the analytical model it is shown that for practical buffer configuration (e.g. buffer size larger than one), we can maximize the total throughput and reduce the packet blocking probability (due to limited buffer size) and the average queuing delay to zero by effectively controlling the offered load. The average MAC layer service delay as well as its standard deviation, is also much lower than that in saturated conditions and has an upper bound. It is also observed that the optimal load is very close to the maximum achievable throughput regardless of the number of stations or buffer size. Moreover, the model is scalable for performance analysis of 802.11e in unsaturated conditions and 802.11 ad hoc networks with heterogenous traffic flows. © 2012 KSI.

An accurate Markov model for slotted CSMA/CA algorithm in IEEE 802.15.4 networks

In this letter we propose an Markov model for slotted CSMA/CA algorithm working in a non-acknowledgement mode, specified in IEEE 802.15.4 standard. Both saturation throughput and energy consumption are modeled as functions of backoff window size, number of contending devices and frame length. Simulations show that the proposed model can achieve a very high accuracy (less than 1% mismatch) if compared to all existing models (bigger than 10% mismatch).

Uncoordinated coexisting IEEE 802.15.4 networks for machine to machine communications

IEEE 802.15.4 standard has been proposed for low power wireless personal area networks. It can be used as an important component in machine to machine (M2M) networks for data collection, monitoring and controlling functions. With an increasing number of machine devices enabled by M2M technology and equipped with 802.15.4 radios, it is likely that multiple 802.15.4 networks may be deployed closely, for example, to collect data for smart metering at residential or enterprise areas. In such scenarios, supporting reliable communications for monitoring and controlling applications is a big challenge. The problem becomes more severe due to the potential hidden terminals when the operations of multiple 802.15.4 networks are uncoordinated. In this paper, we investigate this problem from three typical scenarios and propose an analytic model to reveal how performance of coexisting 802.15.4 networks may be affected by uncoordinated operations under these scenarios. Simulations will be used to validate the analytic model. It is observed that uncoordinated operations may lead to a significant degradation of system performance in M2M applications. With the proposed analytic model, we also investigate the performance limits of the 802.15.4 networks, and the conditions under which coordinated operations may be required to support M2M applications. © 2012 Springer Science + Business Media, LLC.

Coverage overlapping problems in applications of IEEE 802.15.4 wireless sensor networks

IEEE 802.15.4 standard is a relatively new standard designed for low power low data rate wireless sensor networks (WSN), which has a wide range of applications, e.g., environment monitoring, e-health, home and industry automation. In this paper, we investigate the problems of hidden devices in coverage overlapped IEEE 802.15.4 WSNs, which is likely to arise when multiple 802.15.4 WSNs are deployed closely and independently. We consider a typical scenario of two 802.15.4 WSNs with partial coverage overlapping and propose a Markov-chain based analytical model to reveal the performance degradation due to the hidden devices from the coverage overlapping. Impacts of the hidden devices and network sleeping modes on saturated throughput and energy consumption are modeled. The analytic model is verified by simulations, which can provide the insights to network design and planning when multiple 802.15.4 WSNs are deployed closely. © 2013 IEEE.

Modeling impact of both frame collisions and frame corruptions on IEEE 802.15.4 channel access for smart grid applications

IEEE 802.15.4 standard has been recently developed for low power wireless personal area networks. It can find many applications for smart grid, such as data collection, monitoring and control functions. The performance of 802.15.4 networks has been widely studied in the literature. However the main focus has been on the modeling throughput performance with frame collisions. In this paper we propose an analytic model which can model the impact of frame collisions as well as frame corruptions due to channel bit errors. With this model the frame length can be carefully selected to improve system performance. The analytic model can also be used to study the 802.15.4 networks with interference from other co-located networks, such as IEEE 802.11 and Bluetooth networks. © 2011 Springer-Verlag.

Performance modelling and analysis of multiple coexisting IEEE 802.15.4 wireless sensor networks

With the features of low-power and flexible networking capabilities IEEE 802.15.4 has been widely regarded as one strong candidate of communication technologies for wireless sensor networks (WSNs). It is expected that with an increasing number of deployments of 802.15.4 based WSNs, multiple WSNs could coexist with full or partial overlap in residential or enterprise areas. As WSNs are usually deployed without coordination, the communication could meet significant degradation with the 802.15.4 channel access scheme, which has a large impact on system performance. In this thesis we are motivated to investigate the effectiveness of 802.15.4 networks supporting WSN applications with various environments, especially when hidden terminals are presented due to the uncoordinated coexistence problem. Both analytical models and system level simulators are developed to analyse the performance of the random access scheme specified by IEEE 802.15.4 medium access control (MAC) standard for several network scenarios. The first part of the thesis investigates the effectiveness of single 802.15.4 network supporting WSN applications. A Markov chain based analytic model is applied to model the MAC behaviour of IEEE 802.15.4 standard and a discrete event simulator is also developed to analyse the performance and verify the proposed analytical model. It is observed that 802.15.4 networks could sufficiently support most WSN applications with its various functionalities. After the investigation of single network, the uncoordinated coexistence problem of multiple 802.15.4 networks deployed with communication range fully or partially overlapped are investigated in the next part of the thesis. Both nonsleep and sleep modes are investigated with different channel conditions by analytic and simulation methods to obtain the comprehensive performance evaluation. It is found that the uncoordinated coexistence problem can significantly degrade the performance of 802.15.4 networks, which is unlikely to satisfy the QoS requirements for many WSN applications. The proposed analytic model is validated by simulations which could be used to obtain the optimal parameter setting before WSNs deployments to eliminate the interference risks.

Coverage overlapping problems in applications of IEEE 802.15.4 wireless sensor networks

IEEE 802.15.4 standard is a relatively new standard designed for low power low data rate wireless sensor networks (WSN), which has a wide range of applications, e.g., environment monitoring, e-health, home and industry automation. In this paper, we investigate the problems of hidden devices in coverage overlapped IEEE 802.15.4 WSNs, which is likely to arise when multiple 802.15.4 WSNs are deployed closely and independently. We consider a typical scenario of two 802.15.4 WSNs with partial coverage overlapping and propose a Markov-chain based analytical model to reveal the performance degradation due to the hidden devices from the coverage overlapping. Impacts of the hidden devices and network sleeping modes on saturated throughput and energy consumption are modeled. The analytic model is verified by simulations, which can provide the insights to network design and planning when multiple 802.15.4 WSNs are deployed closely. © 2013 IEEE.

Management of services differentiation and guarantee in IEEE 802.11e wireless LANs

In this paper, we study the management and control of service differentiation and guarantee based on enhanced distributed function coordination (EDCF) in IEEE 802.11e wireless LANs. Backoff-based priority schemes are the major mechanism for Quality of Service (QoS) provisioning in EDCF. However, control and management of the backoff-based priority scheme are still challenging problems. We have analysed the impacts of backoff and Inter-frame Space (IFS) parameters of EDCF on saturation throughput and service differentiation. A centralised QoS management and control scheme is proposed. The configuration of backoff parameters and admission control are studied in the management scheme. The special role of access point (AP) and the impact of traffic load are also considered in the scheme. The backoff parameters are adaptively re-configured to increase the levels of bandwidth guarantee and fairness on sharing bandwidth. The proposed management scheme is evaluated by OPNET. Simulation results show the effectiveness of the analytical model based admission control scheme. ©2005 IEEE.