uu.seUppsala University Publications
Change search
Refine search result
123 1 - 50 of 138
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • 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. Adams, Liz
    et al.
    Daniels, Mats
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
    Goold, Annegret
    Hazzan, Orit
    Lynch, Kathy
    Newman, Ian
    Challenges in teaching capstone courses2003In: ACM SIGCSE Bulletin, Vol. 35, no 3, p. 219-220Article in journal (Refereed)
    Abstract [en]

    Many of us run capstone project courses and do so in different ways. The members of this panel come from different countries, belong to different types of institutions, teach in different computing disciplines and the capstone projects they run also vary considerably. Yet, there is a strong sense of consensus about what a capstone project is and how valuable it is as a learning experience for students.The panel discussion will serve as an inspiration to develop new, and change old capstone project courses. The main aim is to discuss why, or why not, different approaches work in a capstone project. What are the learning objectives behind the approach? What are the problems? What are the benefits? How is assessment managed? What resources, tools and techniques are used to administer and manage the projects?Concrete examples of how capstone projects are run at the six institutions represented by the panellists will be given, and issues such as framework, methodologies, project examples and technologies used in the process of producing projects will be addressed.

  • 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.

    List of papers
    1. Theorem proving with bounded rigid E-unification
    Open this publication in new window or tab >>Theorem proving with bounded rigid E-unification
    2015 (English)In: Automated Deduction – CADE-25, Springer, 2015, p. 572-587Conference paper, Published paper (Refereed)
    Place, publisher, year, edition, pages
    Springer, 2015
    Series
    Lecture Notes in Computer Science, ISSN 0302-9743 ; 9195
    National Category
    Computer Sciences
    Identifiers
    urn:nbn:se:uu:diva-268734 (URN)10.1007/978-3-319-21401-6_39 (DOI)000363947500039 ()978-3-319-21400-9 (ISBN)
    Conference
    25th International Conference on Automated Deduction; August 1–7, 2015, Berlin, Germany
    Funder
    Swedish Research Council, 2014-5484
    Available from: 2015-07-25 Created: 2015-12-09 Last updated: 2018-01-10Bibliographically approved
    2. Efficient algorithms for bounded rigid E-unification
    Open this publication in new window or tab >>Efficient algorithms for bounded rigid E-unification
    2015 (English)In: Automated Reasoning with Analytic Tableaux and Related Methods, Springer, 2015, p. 70-85Conference paper, Published paper (Refereed)
    Place, publisher, year, edition, pages
    Springer, 2015
    Series
    Lecture Notes in Computer Science, ISSN 0302-9743 ; 9323
    National Category
    Computer Sciences
    Identifiers
    urn:nbn:se:uu:diva-268735 (URN)10.1007/978-3-319-24312-2_6 (DOI)000366125200009 ()978-3-319-24311-5 (ISBN)
    Conference
    TABLEAUX 2015, September 21–24, Wroclaw, Poland
    Funder
    Swedish Research Council, 2014-5484
    Available from: 2015-11-08 Created: 2015-12-09 Last updated: 2018-01-10Bibliographically approved
    3. Algebraic polynomial-based synthesis for abstract Boolean network analysis
    Open this publication in new window or tab >>Algebraic polynomial-based synthesis for abstract Boolean network analysis
    2016 (English)In: Satisfiability Modulo Theories: SMT 2016, RWTH Aachen University , 2016, p. 41-50Conference paper, Published paper (Refereed)
    Place, publisher, year, edition, pages
    RWTH Aachen University, 2016
    Series
    CEUR Workshop Proceedings, ISSN 1613-0073 ; 1617
    National Category
    Computer Sciences
    Identifiers
    urn:nbn:se:uu:diva-311587 (URN)
    Conference
    14th International Workshop on Satisfiability Modulo Theories
    Available from: 2016-07-02 Created: 2016-12-29 Last updated: 2018-01-13Bibliographically approved
  • 4.
    Backeman, Peter
    et al.
    Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
    Rümmer, Philipp
    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.
    Zeljic, Aleksandar
    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.
    Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction2018In: Formal Methods inComputer-Aided Design / [ed] Nikolaj Bjørner, Arie Gurfinkel, 2018, Vol. 18, p. 50-59Conference paper (Refereed)
    Abstract [en]

    The inference of program invariants over machine arithmetic, commonly called bit-vector arithmetic, is an important problem in verification. Techniques that have been successful for unbounded arithmetic, in particular Craig interpolation, have turned out to be difficult to generalise to machine arithmetic: existing bit-vector interpolation approaches are based either on eager translation from bit-vectors to unbounded arithmetic, resulting in complicated constraints that are hard to solve and interpolate, or on bit-blasting to propositional logic, in the process losing all arithmetic structure. We present a new approach to bitvector interpolation, as well as bit-vector quantifier elimination (QE), that works by lazy translation of bit-vector constraints to unbounded arithmetic. Laziness enables us to fully utilise the information available during proof search (implied by decisions and propagation) in the encoding, and this way produce constraints that can be handled relatively easily by existing interpolation and QE procedures for Presburger arithmetic. The lazy encoding is complemented with a set of native proof rules for bit-vector equations and non-linear (polynomial) constraints, this way minimising the number of cases a solver has to consider

  • 5.
    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.

  • 6.
    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.

  • 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.
    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.

  • 8.
    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.

  • 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.
    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.

    List of papers
    1. SIP: Performance Tuning through Source Code Interdependence
    Open this publication in new window or tab >>SIP: Performance Tuning through Source Code Interdependence
    2002 In: Proceedings of the 8th International Euro-Par ConferenceArticle in journal (Refereed) Published
    Identifiers
    urn:nbn:se:uu:diva-93582 (URN)
    Available from: 2005-10-19 Created: 2005-10-19Bibliographically approved
    2. StatCache: A Probabilistic Approach to Efficient and Accurate Data Locality Analysis
    Open this publication in new window or tab >>StatCache: A Probabilistic Approach to Efficient and Accurate Data Locality Analysis
    2004 In: Proceedings of the 2004 IEEE International Symposium on Performance Analysis of Systems and SoftwareArticle in journal (Refereed) Published
    Identifiers
    urn:nbn:se:uu:diva-93583 (URN)
    Available from: 2005-10-19 Created: 2005-10-19Bibliographically approved
    3. Fast Data-Locality Profiling of Native Execution
    Open this publication in new window or tab >>Fast Data-Locality Profiling of Native Execution
    2005 (English)In: ACM SIGMETRICS Performance Evaluation Review, ISSN 0163-5999, Vol. 33, no 1, p. 169-180Article in journal (Refereed) Published
    National Category
    Computer Sciences
    Identifiers
    urn:nbn:se:uu:diva-93584 (URN)10.1145/1071690.1064232 (DOI)
    Available from: 2005-10-19 Created: 2005-10-19 Last updated: 2018-01-13Bibliographically approved
    4. A Statistical Multiprocessor Cache Model
    Open this publication in new window or tab >>A Statistical Multiprocessor Cache Model
    2006 (English)In: Proc. International Symposium on Performance Analysis of Systems and Software: ISPASS 2006, Piscataway, NJ: IEEE , 2006, p. 89-99Conference paper, Published paper (Refereed)
    Place, publisher, year, edition, pages
    Piscataway, NJ: IEEE, 2006
    National Category
    Computer Sciences
    Identifiers
    urn:nbn:se:uu:diva-93585 (URN)10.1109/ISPASS.2006.1620793 (DOI)1-4244-0186-0 (ISBN)
    Available from: 2005-10-19 Created: 2005-10-19 Last updated: 2018-01-13Bibliographically approved
  • 10.
    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.

  • 11.
    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.

  • 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.
    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.

  • 13.
    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.

    List of papers
    1. How do students understand network protocols?: A phenomenographic study
    Open this publication in new window or tab >>How do students understand network protocols?: A phenomenographic study
    2002 (English)Report (Other academic)
    Series
    Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2002-006
    National Category
    Computer Sciences Educational Sciences
    Identifiers
    urn:nbn:se:uu:diva-44859 (URN)
    Available from: 2008-11-26 Created: 2008-11-26 Last updated: 2018-01-11
    2. On context in phenomenographic research on understanding heat and temperate
    Open this publication in new window or tab >>On context in phenomenographic research on understanding heat and temperate
    2002 (English)In: EARLI, Bi-annual Symposium, Fribourg, Switzerland, 2002Conference paper, Published paper (Refereed)
    Abstract [en]

    Starting from an empirical study of lay adults' understanding of heatand temperature, we distinguish between different meanings of "context" inphenomenographic research. To confuse the variation in ways of experiencingthe context(s) of the study with the variation in ways of experiencing thephenomenon of study is to risk losing fundamental insights. We discuss contextas experienced and as interwoven with the experience of the phenomenon, andanalyse its significance in two dimensions: (1) the stage of the research project:formulating the question, collecting data, analysing data and deploying results;and (2) "who is experiencing" the context: the individual, the collective, or theresearcher. The arguments are illustrated from the empirical study.

    National Category
    Computer Sciences Educational Sciences
    Identifiers
    urn:nbn:se:uu:diva-18488 (URN)
    Conference
    EARLI, Bi-annual Symposium, Fribourg, Switzerland
    Available from: 2008-11-26 Created: 2008-11-26 Last updated: 2018-01-12
  • 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.
    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.

  • 15.
    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.

    List of papers
    1. Haggle Testbed: a Testbed for Opportunistic Networks
    Open this publication in new window or tab >>Haggle Testbed: a Testbed for Opportunistic Networks
    2011 (English)In: In Proceedings of the 7th Swedish National Computer Networking Workshop, 2011Conference paper, Published paper (Refereed)
    Identifiers
    urn:nbn:se:uu:diva-155530 (URN)
    Projects
    Haggle
    Available from: 2011-06-23 Created: 2011-06-23 Last updated: 2014-06-30
    2. Congestion Avoidance in a Data-Centric Opportunistic Network
    Open this publication in new window or tab >>Congestion Avoidance in a Data-Centric Opportunistic Network
    2011 (English)In: Proceedings of the 2011 ACM SIGCOMM Workshop on Information-Centric Networking (ICN-2011), 2011Conference paper, Published paper (Refereed)
    Identifiers
    urn:nbn:se:uu:diva-155528 (URN)
    Projects
    ResumeNet
    Available from: 2011-06-23 Created: 2011-06-23 Last updated: 2014-06-30
    3. Making the Most of Your Contacts: Transfer Ordering in Data-Centric Opportunistic Networks
    Open this publication in new window or tab >>Making the Most of Your Contacts: Transfer Ordering in Data-Centric Opportunistic Networks
    Show others...
    2012 (English)In: Proceedings of the 2012 ACM MobiOpp Workshop on Mobile Opportunistic Networks, Zürich: ACM Press, 2012Conference paper, Published paper (Refereed)
    Abstract [en]

    Opportunistic networks use unpredictable and time-limited con- tacts to disseminate data. Therefore, it is important that protocols transfer useful data when contacts do occur. Specifically, in a data- centric network, nodes benefit from receiving data relevant to their interests. To this end, we study five strategies to select and order the data to be exchanged during a limited contact, and measure their ability to promptly and efficiently deliver highly relevant data.

    Our trace-driven experiments on an emulation testbed suggest that nodes benefit in the short-term from ordering data transfers to satisfy local interests. However, this can lead to suboptimal longterm system performance. Restricting sharing based on matching nodes’ interests can lead to segregation of the network, and limit useful dissemination of data. A non-local understanding of other nodes’ interests is necessary to effectively move data across the network. If ordering of transfers for data relevance is not explicitly considered performance is comparable to random, which limits the delivery of individually relevant data. 

    Place, publisher, year, edition, pages
    Zürich: ACM Press, 2012
    National Category
    Communication Systems
    Identifiers
    urn:nbn:se:uu:diva-171587 (URN)
    Conference
    ACM MobiOpp
    Projects
    ResumeNet
    Available from: 2012-03-22 Created: 2012-03-22 Last updated: 2014-06-30
    4. Resilience and Opportunistic Forwarding: Beyond Average Value Analysis
    Open this publication in new window or tab >>Resilience and Opportunistic Forwarding: Beyond Average Value Analysis
    Show others...
    2014 (English)In: Computer Communications, ISSN 0140-3664, E-ISSN 1873-703X, Vol. 48, no SI, p. 111-120Article in journal (Refereed) Published
    Abstract [en]

    Opportunistic networks are systems with highly distributed operation, relying on the altruistic cooperation of highly heterogeneous, and not always software and hardware-compatible, user nodes. Moreover, the absence of central coordination and control makes them vulnerable to malicious attacks. In this paper, we study the resilience of popular forwarding protocols to a representative set of challenges to their normal operation. These include jamming locally disturbing message transfer between nodes, hardware/software failures and incompatibility among nodes rendering contact opportunities useless, and free-riding phenomena. We first formulate and promote the metric envelope concept as a tool for assessing the resilience of opportunistic forwarding schemes. Metric envelopes depart from the standard practice of average value analysis and explicitly account for the differentiated challenge impact due to node heterogeneity (device capabilities, mobility) and attackers’ intelligence. We then propose heuristics to generate worst- and best-case challenge realization scenarios and approximate the lower and upper bounds of the metric envelopes. Finally, we demonstrate the methodology in assessing the resilience of three popular forwarding protocols in the presence of the three challenges, and under a comprehensive range of mobility patterns. The metric envelope approach provides better insights into the level of protection path diversity and message replication provide against different challenges, and enables more informed choices in opportunistic forwarding when network resilience becomes important.

    National Category
    Communication Systems
    Identifiers
    urn:nbn:se:uu:diva-222822 (URN)10.1016/j.comcom.2014.04.004 (DOI)000337883200010 ()
    Projects
    ResumeNet, WISENET
    Funder
    EU, FP7, Seventh Framework Programme, FP7-224619
    Note

    Special Issue

    Available from: 2014-04-17 Created: 2014-04-14 Last updated: 2017-12-05Bibliographically approved
  • 16.
    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.

  • 17.
    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.

    List of papers
    1. Model Checking
    Open this publication in new window or tab >>Model Checking
    2005 (English)In: Model-Based Testing of Reactive Systems: Advanced Lectures, Berlin / Heidelberg: Springer , 2005, p. 557-603Chapter in book (Other academic)
    Place, publisher, year, edition, pages
    Berlin / Heidelberg: Springer, 2005
    Series
    Lecture Notes in Computer Sciences: Programming and Software Engineering, ISSN 0302-9743 ; 3472
    National Category
    Computer and Information Sciences
    Identifiers
    urn:nbn:se:uu:diva-98082 (URN)978-3-540-26278-7 (ISBN)
    Available from: 2009-02-06 Created: 2009-02-06 Last updated: 2018-01-13Bibliographically approved
    2. Insights to Angluin's Learning
    Open this publication in new window or tab >>Insights to Angluin's Learning
    2005 (English)In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 118, p. 3-18Article in journal (Refereed) Published
    Abstract [en]

    Among other domains, learning finite-state machines is important for obtaining a model of a system under development, so that powerful formal methods such as model checking can be applied.

    A prominent algorithm for learning such devices was developed by Angluin. We have implemented this algorithm in a straightforward way to gain further insights to practical applicability. Furthermore, we have analyzed its performance on randomly generated as well as real-world examples. Our experiments focus on the impact of the alphabet size and the number of states on the needed number of membership queries. Additionally, we have implemented and analyzed an optimized version for learning prefix-closed regular languages. Memory consumption is one major obstacle when we attempted to learn large examples.

    We see that prefix-closed languages are relatively hard to learn compared to arbitrary regular languages. The optimization, however, shows positive results.

    Keywords
    deterministic finite-state automata, learning algorithm, regular languages, prefix-closed regular languages
    National Category
    Computer and Information Sciences
    Identifiers
    urn:nbn:se:uu:diva-98083 (URN)10.1016/j.entcs.2004.12.015 (DOI)
    Available from: 2009-02-06 Created: 2009-02-06 Last updated: 2018-01-13Bibliographically approved
    3. Regular Inference for State Machines with Parameters
    Open this publication in new window or tab >>Regular Inference for State Machines with Parameters
    2006 (English)In: Fundamental approaches to software engineering: ( 9th international conference, FASE 2006, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006 ), Berlin: Springer , 2006, p. 107-121Chapter in book (Other academic)
    Abstract [en]

    Techniques for inferring a regular language, in the form of a finite automaton, from a sufficiently large sample of accepted and nonaccepted input words, have been employed to construct models of software and hardware systems, for use, e.g., in test case generation. We intend to adapt these techniques to construct state machine models of entities of communication protocols. The alphabet of such state machines can be very large, since a symbol typically consists of a protocol data unit type with a number of parameters, each of which can assume many values. In typical algorithms for regular inference, the number of needed input words grows with the size of the alphabet and the size of the minimal DFA accepting the language. We therefore modify such an algorithm (Angluin's algorithm) so that its complexity grows not with the size of the alphabet, but only with the size of a certain symbolic representation of the DFA. The main new idea is to infer, for each state, a partitioning of input symbols into equivalence classes, under the hypothesis that all input symbols in an equivalence class have the same effect on the state machine. Whenever such a hypothesis is disproved, equivalence classes are refined. We show that our modification retains the good properties of Angluin's original algorithm, but that its complexity grows with the size of our symbolic DFA representation rather than with the size of the alphabet. We have implemented the algorithm; experiments on synthesized examples are consistent with these complexity results.

    Place, publisher, year, edition, pages
    Berlin: Springer, 2006
    Series
    Lecture notes in computer science, ISSN 0302-9743
    Keywords
    Test generation, Algorithm complexity, Modeling, Equivalence classes, Deterministic automaton, Data type, Transmission protocol, Finite automaton, Regular language, Inference, Software development
    National Category
    Computer and Information Sciences
    Identifiers
    urn:nbn:se:uu:diva-98084 (URN)3-540-33093-3 (ISBN)
    Available from: 2009-02-06 Created: 2009-02-06 Last updated: 2018-01-13Bibliographically approved
    4. Regular Inference for State Machines Using Domains with Equality Tests
    Open this publication in new window or tab >>Regular Inference for State Machines Using Domains with Equality Tests
    2008 (English)In: Fundamental Approaches to Software Engineering / [ed] Fiadeiro JL; Inverardi P, Berlin: Springer-Verlag , 2008, p. 317-331Conference paper, Published paper (Refereed)
    Abstract [en]

    Existing algorithms for regular inference (aka automata learning) allows to infer a finite state machine by observing the output that the machine produces in response to a selected sequence of input strings. We generalize regular inference techniques to infer a class of state machines with an infinite state space. We consider Mealy machines extended with state variables that can assume values from a potentially unbounded domain. These values can be passed as parameters in input and output symbols, and can be used in tests for equality between state variables and/or message parameters. This is to our knowledge the first extension of regular inference to infinite-state systems. We intend to use these techniques to generate models of communication protocols from observations of their input-output behavior. Such protocols often have parameters that represent node adresses, connection identifiers, etc. that have a large domain, and on which test for equality is the only meaningful operation. Our extension consists of two phases. In the first phase we apply an existing inference technique for finite-state Mealy machines to generate a model for the case that the values are taken from a small data domain. In the second phase we transform this finite-state Mealy machine into an infinite-state Mealy machine by folding it into a compact symbolic form.

    Place, publisher, year, edition, pages
    Berlin: Springer-Verlag, 2008
    Series
    Lecture Notes in Computer Science ; 4961
    National Category
    Computer Sciences
    Identifiers
    urn:nbn:se:uu:diva-98085 (URN)10.1007/978-3-540-78743-3_24 (DOI)000254603000024 ()978-3-540-78742-6 (ISBN)
    Conference
    11th International Conference on Fundamental Approaches to Software Engineering Budapest, HUNGARY, MAR 29-APR 06, 2008
    Available from: 2009-02-06 Created: 2009-02-06 Last updated: 2018-01-13Bibliographically approved
    5. Regular Inference for Communication Protocol Entities
    Open this publication in new window or tab >>Regular Inference for Communication Protocol Entities
    2008 (English)Report (Other academic)
    Series
    Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2008-024
    Identifiers
    urn:nbn:se:uu:diva-98086 (URN)
    Available from: 2009-02-06 Created: 2009-02-06 Last updated: 2009-06-09Bibliographically approved
  • 18.
    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.

  • 19.
    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. 

  • 20.
    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.

    List of papers
    1. The impact of trace and adversary models on location privacy provided by K-anonymity
    Open this publication in new window or tab >>The impact of trace and adversary models on location privacy provided by K-anonymity
    2012 (English)In: Proc. 1st Workshop on Measurement, Privacy, and Mobility, New York: ACM Press, 2012, article id 6Conference paper, Published paper (Refereed)
    Place, publisher, year, edition, pages
    New York: ACM Press, 2012
    National Category
    Computer Sciences
    Research subject
    Computer Science with specialization in Computer Communication
    Identifiers
    urn:nbn:se:uu:diva-171581 (URN)10.1145/2181196.2181202 (DOI)978-1-4503-1163-2 (ISBN)
    Conference
    MPM 2012
    Projects
    ProFuNWISENET
    Available from: 2012-04-10 Created: 2012-03-22 Last updated: 2018-01-12Bibliographically approved
    2. Towards adaptive zero-knowledge protocols: A case study with Fiat–Shamir identification protocol
    Open this publication in new window or tab >>Towards adaptive zero-knowledge protocols: A case study with Fiat–Shamir identification protocol
    2013 (English)In: Proc. 9th Swedish National Computer Networking Workshop, 2013, p. 67-70Conference paper, Published paper (Refereed)
    Abstract [en]

    Interactive zero-knowledge protocols are used as identification protocols. The protocols are executed in rounds, with security being increased with every round. This allows for a trade-off between security and performance to adapt the protocol to the requirements of the scenario. We experimentally investigate the Fiat–Shamir identification protocol on machines and networks with different performance characteristics. We find that the delay of the protocol highly depends on network latency and upload bandwidth. Computation time becomes more visible, when the protocol transmits little amount of data via a low latency network. We also experience that the impact of the sizes of the variables on the delay of the protocol is less than the number of rounds', which are interior factors in the protocol.

    National Category
    Computer Sciences
    Research subject
    Computer Science with specialization in Computer Communication
    Identifiers
    urn:nbn:se:uu:diva-201070 (URN)
    Conference
    SNCNW 2013
    Projects
    WISENETProFuN
    Available from: 2013-06-05 Created: 2013-06-05 Last updated: 2018-01-11Bibliographically approved
    3. Modelling and analysing a WSN secure aggregation protocol: A comparison of languages and tool support
    Open this publication in new window or tab >>Modelling and analysing a WSN secure aggregation protocol: A comparison of languages and tool support
    2015 (English)Report (Other academic)
    Series
    Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2015-033
    National Category
    Computer Sciences Communication Systems
    Research subject
    Computer Science with specialization in Computer Communication
    Identifiers
    urn:nbn:se:uu:diva-268453 (URN)
    Projects
    ProFuN
    Funder
    Swedish Foundation for Strategic Research , RIT08-0065
    Available from: 2015-12-03 Created: 2015-12-04 Last updated: 2018-01-10Bibliographically approved
  • 21.
    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.

  • 22.
    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.

    List of papers
    1. Inferring Canonical Register Automata
    Open this publication in new window or tab >>Inferring Canonical Register Automata