Change search
Refine search result
123 1 - 50 of 134
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 1.
    Alves, Ricardo
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Leveraging Existing Microarchitectural Structures to Improve First-Level Caching Efficiency2019Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    Low-latency data access is essential for performance. To achieve this, processors use fast first-level caches combined with out-of-order execution, to decrease and hide memory access latency respectively. While these approaches are effective for performance, they cost significant energy, leading to the development of many techniques that require designers to trade-off performance and efficiency.

    Way-prediction and filter caches are two of the most common strategies for improving first-level cache energy efficiency while still minimizing latency. They both have compromises as way-prediction trades off some latency for better energy efficiency, while filter caches trade off some energy efficiency for lower latency. However, these strategies are not mutually exclusive. By borrowing elements from both, and taking into account SRAM memory layout limitations, we proposed a novel MRU-L0 cache that mitigates many of their shortcomings while preserving their benefits. Moreover, while first-level caches are tightly integrated into the cpu pipeline, existing work on these techniques largely ignores the impact they have on instruction scheduling. We show that the variable hit latency introduced by way-misspredictions causes instruction replays of load dependent instruction chains, which hurts performance and efficiency. We study this effect and propose a variable latency cache-hit instruction scheduler, that identifies potential misschedulings, reduces instruction replays, reduces negative performance impact, and further improves cache energy efficiency.

    Modern pipelines also employ sophisticated execution strategies to hide memory latency and improve performance. While their primary use is for performance and correctness, they require intermediate storage that can be used as a cache as well. In this work we demonstrate how the store-buffer, paired with the memory dependency predictor, can be used to efficiently cache dirty data; and how the physical register file, paired with a value predictor, can be used to efficiently cache clean data. These strategies not only improve both performance and energy, but do so with no additional storage and minimal additional complexity, since they recycle existing cpu structures to detect reuse, memory ordering violations, and misspeculations.

  • 2.
    Amnell, Tobias
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Code synthesis for timed automata2003Licentiate thesis, monograph (Other scientific)
    Abstract [en]

    In this thesis, we study executable behaviours of timed models. The focus is on synthesis of executable code with predictable behaviours from high level abstract models. We assume that a timed system consists of two parts: the control software and the plant (i.e. the environment to be controlled). Both are modelled as timed automata extended with real time tasks. We consider the extended timed automata as design models.

    We present a compilation procedure to transform design models to executable code including a run-time scheduler (run time system) preserving the correctness and schedulability of the models. The compilation procedure has been implemented in a prototype C-code generator for the brickOS operating system included in the Times tool. We also present an animator, based on hybrid automata, to be used to describe a simulated environment (i.e. the plant) for timed systems. The tasks of the hybrid automata define differential equations and the animator uses a differential equations solver to calculate step-wise approximations of real valued variables. The animated objects, described as hybrid automata, are compiled by the Times tool into executable code using a similar procedure as for controller software.

    To demonstrate the applicability of timed automata with tasks as a design language we have developed the control software for a production cell. The production cell is built in LEGO and is controlled by a Hitachi H8 based LEGO-Mindstorms control brick. The control software has been analysed (using the Times tool) for schedulability and other safety properties. Using results from the analysis we were able to avoid generating code for parts of the design that could never be reached, and could also limit the amount of memory allocated for the task queue.

  • 3.
    Backeman, Peter
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    New techniques for handling quantifiers in Boolean and first-order logic2016Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    The automation of reasoning has been an aim of research for a long time. Already in 17th century, the famous mathematician Leibniz invented a mechanical calculator capable of performing all four basic arithmetic operators. Although automatic reasoning can be done in different fields, many of the procedures for automated reasoning handles formulas of first-order logic. Examples of use cases includes hardware verification, program analysis and knowledge representation.

    One of the fundamental challenges in first-order logic is handling quantifiers and the equality predicate. On the one hand, SMT-solvers (Satisfiability Modulo Theories) are quite efficient at dealing with theory reasoning, on the other hand they have limited support for complete and efficient reasoning with quantifiers. Sequent, tableau and resolution calculi are methods which are used to construct proofs for first-order formulas and can use more efficient techniques to handle quantifiers. Unfortunately, in contrast to SMT, handling theories is more difficult.

    In this thesis we investigate methods to handle quantifiers by restricting search spaces to finite domains which can be explored in a systematic manner. We present this approach in two different contexts.

    First we introduce a function synthesis based on template-based quantifier elimination, which is applied to gene interaction computation. The function synthesis is shown to be capable of generating smaller representations of solutions than previous solvers, and by restricting the constructed functions to certain forms we can produce formulas which can more easily be interpreted by a biologist.

    Secondly we introduce the concept of Bounded Rigid E-Unification (BREU), a finite form of unification that can be used to define a complete and sound sequent calculus for first-order logic with equality. We show how to solve this bounded form of unification in an efficient manner, yielding a first-order theorem prover utilizing BREU that is competitive with other state-of-the-art tableau theorem provers.

  • 4.
    Ben Henda, Noomene
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Infinite-state Stochastic and Parameterized Systems2008Doctoral thesis, monograph (Other academic)
    Abstract [en]

    A major current challenge consists in extending formal methods in order to handle infinite-state systems. Infiniteness stems from the fact that the system operates on unbounded data structure such as stacks, queues, clocks, integers; as well as parameterization.

    Systems with unbounded data structure are natural models for reasoning about communication protocols, concurrent programs, real-time systems, etc. While parameterized systems are more suitable if the system consists of an arbitrary number of identical processes which is the case for cache coherence protocols, distributed algorithms and so forth.

    In this thesis, we consider model checking problems for certain fundamental classes of probabilistic infinite-state systems, as well as the verification of safety properties in parameterized systems. First, we consider probabilistic systems with unbounded data structures. In particular, we study probabilistic extensions of Lossy Channel Systems (PLCS), Vector addition Systems with States (PVASS) and Noisy Turing Machine (PNTM). We show how we can describe the semantics of such models by infinite-state Markov chains; and then define certain abstract properties, which allow model checking several qualitative and quantitative problems.

    Then, we consider parameterized systems and provide a method which allows checking safety for several classes that differ in the topologies (linear or tree) and the semantics (atomic or non-atomic). The method is based on deriving an over-approximation which allows the use of a symbolic backward reachability scheme. For each class, the over-approximation we define guarantees monotonicity of the induced approximate transition system with respect to an appropriate order. This property is convenient in the sense that it preserves upward closedness when computing sets of predecessors.

  • 5.
    Bengtson, Jesper
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Formalising process calculi2010Doctoral thesis, monograph (Other academic)
    Abstract [en]

    As the complexity of programs increase, so does the complexity of the models required to reason about them. Process calculi were introduced in the early 1980s and have since then been used to model communication protocols of varying size and scope. Whereas modeling sophisticated  protocols in simple process algebras like CCS or the pi-calculus is doable, expressing the models required is often gruesome and error prone. To combat this, more advanced process calculi were introduced, which significantly reduce the complexity of the models. However, this simplicity comes at a price -- the theories of the calculi themselves instead become gruesome and error prone, establishing their mathematical and logical properties has turned out to be difficult. Many of the proposed calculi have later turned out to be inconsistent.

    The contribution of this thesis is twofold. First we provide methodologies to formalise the meta-theory of process calculi in an interactive theorem prover. These are used to formalise significant parts of the meta-theory of CCS and the pi-calculus in the theorem prover Isabelle, using Nominal Logic to allow for a smooth treatment of the binders. Second we introduce and formalise psi-calculi, a framework for process calculi incorporating several existing ones, including those we already formalised, and which is significantly simpler and substantially more expressive. Our methods scale well as complexity of the calculi increases.

    The formalised results for all calculi include congruence results for both strong and weak bisimilarities, in the case of the pi-calculus for both the early and the late operational semantics. For the finite pi-calculus, we also formalise the proof that the axiomatisation of strong late bisimilarity is sound and complete. We believe psi-calculi to be the state of the art of process calculi, and our formalisation to be the most extensive formalisation of process calculi ever done inside a theorem prover.

  • 6.
    Bengtsson, Johan
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Clocks, DBMs and States in Timed Systems2002Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    Today, computers are used to control various technical systems in our society. In many cases, time plays a crucial role in the operation of computers embedded in such systems. This thesis is about techniques and tools for the analysis of timing behaviours of computer systems. Its main contributions are in the development and implementation of UPPAAL, a tool designed to automate the analysis process of systems modelled as timed automata.

    As the first contribution, we present a software package for timing constraints represented as Difference Bound Matrices. We describe in details, all data-structures and operations for DBMs needed in state-space exploration of timed automata, as well as techniques for efficient implementation. In particular, we have developed two normalisation algorithms to guarantee termination of reachability analysis for timed automata containing constraints on clock differences, that transform DBMs according to not only maximal constants of clocks as in algorithms published in the literature, but also difference constraints appearing in the automata. The second contribution of this thesis is a collection of low level optimisations on the internal data-structures and algorithms of UPPAAL to minimise memory and time consumption. We present compression techniques to allow the state-space of a system to be efficiently stored and manipulated in main memory. We also study super-trace and hash-compaction methods for timed automata to deal with system-models for which the size of available memory is too small to store the explored state-space. Our experiments show that these techniques have greatly improved the performance of UPPAAL. The third contribution is in partial-order reduction techniques for timed-systems. A major problem in automatic verification is the large number of redundant states and transitions introduced by modelling concurrent events as interleaved transitions. We propose a notion of committed locations for timed automata. Committed locations are annotations that can be used for not only modelling of intermediate states within atomic transitions, but also guiding the model checker to ignore unnecessary interleavings in state-space exploration. The notion of committed locations has been generalised to give a local-time semantics for networks of timed automata, which allows for the application of existing partial order reduction techniques to timed systems.

  • 7.
    Bengtsson, Johan
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Efficient symbolic state exploration of timed systems: Theory and implementation2001Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    Timing aspects are important for the correctness of safety-critical systems. It is crucial that these aspects are carefully analysed in designing such systems. UPPAAL is a tool designed to automate the analysis process. In UPPAAL, a system under construction is described as a network of timed automata and the desired properties of the system can be specified using a query language. Then UPPAAL can be used to explore the state space of the system description to search for states violating (or satisfying) the properties. If such states are found, the tool provides diagnostic information, in form of executions leading to the states, to help the desginers, for example, to locate bugs in the design.

    The major problem for UPPAAL and other tools for timed systems to deal with industrial-size applications is the state space explosion. This thesis studies the sources of the problem and develops techniques for real-time model checkers, such as UPPAAL, to attack the problem. As contributions, we have developed the notion of committed locations to model atomicity and local-time semantics for timed systems to allow partial order reductions, and a number of implementation techniques to reduce time and space consumption in state space exploration. The techniques are studied and compared by case studies. Our experiments demonstrate significant improvements on the performance of UPPAAL.

  • 8.
    Berg, Erik
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Efficient and Flexible Characterization of Data Locality through Native Execution Sampling2005Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    Data locality is central to modern computer designs. The widening gap between processor speed and memory latency has introduced the need for a deep hierarchy of caches. Thus, the performance of an application is to a large extent dependent on the amount of data locality the caches can exploit. Some data locality comes naturally from the way most programs are written and the way their data is allocated in the memory. Compilers further try to create data locality by loop transformations and optimized data layout. Different ways of writing a program and/or laying out its data may improve an application’s locality even more. However, it is far from obvious how such a locality optimization can be achieved, especially since the optimizing compiler may have left the optimization job half done. Thus, efficient tools are needed to guide the software developers on their quest for data locality.

    The main contribution of this dissertation is a sample-based novel method for analyzing the data locality of an application. Very sparse data is collected during a single execution of the studied application. The sparse sampling adds a minimum overhead to the execution time, which enables complex applications running realistic data sets to be studied. The architecturalindependent information collected during the execution is fed to a mathematical cache model for predicting the cache miss ratio. The sparsely-collected data can be used to characterize the application’s data locality in respect to almost any possible cache hierarchy, such as complicated multiprocessor memory systems with multilevel cache hierarchies. Any combination of cache size, cache line size and degree of sharing can be modeled. Each new modeled design point takes only a fraction of a second to evaluate, even though the application from which the sampled data was collected may have executed for hours. This makes the tool not just usable for software developers, but also for hardware developers who need to evaluate a huge memory-system design space.

    We also discuss different ways of presenting data-locality information to a programmer in an intuitive and easily interpreted way. Some of the locality metrics we introduce utilize the flexibility of our algorithm and its ability to vary different cache parameters for one run. The dissertation also presents several prototype implementations of tools for profiling the memory system.

  • 9.
    Berg, Erik
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Methods for run time analysis of data locality2003Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    The growing gap between processor clock speed and DRAM access time puts new demands on software and development tools. Deep memory hierarchies and high cache miss penalties in present and emerging computer systems make execution time sensitive to data locality. Therefore, developers of performance-critical applications and optimizing compilers must be aware of data locality and maximize cache utilization to produce fast code. To aid the optimization process and help understanding data locality, we need methods to analyze programs and pinpoint poor cache utilization and possible optimization opportunities.

    Current methods for run-time analysis of data locality and cache behavior include functional cache simulation, often combined with set sampling or time sampling, other regularity metrics based on strides and data streams, and hardware monitoring. However, they all share the trade-off between run-time overhead, accuracy and explanatory power.

    This thesis presents methods to efficiently analyze data locality at run time based on cache modeling. It suggests source-interdependence profiling as a technique for examining the cache behavior of applications and locating source code statements and/or data structures that cause poor cache utilization. The thesis also introduces a novel statistical cache-modeling technique, StatCache. Rather than implementing a functional cache simulator, StatCache estimates the miss ratios of fully-associative caches using probability theory. A major advantage of the method is that the miss ratio estimates can be based on very sparse sampling. Further, a single run of an application is enough to estimate the miss ratio of caches of arbitrary sizes and line sizes and to study both spatial and temporal data locality.

  • 10.
    Berg, Therese
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Regular inference for reactive systems2006Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    Models of reactive systems play a central role in many techniques for verification and analysis of reactive systems. Both a specification of the system and the abstract behavior of the system can be expressed in a formal model. Compliance with the functional parts in the specification can be controlled in different ways. Model checking techniques can be applied to a model of the system or directly to source code. In testing, model-based techniques can generate test suites from specification. A bottleneck in model-based techniques is however to construct a model of the system. This work concerns a technique that automatically constructs a model of a system without access to specification, code or internal structure. We assume that responses of the system to sequences of input can be observed. In this setting, so called regular inference techniques build a model of the system based on system responses to selected input sequences.

    There are three main contributions in this thesis. The first is a survey on the most well-known techniques for regular inference. The second is an analysis of Angluin's algorithm for regular inference on synthesized examples. On a particular type of examples, with prefix-closed languages, typically used to model reactive systems, the required number of input sequences grow approximately quadratically in the number of transitions of the system. However, using an optimization for systems with prefix-closed languages we were able to reduce the number of required input sequences with about 20%. The third contribution is a developed regular inference technique for systems with parameters. This technique aims to better handle entities of communications protocols where messages normally have many parameters of which few determine the subsequent behavior of the system. Experiments with our implementation of the technique confirm a reduction of the required number of input sequences, in comparison with Angluin's algorithm.

  • 11.
    Berglund, Anders
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Learning computer systems in a distributed project course: The what, why, how and where2005Doctoral thesis, monograph (Other academic)
    Abstract [en]

    Senior university students taking an internationally distributed project course in computer systems find themselves in a complex learning situation. To understand how they experience computer systems and act in their learning situation, the what, the why, the how and the where of their learning have been studied from the students’ perspective. The what aspect concerns the students’ understanding of concepts within computer systems: network protocols. The why aspect concerns the students’ objectives to learn computer systems. The how aspect concerns how the students go about learning. The where aspect concerns the students’ experience of their learning environment. These metaphorical entities are then synthesised to form a whole.

    The emphasis on the students’ experience of their learning motivates a phenomenographic research approach as the core of a study that is extended with elements of activity theory. The methodological framework that is developed from these research approaches enables the researcher to retain focus on learning, and specifically the learning of computer systems, throughout.

    By applying the framework, the complexity in the learning is unpacked and conclusions are drawn on the students’ learning of computer systems. The results are structural, qualitative, and empirically derived from interview data. They depict the students’ experience of their learning of computer systems in their experienced learning situation and highlight factors that facilitate learning.

    The results comprise sets of qualitatively different categories that describe how the students relate to their learning in their experienced learning environment. The sets of categories, grouped after the four components (what, why, how and where), are synthesised to describe the whole of the students’ experience of learning computer systems.

    This study advances the discussion about learning computer systems and demonstrates how theoretically anchored research contributes to teaching and learning in the field. Its multi-faceted, multi-disciplinary character invites further debate, and thus, advances the field.

  • 12.
    Berglund, Anders
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    On the understanding of computer network protocols2002Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    How students learn about network protocols is studied in a project-centred, internationally distributed, university course in computer systems taught jointly by two universities. Insights into students' understanding of basic concepts within computer networks are gained through an empirical phenomenographic research approach.

    The use of phenomenography as a research approach makes it possible to learn about computer science, as it is experienced by the students. The context in which the research is carried out and issues concerning by whom the context is experienced, are investigated and form a part of the methodological basis.

    Students' understanding of some protocols that are used within the project, as well as their experience of the general concept of network protocols are investigated, and different ways of experiencing the protocols are discerned. Some aspects that indicate good learning outcomes are identified, such as being capable of understanding a protocol in different ways and of making relevant choices between the ways it could be experienced according to the context in which it appears.

    Based on these results a discussion on learning and teaching is developed. It is argued that a variation in the context in which the protocol is experienced promotes good learning, since different ways of experiencing a protocol are useful with different tasks to hand. A student with a good understanding of network protocols can choose in a situationally relevant way between different ways of experiencing a protocol.

  • 13.
    Bjurefors, Fredrik
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Measurements in opportunistic networks2012Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    Opportunistic networks are a subset of delay tolerant networks where the contacts are unscheduled. Such networks can be formed ad hoc by wireless devices, such as mobile phones and laptops. In this work we use a data-centric architecture for opportunistic networks to evaluate data dissemination overhead, congestion in nodes' buffer, and the impact of transfer ordering. Dissemination brings an overhead since data is replicated to be spread in the network and overhead leads to congestion, i.e., overloaded buffers.

    We develop and implement an emulation testbed to experimentally evaluate properties of opportunistic networks. We evaluate the repeatability of experiments in the emulated testbed that is based on virtual computers. We show that the timing variations are on the order of milliseconds.

    The testbed was used to investigate overhead in data dissemination, congestion avoidance, and transfer ordering in opportunistic networks. We show that the overhead can be reduced by informing other nodes in the network about what data a node is carrying. Congestion avoidance was evaluated in terms of buffer management, since that is the available tool in an opportunistic network, to handle congestion. It was shown that replication information of data objects in the buffer yields the best results. We show that in a data-centric architecture were each data item is valued differently, transfer ordering is important to achieve delivery of the most valued data.

  • 14.
    Bjurefors, Fredrik
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Opportunistic Networking: Congestion, Transfer Ordering and Resilience2014Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    Opportunistic networks are constructed by devices carried by people and vehicles. The devices use short range radio to communicate. Since the network is mobile and often sparse in terms of node contacts, nodes store messages in their buffers, carrying them, and forwarding them upon node encounters. This form of communication leads to a set of challenging issues that we investigate: congestion, transfer ordering, and resilience.

    Congestion occurs in opportunistic networks when a node's buffers becomes full. To be able to receive new messages, old messages have to be evicted. We show that buffer eviction strategies based on replication statistics perform better than strategies that evict messages based on the content of the message.

    We show that transfer ordering has a significant impact on the dissemination of messages during time limited contacts. We find that transfer strategies satisfying global requests yield a higher delivery ratio but a longer delay for the most requested data compared to satisfying the neighboring node's requests.

    Finally, we assess the resilience of opportunistic networks by simulating different types of attacks. Instead of enumerating all possible attack combinations, which would lead to exhaustive evaluations, we introduce a method that use heuristics to approximate the extreme outcomes an attack can have. The method yields a lower and upper bound for the evaluated metric over the different realizations of the attack. We show that some types of attacks are harder to predict the outcome of and other attacks may vary in the impact of the attack due to the properties of the attack, the forwarding protocol, and the mobility pattern.

  • 15.
    Blom, Johan
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Model-Based Protocol Testing in an Erlang Environment2016Doctoral thesis, monograph (Other academic)
    Abstract [en]

    Testing is the dominant technique for quality assurance of software systems. It typically consumes considerable resources in development projects, and is often performed in an ad hoc manner. This thesis is concerned with model-based testing, which is an approach to make testing more systematic and more automated. The general idea in model-based testing is to start from a formal model, which captures the intended behavior of the software system to be tested. On the basis of this model, test cases can be generated in a systematic way. Since the model is formal, the generation of test suites can be automated and with adequate tool support one can automatically quantify to which degree they exercise the tested software.

    Despite the significant improvements on model-based testing in the last 20 years, acceptance by industry has so far been limited. A number of commercially available tools exist, but still most testing in industry relies on manually constructed test cases.

    This thesis address this problem by presenting a methodology and associated tool support, which is intended to be used for model-based testing of communication protocol implementations in industry. A major goal was to make the developed tool suitable for industrial usage, implying that we had to consider several problems that typically are not addressed by the literature on model-based testing. The thesis presents several technical contributions to the area of model-based testing, including

    - a new specification language based on the functional programming language Erlang,

    - a novel technique for specifying coverage criteria for test suite generation, and

    - a technique for automatically generating test suites.

    Based on these developments, we have implemented a complete tool chain that generates and executes complete test suites, given a model in our specification language. The thesis also presents a substantial industrial case study, where our technical contributions and the implemented tool chain are evaluated. Findings from the case study include that test suites generated using (model) coverage criteria have at least as good fault-detection capability as equally large random test suites, and that model-based testing could discover faults in previously well-tested software where previous testing had employed a relaxed validation of requirements.

  • 16.
    Bohlin, Therese
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Regular Inference for Communication Protocol Entities2009Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    A way to create well-functioning computer systems is to automate error detection in the systems. Automated techniques for finding errors, such as testing and formal verification, requires a model of the system. The technique for constructing deterministic finite automata (DFA) models, without access to the source code, is called regular inference. The technique provides sequences of input, so called membership queries, to a system, observes the responses, and infers a model from the input and responses.

    This thesis presents work to adapt regular inference to a certain kind of systems: communication protocol entities. Such entities interact by sending and receiving messages consisting of a message type and a number of parameters, each of which potentially can take on a large number of values. This may cause a model of a communication protocol entity inferred by regular inference, to be very large and take a long time to infer. Since regular inference creates a model from the observed behavior of a communication protocol entity, the model may be very different from a designer's model of the system's source code.

    This thesis presents adaptations of regular inference to infer more compact models and use less membership queries. The first contribution is a survey over three algorithms for regular inference. We present their similarities and their differences in terms of the required number of membership queries. The second contribution is an investigation on how many membership queries a common regular inference algorithm, the L* algorithm by Angluin, requires for randomly generated DFAs and randomly generated DFAs with a structure common for communication protocol entities. In comparison, the DFAs with a structure common for communication protocol entities require more membership queries. The third contribution is an adaptation of regular inference to communication protocol entities which behavior foremost are affected by the message types. The adapted algorithm avoids asking membership queries containing messages with parameter values that results in already observed responses. The fourth contribution is an approach for regular inference of communication protocol entities which communicate with messages containing parameter values from very large ranges. The approach infers compact models, and uses parameter values taken from a small portion of their ranges in membership queries. The fifth contribution is an approach to infer compact models of communication protocol entities which have a similar partitioning of an entity's behavior into control states as in a designer's model of the protocol.

  • 17.
    Borgh, Joakim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
    Attribute-Based Encryption in Systems with Resource Constrained Devices in an Information Centric Networking Context2016Independent thesis Advanced level (professional degree), 20 credits / 30 HE creditsStudent thesis
    Abstract [en]

    An extensive analysis of attribute-based encryption (ABE) in systems with resource constrained devices is performed. Two system solutions of how ABE can be performed in such systems are proposed, one where the ABE operations are performed at the resource constrained devices and one where ABE is performed at a powerful server. The system solutions are discussed with three different ABE schemes. Two of the schemes are the traditional key policy ABE (KP-ABE) and ciphertext policy ABE (CP-ABE). The third scheme is using KP-ABE to simulate CP-ABE, in an attempt to benefit from KP-ABE being computationally cheaper than CP-ABE while maintaining the intuitive way of using CP-ABE.

    ABE is a computationally expensive encryption method which might not be feasible to perform at the resource constrained sensors, depending on the hardware.

    An implementation of a CP-ABE scheme with a 128 bit security level was written and used to evaluate the feasibility of ABE on a sensor equipped with an ARM Cortex-M3 processor having 32 kB RAM and 256 kB flash. It is possible to perform CP-ABE on the sensor used in this project. The limiting factor of feasibility of ABE on the sensor is the RAM size. In this case policy sizes up to 12 attributes can be performed on the sensor.

    The results give an idea of the feasibility of encryption with ABE on sensors. In addition to the results several ways of improving performance of ABE on the sensor are discussed.

  • 18.
    Bälter Eronell, Sofia
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
    Lindvall, Lisa
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
    Framtagning av affärsmodell inom Internet of Things: En studie om hur ett IT-konsultbolag kan verka som integratör inom IoT-ekosystemet2016Independent thesis Advanced level (professional degree), 20 credits / 30 HE creditsStudent thesis
    Abstract [en]

    This study examines how an Information Technology consulting firm can act as an integrator for the Internet of Things. The aim is to contribute to a greater understanding of how the IoT-ecosystem looks and what roles an integrator can take in collaboration with partners. In order to create a deeper understanding of the topic a qualitative study was conducted with Softhouse's partners, customers, and themselves, in order to place them within the IoT-ecosystem. The study focused on examining how IoT solutions can be implemented in the forestry industry. The results show that Softhouse has a great potential to offer IoT solutions by a solid collaboration with partners. They should focus on becoming experts in data analysis through training and recruitment. Selection of partners for different projects depends on its size, complexity

    and type. Through analysis and by using the business model Business Model Canvas it is possible to see which partners are most suitable for which type of project. This was applied to two such cases with clients in the forest industry; Södra Skog and APEA Mobile Security Solutions. 

  • 19.
    Cambazoglu, Volkan
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Protocol, mobility and adversary models for the verification of security2016Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    The increasing heterogeneity of communicating devices, ranging from resource constrained battery driven sensor nodes to multi-core processor computers, challenges protocol design. We examine security and privacy protocols with respect to exterior factors such as users, adversaries, and computing and communication resources; and also interior factors such as the operations, the interactions and the parameters of a protocol.

    Users and adversaries interact with security and privacy protocols, and even affect the outcome of the protocols. We propose user mobility and adversary models to examine how the location privacy of users is affected when they move relative to each other in specific patterns while adversaries with varying strengths try to identify the users based on their historical locations. The location privacy of the users are simulated with the support of the K-Anonymity protection mechanism, the Distortion-based metric, and our models of users' mobility patterns and adversaries' knowledge about users.

    Security and privacy protocols need to operate on various computing and communication resources. Some of these protocols can be adjusted for different situations by changing parameters. A common example is to use longer secret keys in encryption for stronger security. We experiment with the trade-off between the security and the performance of the Fiat–Shamir identification protocol. We pipeline the protocol to increase its utilisation as the communication delay outweighs the computation.

    A mathematical specification based on a formal method leads to a strong proof of security. We use three formal languages with their tool supports in order to model and verify the Secure Hierarchical In-Network Aggregation (SHIA) protocol for Wireless Sensor Networks (WSNs). The three formal languages specialise on cryptographic operations, distributed systems and mobile processes. Finding an appropriate level of abstraction to represent the essential features of the protocol in three formal languages was central.

  • 20.
    Carlström, Jakob
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Reinforcement learning for admission control and routing2000Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    When a user requests. a connection to another user or a computer in a communications network, a routing algorithm selects a path for transferring the resulting data stream. If all suitable paths are busy, the user request cannot beserved, and is blocked. A routing algorithm that minimizes this blocking probability results in satisfied users, and maximizes the network operator's revenue. In some cases, it may even be advantageous to block a request from one user, to make it possible to serve other users better. This thesis presents improved and partially new algorithms, based on reinforcement learning, which optimize the way a network is shared.

    A main contribution of the thesis is the development of algorithms thatadapt to arrivals of user requests that are correlated over time. These methodsare shown to increase network utilization in cases where the request arrivalprocesses are statistically self-similar. Another main contribution is gainscheduled routing, which reduces the computational cost associated withmaking routing decisions. The thesis also demonstrates how to integrate theconcept of max-min fairness into reinforcement learning routing.

  • 21.
    Cassel, Sofia
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Learning Component Behavior from Tests: Theory and Algorithms for Automata with Data2015Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    Formal models are often used to describe the behavior of a computer program or component. Behavioral models have many different usages, e.g., in model-based techniques for software development and verification,such as model checking and model based testing.

    The application of model-based techniques is hampered by the current lack of adequate models for most actual systems, largely due to the significant manual effort typically needed to construct them. To remedy this, automata learning techniques (whereby models can be inferred by performing tests on a component) have been developed for finite automata that capture control flow. However, many usages requiremodels also to capture data flow, i.e., how behavior is affected by data values in method invocations and commands. Unfortunately, techniques are less developed for models that combinecontrol flow with data.

    In this thesis, we extend automata learning to infer automata models that captureboth control flow and data flow. We base our technique on a corresponding extension of classical automata theoryto capture data.

    We define a formalism for register automata, a model that extends finite automata by adding registers that can store data values and be used in guards and assignments on transitions. Our formalism is parameterized on a theory, i.e., a set of relations on a data domain. We present a Nerode congruence for the languages that our register automata can recognize, and provide a Myhill-Nerode theorem for constructing canonical register automata, thereby extending classical automata theory to register automata.

    We also present a learning algorithm for register automata: the new SL* algorithm, which extends the well-known L* algorithm for finite automata. The SL* algorithm is based on our new Nerode congruence, and uses a novel technique to infer symbolic data constraints on parameters. We evaluated our algorithm in a black-box scenario, inferring, e.g., the connection establishment phase of TCP and a priority queue, in addition to a number of smaller models. The SL* algorithm is implemented in a tool, which allows for use in more realistic settings, e.g., where models have both input and output, and for directly inferring Java classes.

  • 22.
    Ceballos, Germán
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Modeling the interactions between tasks and the memory system2017Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    Making computer systems more energy efficient while obtaining the maximum performance possible is key for future developments in engineering, medicine, entertainment, etc. However it has become a difficult task due to the increasing complexity of hardware and software, and their interactions. For example, developers have to deal with deep, multi-level cache hierarchies on modern CPUs, and keep busy thousands of cores in GPUs, which makes the programming process more difficult.

    To simplify this task, new abstractions and programming models are becoming popular. Their goal is to make applications more scalable and efficient, while still providing the flexibility and portability of old, widely adopted models. One example of this is task-based programming, where simple independent tasks (functions) are delegated to a runtime system which orchestrates their execution. This approach has been successful because the runtime can automatically distribute work across hardware cores and has the potential to minimize data movement and placement (e.g., being aware of the cache hierarchy).

    To build better runtime systems, it is crucial to understand bottlenecks in the performance of current and future multicore systems. In this thesis, we provide fast, accurate and mathematically-sound models and techniques to understand the execution of task-based applications concerning three key aspects: memory behavior (data locality), scheduling, and performance. With these methods, we lay the groundwork for improving runtime system, providing insight into the interplay between the schedule's behavior, data reuse through the cache hierarchy, and the resulting performance.

  • 23.
    Ceballos, Germán
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Understanding Task Parallelism: Providing insight into scheduling, memory, and performance for CPUs and Graphics2018Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    Maximizing the performance of computer systems while making them more energy efficient is vital for future developments in engineering, medicine, entertainment, etc. However, the increasing complexity of software, hardware, and their interactions makes this task difficult. Software developers have to deal with complex memory architectures such as multilevel caches on modern CPUs and keeping thousands of cores busy in GPUs, which makes the programming process harder.

    Task-based programming provides high-level abstractions to simplify the development process. In this model, independent tasks (functions) are submitted to a runtime system, which orchestrates their execution across hardware resources. This approach has become popular and successful because the runtime can distribute the workload across hardware resources automatically, and has the potential to optimize the execution to minimize data movement (e.g., being aware of the cache hierarchy).

    However, to build better runtime systems, we now need to understand bottlenecks in the performance of current and future multicore architectures. Unfortunately, since most current work was designed for sequential or thread-based workloads, there is an overall lack of tools and methods to gain insight about the execution of these applications, allowing both the runtime and the programmers to detect potential optimizations.

    In this thesis, we address this lack of tools by providing fast, accurate and mathematically-sound models to understand the execution of task-based applications. In particular, we center these models around three key aspects of the execution: memory behavior (data locality), scheduling, and performance. Our contributions provide insight into the interplay between the schedule's behavior, data reuse through the cache hierarchy, and the resulting performance. These contributions lay the groundwork for improving runtime systems. We first apply these methods to analyze a diverse set of CPU applications, and then leverage them to one of the most common workloads in current systems: graphics rendering on GPUs.

  • 24.
    D'Angelo, Laura
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
    Evaluation of code generation in agile software development of embedded systems2018Independent thesis Advanced level (professional degree), 20 credits / 30 HE creditsStudent thesis
    Abstract [en]

    Generating code from software models is considered to be a new generation leap within software development methods. The objective of this M.Sc. project is to evaluate how different approaches to modelling and code generation affect embedded systems software development and propose recommendations on how to improve software development. Two product areas at Saab Surveillance EW Systems in Järfälla, Stockholm, are used as study objects.

    A research overview is made to highlight themes regarding modelling, code generation and software development in general. Based on these, interviews are held with system engineers and software developers at each product area, where they use different modelling and code generation approaches. The two development processes are described thoroughly. Challenges and advantages related to each area’s approach are investigated.

    Software development within product area A is affected by the product complexity and the larger scale of the development, including projects running over a longer time with more teams involved. Recommendations include enabling code generation by aligning it with other investments on process improvement and limiting the approach to generating some system components. Software developers within product area B can use full code generation, enabled by the limited product complexity. The product area is affected by software standards and external requirements on the process. Recommendations include extending the modelling approach to make it easier to trace functionality from system to software level. Conclusions are that both product areas can apply modelling and code generation to more software development activities to improve their respective development processes.

  • 25.
    Daniels, Mats
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Developing and Assessing Professional Competencies: a Pipe Dream?: Experiences from an Open-Ended Group Project Learning Environment2011Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    Professional competencies are explicitly identified in the primary learning outcomes for science and engineering degrees at many tertiary institutions.  Fulfillment of the requirements to equip our students with these skills, while formally acknowledged as important by all stakeholders, can be hard to demonstrate in practice.  Most degree awarding institutions would have difficulties if asked to document where in degree programs such competencies are developed.

    The work in this thesis addresses the issue of professional competencies from several angles.  The Open-Ended Group Project (OEGP) concept is introduced and proposed as an approach to constructing learning environments in which students’ development of professional competencies can be stimulated and assessed.  Scholarly, research-based development of the IT in Society course unit (ITiS) is described and analyzed in order to present ideas for tailoring OEGP-based course units towards meeting learning objectives related to professional competence.  Work in this thesis includes an examination of both the meanings attributed to the term professional competencies, and methods which can be used to assess the competencies once they are agreed on.

    The empirical work on developing ITiS is based on a framework for educational research, which has been both refined and extended as an integral part of my research.  The action research methodology is presented and concrete examples of implementations of different pedagogical interventions, based on the methodology, are given.  The framework provides support for relating a theoretical foundation to studies, or development, of learning environments.  The particular theoretical foundation for the examples in this thesis includes, apart from the action research methodology, constructivism, conceptual change, threshold concepts, communities of practice, ill-structured problem solving, the reflective practicum, and problem based learning.

    The key finding in this thesis is that development and assessment of professional competencies is not a pipe dream.  Assessment can be accomplished, and the OEGP concept provides a flexible base for creating an appropriate learning environment for this purpose.

  • 26.
    Davari, Mahdad
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Architecture and Computer Communication.
    Advances Towards Data-Race-Free Cache Coherence Through Data Classification2017Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    Providing a consistent view of the shared memory based on precise and well-defined semantics—memory consistency model—has been an enabling factor in the widespread acceptance and commercial success of shared-memory architectures. Moreover, cache coherence protocols have been employed by the hardware to remove from the programmers the burden of dealing with the memory inconsistency that emerges in the presence of the private caches. The principle behind all such cache coherence protocols is to guarantee that consistent values are read from the private caches at all times.

    In its most stringent form, a cache coherence protocol eagerly enforces two invariants before each data modification: i) no other core has a copy of the data in its private caches, and ii) all other cores know where to receive the consistent data should they need the data later. Nevertheless, by partly transferring the responsibility for maintaining those invariants to the programmers, commercial multicores have adopted weaker memory consistency models, namely the Total Store Order (TSO), in order to optimize the performance for more common cases.

    Moreover, memory models with more relaxed invariants have been proposed based on the observation that more and more software is written in compliance with the Data-Race-Free (DRF) semantics. The semantics of DRF software can be leveraged by the hardware to infer when data in the private caches might be inconsistent. As a result, hardware ignores the inconsistent data and retrieves the consistent data from the shared memory. DRF semantics therefore removes from the hardware the burden of eagerly enforcing the strong consistency invariants before each data modification. Instead, consistency is guaranteed only when needed. This results in manifold optimizations, such as reducing the energy consumption and improving the performance and scalability. The efficiency of detecting and discarding the inconsistent data is an important factor affecting the efficiency of such coherence protocols. For instance, discarding the consistent data does not affect the correctness, but results in performance loss and increased energy consumption.

    In this thesis we show how data classification can be leveraged as an effective tool to simplify the cache coherence based on the DRF semantics. In particular, we introduce simple but efficient hardware-based private/shared data classification techniques that can be used to efficiently detect the inconsistent data, thus enabling low-overhead and scalable cache coherence solutions based on the DRF semantics.

  • 27.
    David, Alexandre
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Hierarchical Modeling and Analysis of Real Time Systems2003Doctoral thesis, monograph (Other academic)
    Abstract [en]

    UPPAAL is a tool for model-checking real-time systems developed jointly by Uppsala University and Aalborg University. It has been applied successfully in case studies ranging from communication protocols to multimedia applications. The tool is designed to verify systems that can be modeled as networks of timed automata. But it lacks support for systems with hierarchical structures, which makes the construction of large models difficult. In this thesis we improve the efficiency of UPPAAL with new data structures and extend its modeling language and its engine to support hierarchical constructs.

    To investigate the limits of UPPAAL, we model and analyze an industrial fieldbus communication protocol. To our knowledge, this case study is the largest application UPPAAL has been confronted to and we managed to verify the models. However, the hierarchical structure of the protocol is encoded as a network of automata without hierarchy, which artificially complicates the model. It turns out that we need to improve performance and enrich the modeling language.

    To attack the performance bottlenecks, we unify the two central structures of the UPPAAL engine, the passed and waiting lists, and improve memory management to take advantage of data sharing between states. We present experimental results that demonstrate improvements by a factor 2 in time consumption and a factor 5 in memory consumption.

    We enhance the modeling capabilities of UPPAAL by extending its input language with hierarchical constructs to structure the models. We have developed a verification engine that supports modeling of hierarchical systems without penalty in performance. To further benefit from the structures of models, we present an approximation technique that utilizes hierarchy in verification.

    Finally, we propose a new architecture to integrate the different verification techniques into a common framework. It is designed as a pipeline built with components that are changed to fit particular experimental configurations and to add new features. The new engine of UPPAAL is based on this architecture. We believe that the architecture is applicable to other verification tools.

  • 28.
    David, Alexandre
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Practical verification of real-time systems2001Licentiate thesis, monograph (Other scientific)
    Abstract [en]

    Formal methods are becoming mature enough to be used on nontrivial examples. They are particularly well fitted for real-time systems whose correctness is defined in terms of correct responses at correct times. Most common real-time systems are of reasonable size and can therefore be handled by an automatic verification tool such as Uppaal. Unfortunately the application of such techniques is not widely spread.

    This thesis presents advances in making formal techniques more accessable technology for system development and analysis. As the first contribution, we report on an industrial case study to show that model checkers can be used for debugging and error localization. We shall present a number of abstraction techniques applied in the case study to avoid the state explosion problem. As the second contribution, we have developed a hierarchical extension of timed automata to enable more structured, compact, and more complex descriptions of systems by the users. Such a hierarchical representation is better suited for abstraction and expected to give better searching algorithms. Finally we present a hybrid animation system serving as a plug-in module for model-checkers to improve features for modelling and simulation.

  • 29.
    Deneux, Johann
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Verification of Parameterized and Timed Systems: Undecidability Results and Efficient Methods2006Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    Software is finding its way into an increasing range of devices (phones, medical equipment, cars...). A challenge is to design verification methods to ensure correctness of software.

    We focus on model checking, an approach in which an abstract model of the implementation and a specification of requirements are provided. The task is to answer automatically whether the system conforms with its specification.We concentrate on (i) timed systems, and (ii) parameterized systems.

    Timed systems can be modeled and verified using the classical model of timed automata. Correctness is translated to language inclusion between two timed automata representing the implementation and the specification. We consider variants of timed automata, and show that the problem is at best highly complex, at worst undecidable.

    A parameterized system contains a variable number of components. The problem is to verify correctness regardless of the number of components. Regular model checking is a prominent method which uses finite-state automata. We present a semi-symbolic minimization algorithm combining the partition refinement algorithm by Paige and Tarjan with decision diagrams.

    Finally, we consider systems which are both timed and parameterized: Timed Petri Nets (TPNs), and Timed Networks (TNs). We present a method for checking safety properties of TPNs based on forward reachability analysis with acceleration. We show that verifying safety properties of TNs is undecidable when each process has at least two clocks, and explore decidable variations of this problem.

  • 30.
    d'Orso, Julien
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    New Directions in Symbolic Model Checking2003Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    In today's computer engineering, requirements for generally high reliability have pushed the notion of testing to its limits. Many disciplines are moving, or have already moved, to more formal methods to ensure correctness. This is done by comparing the behavior of the system as it is implemented against a set of requirements. The ultimate goal is to create methods and tools that are able to perform this kind of verfication automatically: this is called Model Checking.

    Although the notion of model checking has existed for two decades, adoption by the industry has been hampered by its poor applicability to complex systems. During the 90's, researchers have introduced an approach to cope with large (even infinite) state spaces: Symbolic Model Checking. The key notion is to represent large (possibly infinite) sets of states by a small formula (as opposed to enumerating all members). In this thesis, we investigate applying symbolic methods to different types of systems:

    Parameterized systems. We work whithin the framework of Regular Model Chacking. In regular model checking, we represent a global state as a word over a finite alphabet. A transition relation is represented by a regular length-preserving transducer. An important operation is the so-called transitive closure, which characterizes composing a transition relation with itself an arbitrary number of times. Since completeness cannot be achieved, we propose methods of computing closures that work as often as possible.

    Games on infinite structures. Infinite-state systems for which the transition relation is monotonic with respect to a well quasi-ordering on states can be analyzed. We lift the framework of well quasi-ordered domains toward games. We show that monotonic games are in general undecidable. We identify a subclass of monotonic games: downward-closed games. We propose an algorithm to analyze such games with a winning condition expressed as a safety property.

    Probabilistic systems. We present a framework for the quantitative analysis of probabilistic systems with an infinite state-space: given an initial state sinit, a set F of final states, and a rational Θ > 0, compute a rational ρ such that the probability of reaching F form sinit is between ρ and ρ + Θ. We present a generic algorithm and sufficient conditions for termination.

  • 31.
    Edström, Rickard
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
    Internet caching - sizing and placement for dynamic content2015Independent thesis Advanced level (professional degree), 20 credits / 30 HE creditsStudent thesis
    Abstract [en]

    Traffic volumes on the Internet continue to increase, with the same links carrying the same data multiple times. In-network caching can alleviate much of the redundant traffic by storing popular items close to the users. This was a master thesis project that involved building on existing research and simulators, simulating a multi-level hierarchical network cache system and its resulting performance, with varying parameters such as placement and sizing of the individual cache nodes. One of the goals of the thesis work was to improve and integrate the simulation frameworks used as a starting point. Another goal was to run simulations with the improved framework and shed light on how a high Quality of Experience (QoE) can be achieved within this kind of cache system, varying the input parameters. An improved and integrated simulation framework was produced, including improved visualization capabilities. Using this improved simulation framework, the behavior of the cache system was studied, in particular how the system behaves with static and dynamic cache sizing approaches. Conclusions drawn are e.g. that the dynamic sizing approach deployed can be a good way to achieve a high QoE. Finally, future research opportunities are identified.

  • 32.
    Ekberg, Pontus
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Models and Complexity Results in Real-Time Scheduling Theory2015Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    When designing real-time systems, we want to prove that they will satisfy given timing constraints at run time. The main objective of real-time scheduling theory is to analyze properties of mathematical models that capture the temporal behaviors of such systems. These models typically consist of a collection of computational tasks, each of which generates an infinite sequence of task activations. In this thesis we study different classes of models and their corresponding analysis problems.

    First, we consider models of mixed-criticality systems. The timing constraints of these systems state that all tasks must meet their deadlines for the run-time scenarios fulfilling certain assumptions, for example on execution times. For the other scenarios, only the most important tasks must meet their deadlines. We study both tasks with sporadic activation patterns and tasks with complicated activation patterns described by arbitrary directed graphs. We present sufficient schedulability tests, i.e., methods used to prove that a given collection of tasks will meet their timing constraints under a particular scheduling algorithm.

    Second, we consider models where tasks can lock mutually exclusive resources and have activation patterns described by directed cycle graphs. We present an optimal scheduling algorithm and an exact schedulability test.

    Third, we address a pair of longstanding open problems in real-time scheduling theory. These concern the computational complexity of deciding whether a collection of sporadic tasks are schedulable on a uniprocessor. We show that this decision problem is strongly coNP-complete in the general case. In the case where the asymptotic resource utilization of the tasks is bounded by a constant smaller than 1, we show that it is weakly coNP-complete.

  • 33.
    Eklöv, David
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Efficient methods for application performance analysis2011Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    To reduce latency and increase bandwidth to memory, modern microprocessors are designed with deep memory hierarchies including several levels of caches. For such microprocessors, the service time for fetching data from off-chip memory is about two orders of magnitude longer than fetching data from the level-one cache. Consequently, the performance of applications is largely determined by how well they utilize the caches in the memory hierarchy, captured by their miss ratio curves. However, efficiently obtaining an application's miss ratio curve and interpreting its performance implications is hard. This task becomes even more challenging when analyzing application performance on multicore processors where several applications/threads share caches and memory bandwidths. To accomplish this, we need powerful techniques that capture applications' cache utilization and provide intuitive performance metrics.

    In this thesis we present three techniques for analyzing application performance, StatStack, StatCC and Cache Pirating. Our main focus is on providing memory hierarchy related performance metrics such as miss ratio, fetch ratio and bandwidth demand, but also execution rate. These techniques are based on profiling information, requiring both runtime data collection and post processing. For such techniques to be broadly applicable the data collection has to have minimal impact on the profiled application, allow profiling of unmodified binaries, and not depend on custom hardware and/or operating system extensions. Furthermore, the information provided has to be accurate and easy to interpret by programmers, the runtime environment and compilers.

    StatStack estimates an application's miss ratio curve, StatCC estimates the miss ratio of co-running application sharing the last-level cache and Cache Pirating measures any desired performance metric available through hardware performance counters as a function of cache size. We have experimentally shown that our methods are both efficient and accurate. The runtime information required by StatStack and StatCC can be collected with an average runtime overhead of 40%. The Cache Pirating method measures the desired performance metrics with an average runtime overhead of 5%.

  • 34.
    Eklöv, David
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Profiling Methods for Memory Centric Software Performance Analysis2012Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    To reduce latency and increase bandwidth to memory, modern microprocessors are often designed with deep memory hierarchies including several levels of caches. For such microprocessors, both the latency and the bandwidth to off-chip memory are typically about two orders of magnitude worse than the latency and bandwidth to the fastest on-chip cache. Consequently, the performance of many applications is largely determined by how well they utilize the caches and bandwidths in the memory hierarchy. For such applications, there are two principal approaches to improve performance: optimize the memory hierarchy and optimize the software. In both cases, it is important to both qualitatively and quantitatively understand how the software utilizes and interacts with the resources (e.g., cache and bandwidths) in the memory hierarchy.

    This thesis presents several novel profiling methods for memory-centric software performance analysis. The goal of these profiling methods is to provide general, high-level, quantitative information describing how the profiled applications utilize the resources in the memory hierarchy, and thereby help software and hardware developers identify opportunities for memory related hardware and software optimizations. For such techniques to be broadly applicable the data collection should have minimal impact on the profiled application, while not being dependent on custom hardware and/or operating system extensions. Furthermore, the resulting profiling information should be accurate and easy to interpret.

    While several use cases are presented, the main focus of this thesis is the design and evaluation of the core profiling methods. These core profiling methods measure and/or estimate how high-level performance metrics, such as miss-and fetch ratio; off-chip bandwidth demand; and execution rate are affected by the amount of resources the profiled applications receive. This thesis shows that such high-level profiling information can be accurately obtained with very little impact on the profiled applications and without requiring costly simulations or custom hardware support.

  • 35.
    El Shobaki, Mohammed
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    On-chip monitoring for non-intrusive hardware/software observability2004Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    The increased complexity in today's state-of-the-art computer systems make them hard to analyse, test, and debug. Moreover, the advances in hardware technology give system designers enormous possibilities to explore hardware as a means to implement performance demanding functionality. We see examples of this trend in novel microprocessors, and Systems-on-Chip, that comprise reconfigurable logic allowing for hardware/software co-design. To succeed in developing computer systems based on these premises, it is paramount to have efficient design tools and methods.

    An important aspect in the development process is observability, i.e., the ability to observe the system's behaviour at various levels of detail. These observations are required for many applications: when looking for design errors, during debugging, during performance assessments and fine-tuning of algorithms, for extraction of design data, and a lot more. In real-time systems, and computers that allow for concurrent process execution, the observability must be obtained without compromising the system's functional and timing behaviour.

    In this thesis we propose a monitoring system that can be used for nonintrusive run-time observations of real-time and concurrent computer systems. The monitoring system, designated Multipurpose/Multiprocessor Application Monitor (MAMon), is based on a hardware probe unit (IPU) which is integrated with the observed system s hardware. The IPU collects process-level events from a hardware Real-Time Kernel (RTK), without perturbing the system, and transfers the events to an external computer for analysis, debugging, and visualisation. Moreover, the MAMon concept also features hybrid monitoring for collection of more fine-grained information, such as program instructions and data flows.

    We describe MAMon s architecture, the implementation of two hardware prototypes, and validation of the prototypes in different case-studies. The main conclusion is that process level events can be traced non-intrusively by integrating the IPU with a hardware RTK. Furthermore, the IPU's small footprint makes it attractive for SoC designs, as it provides increased system observability at a low hardware cost.

  • 36.
    Engblom, Jakob
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Processor Pipelines and Static Worst-Case Execution Time Analysis2002Doctoral thesis, monograph (Other academic)
    Abstract [en]

    Worst-Case Execution Time (WCET) estimates for programs are necessary when building real-time systems. They are used to ensure timely responses from interrupts, to guarantee the throughput of cyclic tasks, as input to scheduling and schedule analysis algorithms, and in many other circumstances. Traditionally, such estimates have been obtained either by measurements or labor-intensive manual analysis, which is both time consuming and error-prone. Static worst-case execution time analysis is a family of techniques that promise to quickly provide safe execution time estimates for real-time programs, simultaneously increasing system quality and decreasing the development cost. This thesis presents several contributions to the state-of-the-art in WCET analysis.

    We present an overall architecture for WCET analysis tools that provides a framework for implementing modules. Within the stable interfaces provided, modules can be independently replaced, making it easy to customize a tool for a particular target and perform performance-precision trade-offs.

    We have developed concrete techniques for analyzing and representing the timing behavior of programs running on pipelined processors. The representation and analysis is more powerful than previous approaches in that pipeline timing effects across more than pairs of instructions can be handled, and in that no assumptions are made about the program structure. The analysis algorithm relies on a trace-driven processor simulator instead of a special-purpose processor model. This allows us to use existing simulators to adapt the analysis to a new target platform, reducing the retargeting effort.

    We have defined a formal mathematical model of processor pipelines, which we use to investigate the properties of pipelines and WCET analysis. We prove several interesting properties of processors with in-order issue, such as the freedom from timing anomalies and the fundamental safety of WCET analysis for certain classes of pipelines. We have also constructed a number of examples that demonstrate that tight and safe WCET analysis for pipelined processors might not be as easy as once believed.

    Considering the link between the analysis methods and the real world, we discuss how to build accurate software models of processor hardware, and the conditions under which accuracy is achievable.

  • 37.
    Eriksson, Emil
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
    System collaboration and information sharing using DDS technology2016Independent thesis Advanced level (professional degree), 20 credits / 30 HE creditsStudent thesis
    Abstract [en]

    Just as the Internet of Things is set to change how devices are being used and connected in society in general, the Industrial Internet of Things will change the industries. In an industrial production line there are often many heterogeneous devices, and the requirements on the real-time properties of the communication between them are often strict. Creating a communication solution for the different devices, that also meet such requirements, is difficult. The traditional way for industrial devices to communicate is directly with each other or via a central point, but this communication solution is inflexible and difficult to scale up.

    One possible way to make communication and information sharing between devices easier is to use a dedicated middleware to handle the communication. One middleware standard is the Data Distribution Service (DDS) defined by the Object Management Group. In this thesis a DDS middleware from a specific vendor (vendor name is removed due to company confidentiality) is implemented and evaluated.

    The middleware is evaluated based on (1) an implementation in a prototype which shows how the middleware performs in a real-life industrial context, and (2) a simulation that showcases the potential of the technology.

    The DDS middleware was shown to function with a specific set of existing industrial hardware and software. The real-time properties of the communication system were studied and found to be around 3.5 times slower, when using the prototype setup, than those of the replaced communication solution. However, the round trip latency was still only 2 ms on average and 4.1 ms maximum when using the preferred settings.

    The simulation showed that there is potential for the DDS technology to be used in more advanced scenarios and that it should be investigated further.

  • 38.
    Eriksson, Joakim
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Detailed simulation of heterogeneous wireless sensor networks2009Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    Wireless sensor networks consist of many small nodes. Each node has a small microprocessor, a radio chip, some sensors, and is usually battery powered which limits network lifetime. Applications of wireless sensor networks range from environmental monitoring and health-care to industrial automation and military surveillance.

    Since the nodes are battery powered and communication consumes more than computation much of the research focuses on power efficient communication. One of the problems is however to measure the power consumption and communication quality of the different solutions.

    Simulation of sensor networks can greatly increase development speed and also be used for evaluating power consumption as well as communication quality. Simulation experiments typically give easier access to fine grained results than corresponding real-world experiments. The problem with simulators is that it is hard to show that a simulation experiment corresponds well with a similar real-world experiment.

    This thesis studies how detailed simulation of wireless sensor networks can be validated for accuracy and also shows several important uses of detailed simulation such as power consumption profiling and interoperability testing. Both of them represent important topics in today's wireless sensor network research and development.

    The results of the thesis are the simulation platform COOJA/MSPSim and that we show that MAC-protocol experiments performed in our simulator COOJA/MSPSim correspond well with experiments performed in our testbed. We also show that using COOJA/MSPSim any software running in the simulation can be power profiled.

  • 39.
    Ermedahl, Andreas
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    A Modular Tool Architecture for Worst-Case Execution Time Analysis2003Doctoral thesis, monograph (Other academic)
    Abstract [en]

    Estimations of the Worst-Case Execution Time (WCET) are required in providing guarantees for timing of programs used in computer controlled products and other real-time computer systems. To derive program WCET estimates, both the properties of the software and the hardware must be considered. The traditional method to obtain WCET estimates is to test the system and measure the execution time. This is labour-intensive and error-prone work, which unfortunately cannot guarantee that the worst case is actually found. Static WCET analyses, on the other hand, are capable of generating safe WCET estimates without actually running the program. Such analyses use models of program flow and hardware timing to generate WCET estimates.

    This thesis includes several contributions to the state-of-the-art in static WCET analysis:

    (1) A tool architecture for static WCET analysis, which divides the WCET analysis into several steps, each with well-defined interfaces. This allows independent replacement of the

    modules implementing the different steps, which makes it easy to customize a WCET tool for particular target hardware and analysis needs.

    (2) A representation for the possible executions of a program. Compared to previous approaches, our representation extends the type of program flow information possible to express and handle in WCET analysis.

    (3) A calculation method which explicitly extracts a longest program execution path. The method is more efficient than previously presented path-based methods, with a computational complexity close to linear in the size of the program.

    (4) A calculation method using integer linear programming or constraint programming techniques for calculating the WCET estimate. The method extends the power of such calculation methods to handle new types of flow and timing information.

    (5) A calculation method that first uses flow information to divide the program into smaller parts, then calculates individual WCET estimates for these parts, and finally combines these into an overall program WCET. This novel approach avoids potential complexity problems, while still providing high precision WCET estimates.

    We have additionally implemented a prototype WCET analysis tool based on the proposed architecture. This tool is used for extensive evaluation of the precision and performance of our proposed methods. The results indicate that it is possible to perform WCET analysis in a modular fashion, and that this analysis produces high quality WCET estimates.

  • 40.
    Fersman, Elena
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    A Generic Approach to Schedulability Analysis of Real-Time Systems2003Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    This thesis presents a framework for design, analysis, and implementation of embedded systems. We adopt a model of timed automata extended with asynchronous processes i.e. tasks triggered by events. A task is an executable program characterized by its worst-case execution time and deadline, and possibly other parameters such as priorities etc. for scheduling. The main idea is to associate each location of an automaton with a task (or a set of tasks). A transition leading to a location denotes an event triggering the tasks and the clock constraint on the transition specifies the possible arrival times of the event. This yields a model for real-time systems expressive enough to describe concurrency and synchronization, and tasks with (or without) combinations of timing, precedence and resource constraints, which may be periodic, sporadic, preemptive and (or) non-preemptive. We believe that the model may serve as a bridge between scheduling theory and automata-theoretic approaches to system modelling and analysis.

    Our main result is that the schedulability checking problem for this model is decidable. To our knowledge, this is the first general decidability result on dense-time models for real time scheduling without assuming that preemptions occur only at integer time points. The proof is based on a decidable class of updatable automata: timed automata with subtraction in which clocks may be updated by subtractions within a bounded zone. As the second contribution, we show that for fixed priority scheduling strategy, the schedulability checking problem can be solved by reachability analysis on standard timed automata using only two extra clocks in addition to the clocks used in the original model to describe task arrival times. The analysis can be done in a similar manner to response time analysis in classic Rate-Monotonic Scheduling. We believe that this is the optimal solution to the problem. The third contribution is an extension of the above results to deal with precedence and resource constraints. We present an operational semantics for the model, and show that the related schedulability analysis problem can be solved efficiently using the same techniques. Finaly, to demonstrate the applicability of the framework, we have modelled, analysed, and synthesised the control software for a production cell. The presented results have been implemented in the Times tool for automated schedulability analysis and code synthesis.

  • 41.
    Finne, Niclas
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Towards adaptive sensor networks2011Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    Wireless sensor networks consist of many small embedded devices that are equipped with sensors and a wireless communication unit. These devices, or sensor nodes, are typically low cost, resource constrained and battery-powered. Sensor network applications include environmental monitoring, industrial condition monitoring, building surveillance, and intelligent homes.

    Sensor network applications today are often developed either using standard software components which enables simpler development but leads to far from optimal performance, or software customized for the specific application which complicates development, software updates, and software reuse.

    We suggest that logic is separated from configuration and other information, for instance, network statistics and estimated power consumption. Software components publish their configuration and other information using a generalized programming abstraction. Configuration policies are separate modules that react on changes and reconfigure the sensor node as needed. These configuration policies are responsible for coordinating the configuration between the components and optimize the sensor network towards the application objectives.

    One of our contributions is that we demonstrate the need for self-monitoring and self-configuration based on experiences from two deployed sensor networks. Our main contribution is that we devise a configuration architecture that solves the problem of cross-layer optimization for sensor network applications without tight coupling between components, thus enabling standard and easily replaceable components to be used. The configuration architecture makes it possible to reach the same level of performance as specialized cross-layer optimizations but without adding application-specific knowledge to the components.

  • 42.
    Forslin, Sara
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
    Automatiska GUI-test: En teoretisk och praktisk studie för hållbarare test2010Independent thesis Advanced level (professional degree), 20 credits / 30 HE creditsStudent thesis
    Abstract [en]

    To automate software testing is an investment, and that makes it important to have good knowledge about automation before an implementation is made. In this master thesis a study about automated testing is carried out. The study also includes a closer look at the testing tool TestComplete. TestComplete is one out of many tools on the market that is developed for automated GUI testing and the goal is to get a picture of how well the tool can adjust to CC Systems own applications. Studies show that it is hard to write lasting test scripts. The automation must be implemented early in the development process and many protective measures have to be applied to the tests in order to protect  them. The report  also discusses a number of design requirements that is put on the tested application. These requirements are relatively easy to implement if they are known from the start of the development process. Two of the most important requirements are that the controls have to have specified names so the tests can use them and identify them and that the values that are important in the verification of the test have to be accessible and readable. CCSimTech is one of CC Systems own developed products and it is used in different hardware simulations. It is an important tool in manual testing at CC System today. Therefore it is important that also TestComplete can use it. To solve this, a library of functions adjusted for TestComplete has been created. The functions are developed so that they can be called directly from the test scripts in TestComplete in a user-friendly way. If the tests are able to call and use CCSimTech that will mean a way to further control the applications and make the test even more powerful

  • 43.
    Furunäs Åkesson, Johan
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Interprocess communication utilising special purpose hardware2001Licentiate thesis, comprehensive summary (Other academic)
    Abstract [en]

    Real-Time Systems are computer systems with constraints on the timing of actions. To ease the development and maintenance of application software, Real-time Systems often make use of a Real-Time Operating System (RTOS). Its main task is scheduling of application processes (tasks). Other functions can be interprocess communication, interrupt handling, memory management etc.

    Sometimes it is hard (or even impossible) to meet the time constraints specified for a real-time system, resulting in an incorrectly functioning application. A possible remedy is to redesign the system by upgrading the processor and/or remove functionality, etc. An alternative solution could be the use of a special purpose hardware accelerated RTOS. The aim of such an accelerator is to speedup RTOS functions that impose big overhead i.e. to reduce the kernel overhead by offloading the application processor. Accordingly, the processor gets more time for executing application software, and hopefully the time constraints can be met. The main drawback is the cost of extra hardware.

    This thesis presents results from implementing RTOS functions in hardware, especially interprocess communication (IPC) functions. The types of systems considered are uniprocessor and shared memory multiprocessor real-time systems.

    IPC is used in systems with co-operating processes. The operating systems on the market support a large variation of IPC mechanisms. We will here present and evaluate three different IPC implementations. The first is an extended message queue mechanism that is used in commercial robot control applications. The second is the signal mechanism in OSE, a commercial RTOS predominantly used in telecommunication control applications, and the third is the semaphore and message queue mechanisms supported by the leading commercial RTOS VxWorks. All the implementations are based on a pre-emptive priority-based hardware real-time kernel accelerator.

    We show that it is not optimal, practical or desirable to implement every kernel function into hardware, regarding systems in the scope of this thesis. However, an accelerator allows new functionality to be implemented. We illustrate this by implementing a message queue mechanism that supports priority inheritance for message arrival in hardware, which is too expensive to implement in software. Also, we show that substantial speedups are possible, and that a crucial mechanism in achieving speedup is the accelerator-processor interconnect. We further note that application speedups are possible, even in cases with an IPC-mechanism slow-down. The main reasons for this is that the accelerator can off-load the processor by handling the RTOS timing mechanism (clock-ticks), reducing the RTOS code to be executed on the processor, and handling interrupts.

  • 44.
    Furuskog, Martin
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
    Wemyss, Stuart
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
    Cross-platform development of smartphone applications: An evaluation of React Native2016Independent thesis Advanced level (professional degree), 20 credits / 30 HE creditsStudent thesis
    Abstract [en]

    During the last ten years the market for smartphones has grown drastically. Because of the current state of the market with different operating systems many smartphone applications need to be developed for several platforms. With this thesis, the goal was ultimately to contribute to the understanding of cross-platform development as a way of developing smartphone applications. React Native has been evaluated as a framework with which development is done for both Android and iOS using the same code. To study React Native as a framework, a smartphone application for Android and iOS was developed at an Uppsala based IT-company with expertise in web services, smartphone applications, and online gaming. Furthermore, performance tests and user tests were conducted in which React Native was compared to native applications and applications developed using Xamarin (similar cross-platform development framework owned by Microsoft). It was evident that using the same code for both Android and iOS was time saving. However, the performance tests results showed that applications developed with React Native did not perform as well as the native and Xamarin versions. Leading to the conclusion that choice of framework when developing cross-platform applications need to take into consideration performance, development time, and programming language preference.

  • 45.
    Gold, Richard
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    An Indirection Architecture for the Internet2005Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    We present an indirection architecture for the Internet called SelNet. SelNet provides a uniform indirection mechanism for controlling the route that packets take through the network and which functions are invoked to process these packets. In the current Internet, at least for the majority of users, there is only one way that a packet can go and that is to the default route. Whilst this is sufficient for many applications, numerous applications have arisen which require alternative routes or processing to be present not only at the application-layer of the protocol stack, but at the network-layer itself. Solutions to such scenarios attempt to place an indirection point between the communicating end-systems either with a middlebox (such as a proxy) or by altering one or more of the Internet's naming systems. However these approaches lead to an application-specific network, which is against the Internet's design goals. We argue for a uniform approach to indirection instead of building multiple, partially overlapping structures as is the current trend. SelNet differs from existing indirection approaches in that it is function-orientated, rather than node-orientated and that it provides an explicit, controllable resolution mechanism for resolving host names and services. The motivation behind our approach is to create efficient indirection structures for supporting new applications which have indirection requirements. We present a detailed design and specification of SelNet. We then go on to describe implementation work with the LUNAR ad-hoc routing protocol and the Janus middleware for accessing sensor networks systems. The purpose of this implementation work is to demonstrate the feasibility of SelNet and its ability to reach its goals.

  • 46.
    Grinchtein, Olga
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Learning of Timed Systems2008Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    Regular inference is a research direction in machine learning. The goal of regular inference is to construct a representation of a regular language in the form of deterministic finite automaton (DFA) based on the set of positive and negative examples. DFAs take strings of symbols (words) as input, and produce a binary classification as output, indicating whether the word belongs to the language or not. There are two types of learning algorithms for DFAs: passive and active learning algorithms. In passive learning, the set of positive and negative examples is given and not chosen by inference algorithm. In contrast, in active learning, the learning algorithm chooses examples from which a model is constructed.

    Active learning was introduced in 1987 by Dana Angluin. She presented the L* algorithm for learning DFAs by asking membership and equivalence queries to a teacher who knows the regular language accepted by DFA to be learned. A membership query checks whether a word belongs to the language or not. An equivalence query checks whether a hypothesized model is equivalent to the DFA to be learned.The L* algorithm has been found to be useful in different areas, including black box checking, compositional verification and integration testing. There are also other algorithms similar to L* for regular inference. However, the learning of timed systems has not been studied before. This thesis presents algorithms for learning timed systems in an active learning framework.

    As a model of timed system we choose event-recording automata (ERAs), a determinizable subclass of the widely used timed automata. The advantages of ERA in comparison with timed automata, is that it is known priori the set of clocks of an ERA and when clocks are reset. The contribution of this thesis is four algorithms for learning deterministic event-recording automaton (DERA). Two algorithms learn a subclass of DERA, called event-deterministic ERA (EDERA) and two algorithms learn general DERA.

    The problem with DERAs that they do not have canonical form. Therefore we focus on subclass of DERAs that have canonical representation, EDERA, and apply the L* algorithm to learn EDERAs. The L* algorithm in timed setting requires a procedure that learns clock guards of DERAs. This approach constructs EDERAs which are exponentially bigger than automaton to be learned. Another procedure can be used to lean smaller EDERAs, but it requires to solve NP-hard problem.

    We also use the L* algorithm to learn general DERA. One drawback of this approach that inferred DERAs have a form of region graph and there is blow-up in the number of transitions. Therefore we introduce an algorithm for learning DERA which uses a new data structure for organising results of queries, called a timed decision tree, and avoids region graph construction. Theoretically this algorithm can construct bigger DERA than the L* algorithm, but in the average case we expect better performance.

  • 47.
    Guan, Nan
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    New Techniques for Building Timing-Predictable Embedded Systems2013Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    Embedded systems are becoming ubiquitous in our daily life. Due to close interaction with physical world, embedded systems are typically subject to timing constraints. At design time, it must be ensured that the run-time behaviors of such systems satisfy the pre-specified timing constraints under any circumstance. In this thesis, we develop techniques to address the timing analysis problems brought by the increasing complexity of underlying hardware and software on different levels of abstraction in embedded systems design.

    On the program level, we develop quantitative analysis techniques to predict the cache hit/miss behaviors for tight WCET estimation, and study two commonly used replacement policies, MRU and FIFO, which cannot be analyzed adequately using the state-of-the-art qualitative cache analysis method. Our quantitative approach greatly improves the precision of WCET estimation and discloses interesting predictability properties of these replacement policies, which are concealed in the qualitative analysis framework.

    On the component level, we address the challenges raised by multi-core computing. Several fundamental problems in multiprocessor scheduling are investigated. In global scheduling, we propose an analysis method to rule out a great part of impossible system behaviors for better analysis precision, and establish conditions to guarantee the bounded responsiveness of computing tasks. In partitioned scheduling, we close a long standing open problem to generalize the famous Liu and Layland's utilization bound in uniprocessor real-time scheduling to multiprocessor systems. We also propose to use cache partitioning for multi-core systems to avoid contentions on shared caches, and solve the underlying schedulability analysis problem.

    On the system level, we present techniques to improve the Real-Time Calculus (RTC) analysis framework in both efficiency and precision. First, we have developed Finitary Real-Time Calculus to solve the scalability problem of the original RTC due to period explosion. The key idea is to only maintain and operate on a limited prefix of each curve that is relevant to the final results during the whole analysis procedure. We further improve the analysis precision of EDF components in RTC, by precisely bounding the response time of each computation request.

  • 48.
    Gustafsson, Jan
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Analyzing execution-time of object-oriented programs using abstract interpretation2000Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    As a result of the industrial deployment of real-time systems, there is an increasing demandfor methods to perform safe and tight calculation of the worst case execution time (WCET) ofprograms. The WCET is a necessary prerequisite for guaranteeing correct timing behaviour ofreal-time systems. WCET calculation means to find the path, often among a huge number ofpaths, that takes the longest time to execute. The calculation is based on path information for theprogram, such as the maximum number of iterations in loops and identification of paths that arenever executed. In most existing WCET analysis methods, this information is given as manual annotations by the programmer.

    In this thesis we present a method which automatically calculates path information for object-oriented real-time programs by static analysis. Thus, the method can be used in automating the WCET analysis, thereby relieving the programmer from the tedious and error-prone manualannotation work.

    The method, which is based on abstract interpretation, generates safe but not necessarily exactpath information. A trade-off between quality and calculation cost has to be made, since findingthe exact information is a complex, often intractable problem for non-trivial programs.

    We show how the general abstract interpretation theory can be used, in a structured way, toapproximate the semantics of an imperative or object-oriented programming language.

    We have chosen to analyze RealTimeTalk (RTT), an object-oriented language based on Smalltalk,and have developed a prototype tool which implements our analysis for a subset of the language,We show that the tool is capable of analyzing programs with a complexity which would makemanual annotation of the program all but trivial.

  • 49.
    Haziza, Frédéric
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
    Few is Just Enough!: Small Model Theorem for Parameterized Verification and Shape Analysis2015Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    This doctoral thesis considers the automatic verification of parameterized systems, i.e. systems with an arbitrary number of communicating components, such as mutual exclusion protocols, cache coherence protocols or heap manipulating programs. The components may be organized in various topologies such as words, multisets, rings, or trees.

    The task is to show correctness regardless of the size of the system and we consider two methods to prove safety:(i) a backward reachability analysis, using the well-quasi ordered framework and monotonic abstraction, and (ii) a forward analysis which only needs to inspect a small number of components in order to show correctness of the whole system. The latter relies on an abstraction function that views the system from the perspective of a fixed number of components. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state-space need not continue.

    Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable property. It has been, for example, successfully applied to verify a fine-grained model of Szymanski's mutual exclusion protocol. Finally, we applied the methods to solve the complex problem of verifying highly concurrent data-structures, in a challenging setting: We do not a priori bound the number of threads, the size of the data-structure, the domain of the data to store nor do we require the presence of a garbage collector. We successfully verified the concurrent Treiber's stack and Michael & Scott's queue, in the aforementioned setting.

    To the best of our knowledge, these verification problems have been considered challenging in the parameterized verification community and could not be carried out automatically by other existing methods.

  • 50.
    Henriksson, Jonas
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
    Visual Stimulus Development: FlyFly - A user friendly interface for MatLaba nd the Psychophysics toolbox2010Independent thesis Advanced level (professional degree), 20 credits / 30 HE creditsStudent thesis
    Abstract [en]

    Flies use visual cues for a variety of tasks, such as maneuvering through the environment and finding potential mates. Hoverflies, in particular, have very developed eyes and use them to be able to hover mid air and perform fast, elegant movements. The Motion Vision Group, located at the Department of Neuroscience at BMC, Uppsala, studies the motion vision system of the hoverfly brain, using electrophysiology. Experiments are performed by displaying visual stimuli on a screen in front of an immobilized fly, while recording the response from a single neuron with a thin electrode.Until now, the Motion Vision group has been using the open source program VisionEgg to generate the stimuli. VisionEgg is able to display stimuli at high frame rate and has a large set of useful features such as perspective distortion. It also has a lot of drawbacks that makes it desirable to acquire new software. The main drawbacks include it being hard to learn, use and modify, as well as being unable to generate the stimuli needed for some key experiments.This master´s thesis describes the development of software more suited to the lab´s needs. This software should be able to generate some of the stimuli that were impossible to do at the moment, as well as being easy to expand and add upon. The frame rate of the displayed stimuli has to be both high and stable in order to perform high precision experiments.The resulting program is called FlyFly and has been developed iteratively in close cooperation with its end users, ensuring a user friendly end product capable of meeting the lab´s needs. FlyFly is implemented using MatLab and the Psychophysics toolbox with the graphical user interface (GUI) designed with the Guide editor. The GUI is decoupled from the functions drawing the stimuli, making it easy to improve or remove parts altogether. FlyFly is intuitive to use and allows anyone to quickly get started. It allows easy manipulation of series of trials, and supports drawing of multiple objects simultaneously. With the current machine set-up, it displays stimuli at 160 frames per second with few or no dropped frames.FlyFly is currently being used in the lab and will be so for the foreseeable future.

123 1 - 50 of 134
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf