In urban planning, sophisticated simulation models are key tools to estimate future population growth for measuring the impact of planning decisions on urban developments and the environment. Simulated population projections usually result in large, macro-scale, multivariate geospatial data sets. Millions of records have to be processed, stored, and visualized to help planners explore and analyze complex population patterns. We introduce a database driven framework for visualizing geospatial multidimensional simulation data based on the output from UrbanSim, a software for the analysis and planning of urban developments. The designed framework is extendable and aims at integrating empirical-stochastic methods and urban simulation models with techniques developed for information visualization and cartography. First, we develop an empirical model for the estimation of residential building types based on demographic household characteristics. The predicted dwelling type information is important for the analysis of future material use, carbon footprint calculations, and for visualizing simultaneously the results of land usage, density, and other significant parameters in 3D space. Our model uses multinomial logistic regression to derive building types at different scales. The estimated regression coefficients are applied to UrbanSim output in order to predict residential building types. The simulation results and the estimated building types are managed in an object-relational geodatabase. From the database, density, building types, and significant demographic variables are visually encoded as scalable, georeferenced 3D geometries and displayed on top of aerial photographs in a Google Earth visual synthesis. The geodatabase can be accessed and the visualization parameters can be chosen through a web-based user interface. The geometries are encoded in KML, Google's markup language, as ready-to-visualize data sets. The goal is to enhance human cognition by displaying abstract representations of multidimensional data sets in a realistic context and thus to support decision making in planning processes.
The visualization of numerical fluid flow datasets is essential to the engineering processes that motivate their computational simulation. To address the need for visual representations that convey meaningful relations and enable a deep understanding of flow structures, the discipline of Flow Visualization has produced many methods and schemes that are tailored to a variety of visualization tasks. The ever increasing complexity of modern flow simulations, however, puts an enormous demand on these methods. The study of vortex breakdown, for example, which is a highly transient and inherently three-dimensional flow pattern with substantial impact wherever it appears, has driven current techniques to their limits. In this thesis, we propose several novel visualization methods that significantly advance the state of the art in the visualization of complex flow structures. First, we propose a novel scheme for the construction of stream surfaces from the trajectories of particles embedded in a flow. These surfaces are extremely useful since they naturally exploit coherence between neighboring trajectories and are highly illustrative in nature. We overcome the limitations of existing stream surface algorithms that yield poor results in complex flows, and show how the resulting surfaces can be used a building blocks for advanced flow visualization techniques. Moreover, we present a visualization method that is based on moving section planes that travel through a dataset and sample the flow. By considering the changes to the flow topology on the plane as it moves, we obtain a method of visualizing topological structures in three-dimensional flows that are not accessible by conventional topological methods. On the same algorithmic basis, we construct an algorithm for the tracking of critical points in such flows, thereby enabling the treatment of time-dependent datasets. Last, we address some problems with the recently introduced Lagrangian techniques. While conceptually elegant and generally applicable, they suffer from an enormous computational cost that we significantly use by developing an adaptive approximation algorithm. This allows the application of such methods on very large and complex numerical simulations. Throughout this thesis, we will be concerned with flow visualization aspect of general practical significance but we will particularly emphasize the remarkably challenging visualization of the vortex breakdown phenomenon.
This technical report is the Emerging Trends proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), which was held during 10-13 September in Kaiserslautern, Germany. TPHOLs covers all aspects of theorem proving in higher order logics as well as related topics in theorem proving and veriﬁcation.
Modelling languages are important in the process of software development. The suitability of a modelling language for a project depends on its applicability to the target domain. Here, domain-specific languages have an advantage over more general modelling languages. On the other hand, modelling languages like the Unified Modeling Language can be used in a wide range of domains, which supports the reuse of development knowledge between projects. This thesis treats the syntactical and semantical harmonisation of modelling languages and their combined use, and the handling of complexity of modelling languages by providing language subsets - called language profiles - with tailor-made formal semantics definitions, generated by a profile tool. We focus on the widely-used modelling languages SDL and UML, and formal semantics definitions specified using Abstract State Machines.
Calibration of robots has become a research field of great importance over the last decades especially in the field industrial robotics. The main reason for this is that the field of application was significantly broadened due to an increasing number of fully automated or robot assisted tasks to be performed. Those applications require significantly higher level of accuracy due to more delicate tasks that need to be fulfilled (e.g. assembly in the semiconductor industry or robot assisted medical surgery). In the past, (industrial) robot calibration had to be performed manually for every single robot under lab conditions in a long and cost intensive process. Expensive and complex measurement systems had to be operated by highly trained personnel. The result of this process is a set of measurements representing the robot pose in the task space (i.e. world coordinate system) and as joint encoder values. To determine the deviation, the robot pose indicated by the internal joint encoder values has to be compared to the physical pose (i.e. external measurement data). Hence, the errors in the kinematic model of the robot can be computed and therefore later on compensated. These errors are inevitable and caused by varying manufacturing tolerances and other sources of error (e.g. friction and deflection). They have to be compensated in order to achieve sufficient accuracy for the given tasks. Furthermore for performance, maintenance, or quality assurance reasons the robots may have to undergo the calibration process in constant time intervals to monitor and compensate e.g. ageing effects such as wear and tear. In modern production processes old fashioned procedures like the one mentioned above are no longer suitable. Therefore a new method has to be found that is less time consuming, more cost effective, and involves less (or in the long term even no) human interaction in the calibration process.
The provision of quality-of-service (QoS) on the network layer is a major challenge in communication networks. This applies particularly to mobile ad-hoc networks (MANETs) in the area of Ambient Intelligence (AmI), especially with the increasing use of delay and bandwidth sensitive applications. The focus of this survey lies on the classification and analysis of selected QoS routing protocols in the domain of mobile ad-hoc networks. Each protocol is briefly described and assessed, and the results are summarized in multiple tables.
Abstraction is intensively used in the verification of large, complex or infinite-state systems. With abstractions getting more complex it is often difficult to see whether they are valid. However, for using abstraction in model checking it has to be ensured that properties are preserved. In this paper, we use a translation validation approach to verify property preservation of system abstractions. We formulate a correctness criterion based on simulation between concrete and abstract system for a property to be verified. For each distinct run of the abstraction procedure the correctness is verified in the theorem prover Isabelle/HOL. This technique is applied in the verification of embedded adaptive systems. This paper is an extended version a previously published work.
The Super-Peer Selection Problem is an optimization problem in network topology construction. It may be cast as a special case of a Hub Location Problem, more exactly an Uncapacitated Single Allocation p-Hub Median Problem with equal weights. We show that this problem is still NP-hard by reduction from Max Clique.
Guaranteeing correctness of compilation is a ma jor precondition for correct software. Code generation can be one of the most error-prone tasks in a compiler. One way to achieve trusted compilation is certifying compilation. A certifying compiler generates for each run a proof that it has performed the compilation run correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof, one can be sure that the compiler produced correct code. This paper presents a certifying code generation phase for a compiler translating an intermediate language into assembler code. The time spent for checking the proofs is the bottleneck of certifying compilation. We exhibit an improved framework for certifying compilation and considerable advances to overcome this bottleneck. We compare our implementation featuring the Coq theorem prover to an older implementation. Our current implementation is feasible for medium to large sized programs.
The provision of network Quality-of-Service (network QoS) in wireless (ad-hoc) networks is a major challenge in the development of future communication systems. Before designing and implementing these systems, the network QoS requirements are to be specified. Since QoS functionalities are integrated across layers and hence QoS specifications exist on different system layers, a QoS mapping technique is needed to translate the specifications into each other. In this paper, we formalize the relationship between layers. Based on a comprehensive and holistic formalization of network QoS requirements, we define two kinds of QoS mappings. QoS domain mappings associate QoS domains of two abstraction levels. QoS scalability mappings associate utility and cost functions of two abstraction levels. We illustrate our approach by examples from the case study Wireless Video Transmission.