Real-time hierarchical control

A framework for developing hierarchical control systems consisting of layers that group transformation types, the tools to help implement the layers and validate timing properties, and the mechanisms for communicating among layers is discussed. The layered framework supports the design and implementation of control systems with both continuous and discrete components, and is suitable for integrating symbolic and numeric computations in a range of applications. Two applications of the framework-an elevator control system and driver support system-are described     

Time-aware utility-based resource allocation in wireless networks

This paper presents a time-aware admission control and resource allocation scheme in wireless networks in the context of a future generation cellular network. The quality levels (and their respective utility) of different connections are specified using discrete resource-utility (R-U) functions. The scheme uses these R-U functions for allocating and reallocating bandwidth to connections, aiming to maximize the accumulated utility of the system. However, different applications react differently to resource reallocations. Therefore, at each allocation time point, the following factors are taken into account: the age of the connection, a disconnection (drop) penalty, and the sensitiveness to reallocation frequency. The evaluation of our approach shows a superior performance compared to a recent adaptive bandwidth allocation scheme (RBBS). In addition, we have studied the overhead that performing a reallocation imposes on the infrastructure. To minimize this overhead, we present an algorithm that efficiently reduces the number of reallocations while remaining within a given utility bound.     

A Bidding Algorithm for Optimized Utility-Based Resource Allocation in Ad Hoc Networks

This article proposes a scheme for bandwidth allocation in wireless ad hoc networks. The quality of service (QoS) levels for each end-to-end flow are expressed using resource-utility functions, and our algorithms aim to maximize aggregated utility. The shared channel is modeled as bandwidth resources defined by maximal cliques of mutual interfering links. We propose an entirely novel resource allocation algorithm that employs auction mechanisms where flows are bidding for resources. The bids depend both on the flow's utility function and the intrinsically derived shadow prices. Then we combine it with a utility-aware on-demand shortest path routing algorithm where shadow prices are used as a natural distance metric. We also show that the problem can be formulated as a linear programming problem. Thus we can compare the performance of our scheme to the centralized optimal LP solution, registering results very close to the optimum. We isolate the performance of the price-based routing and show its advantages in hotspot scenarios, and also propose an asynchronous version that is more feasible for ad hoc environments. Experimental results of a comparison with the state-of-the-art approach based on Kelly's utility maximization framework show that our approach exhibits superior performance for networks with both increased mobility or increased allocation period.     

Formal Verification of Dynamic Properties in an Aerospace Application

Formal verification of computer-based engineering systems is only meaningful if the mathematical models used are derived systematically, recording the assumptions made at each modelling stage. In this paper we give an exposition of research efforts in cooperation with aerospace industries in Sweden. We emphasize the need for modelling techniques and languages covering the whole spectrum from informal engineering documents, to hybrid mathematical models. In this modelling process we give as much weight to the physical environment as to the controlling software. In particular, we report on our experience using switched bond graphs for the modelling of hardware components in hybrid systems. We present the basic ideas underlying bond graphs and illustrate the approach by modelling an aircraft landing gear system. This system consists of actuating hydromechanic and electromechanic hardware, as well as controlling components implemented in software and electronics. We present a detailed analysis of the closed loop system with respect to safety and timeliness properties. The proofs are carried out within the proof system of Extended Duration Calculus.     

Formal verification of fault tolerance in safety-critical reconfigurable modules

Demands for higher flexibility in aerospace applications has led to increasing deployment of reconfiguarble modules. In several cases the industry is looking into Field Programmable Gate Arrays (FPGA) as a means of efficient adaption of existing components. This paper addresses the safety analysis issues for reconfigurable modules with an emphasis on FPGAs. FPGAs act as digital hardware but in the context of safety analysis they should be treated as software, i.e. with added demands on formal analysis. The contributions of this paper are twofold. First, we illustrate a development process using a language with formal semantics (Esterel) for design, formal verification of high-level design, and automatic code generation down to synthesizable VHDL. We argue that this process reduces the likelihood of systematic (permanent) faults in the design, and still produces VHDL code that may be of acceptable quality (size of FPGA, delay). Secondly, in a general approach that is equally applicable to other formal design languages, we illustrate how the effect of transient fault modes and faults in external modules can be formally studied. We modularly extended the component design model with fault models that represent specific or random faults (e.g. radiation leading to bit flips in the component under design), and transient or permanent faults in the rest of the environment. Some faults corrupt inputs to the component and others jeopardise the effect of output signals that control the environment. This process supports a formal version of Failure Modes and Effects Analysis (FMEA). The set-up is then used to formally determine which (single or multiple) fault modes cause violation of the top-level safety-related property, much in the spirit of fault-tree analyses (FTA). All of this is done with out building the fault tree and using a common model for design and for safety analyses. An aerospace hydraulic monitoring system is used to illustrate the analysis of fault tolerance .