Logo: to the web site of Uppsala University

uu.sePublikasjoner fra Uppsala universitet
Endre søk
Begrens søket
1234567 1 - 50 of 503
RefereraExporteraLink til resultatlisten
Permanent link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Treff pr side
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sortering
  • Standard (Relevans)
  • Forfatter A-Ø
  • Forfatter Ø-A
  • Tittel A-Ø
  • Tittel Ø-A
  • Type publikasjon A-Ø
  • Type publikasjon Ø-A
  • Eldste først
  • Nyeste først
  • Skapad (Eldste først)
  • Skapad (Nyeste først)
  • Senast uppdaterad (Eldste først)
  • Senast uppdaterad (Nyeste først)
  • Disputationsdatum (tidligste først)
  • Disputationsdatum (siste først)
  • Standard (Relevans)
  • Forfatter A-Ø
  • Forfatter Ø-A
  • Tittel A-Ø
  • Tittel Ø-A
  • Type publikasjon A-Ø
  • Type publikasjon Ø-A
  • Eldste først
  • Nyeste først
  • Skapad (Eldste først)
  • Skapad (Nyeste først)
  • Senast uppdaterad (Eldste først)
  • Senast uppdaterad (Nyeste først)
  • Disputationsdatum (tidligste først)
  • Disputationsdatum (siste først)
Merk
Maxantalet träffar du kan exportera från sökgränssnittet är 250. Vid större uttag använd dig av utsökningar.
  • 1. Aarts, Fides
    et al.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Uijen, Johan
    Vaandrager, Frits
    Generating models of infinite-state communication protocols using regular inference with abstraction2015Inngår i: Formal methods in system design, ISSN 0925-9856, E-ISSN 1572-8102, Vol. 46, nr 1, s. 1-41Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    In order to facilitate model-based verification and validation, effort is underway to develop techniques for generating models of communication system components from observations of their external behavior. Most previous such work has employed regular inference techniques which generate modest-size finite-state models. They typically suppress parameters of messages, although these have a significant impact on control flow in many communication protocols. We present a framework, which adapts regular inference to include data parameters in messages and states for generating components with large or infinite message alphabets. A main idea is to adapt the framework of predicate abstraction, successfully used in formal verification. Since we are in a black-box setting, the abstraction must be supplied externally, using information about how the component manages data parameters. We have implemented our techniques by connecting the LearnLib tool for regular inference with an implementation of session initiation protocol (SIP) in ns-2 and an implementation of transmission control protocol (TCP) in Windows 8, and generated models of SIP and TCP components.

  • 2.
    Abdulla, Parosh
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Aronis, Stavros
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Optimal dynamic partial order reduction2014Inngår i: Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York: ACM Press, 2014, s. 373-384Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Stateless model checking is a powerful technique for program verification, which however suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is Dynamic Partial Order Reduction (DPOR). We present a new DPOR algorithm, which is the first to be provably optimal in that it always explores the minimal number of executions. It is based on a novel class of sets, called source sets, which replace the role of persistent sets in previous algorithms. First, we show how to modify an existing DPOR algorithm to work with source sets, resulting in an efficient and simple to implement algorithm. Second, we extend this algorithm with a novel mechanism, called wakeup trees, that allows to achieve optimality. We have implemented both algorithms in a stateless model checking tool for Erlang programs. Experiments show that source sets significantly increase the performance and that wakeup trees incur only a small overhead in both time and space.

  • 3.
    Abdulla, Parosh
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Ngo, Tuan-Phong
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik.
    Optimal Stateless Model Checking under the Release-Acquire Semantics2018Inngår i: SPLASH OOPSLA 2018, Boston, Nov 4-9, 2018, ACM Digital Library, 2018Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We present a framework for efficient application of stateless model checking (SMC) to concurrent programs running under the Release-Acquire (RA) fragment of the C/C++11 memory model. Our approach is based on exploring the possible program orders, which define the order in which instructions of a thread are executed, and read-from relations, which define how reads obtain their values from writes. This is in contrast to previous approaches, which in addition explore the possible coherence orders, i.e., orderings between conflicting writes. Since unexpected test results such as program crashes or assertion violations depend only on the read-from relation, we avoid a potentially large source of redundancy. Our framework is based on a novel technique for determining whether a particular read-from relation is feasible under the RA semantics. We define an SMC algorithm which is provably optimal in the sense that it explores each program order and read-from relation exactly once. This optimality result is strictly stronger than previous analogous optimality results, which also take coherence order into account. We have implemented our framework in the tool Tracer. Experiments show that Tracer can be significantly faster than state-of-the-art tools that can handle the RA semantics.

  • 4.
    Abdulla, Parosh
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik.
    Ngo, Tuan-Phong
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Optimal Stateless Model Checking under the Release-Acquire Semantics2018Inngår i: Proceedings of the ACM on Programming Languages, E-ISSN 2475-1421, Vol. 2, nr OOPSLA, s. 1-29, artikkel-id 135Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present a framework for the efficient application of stateless model checking (SMC) to concurrent programs running under the Release-Acquire (RA) fragment of the C/C++11 memory model. Our approach is based on exploring the possible program orders, which define the order in which instructions of a thread are executed, and read-from relations, which specify how reads obtain their values from writes. This is in contrast to previous approaches, which also explore the possible coherence orders, i.e., orderings between conflicting writes. Since unexpected test results such as program crashes or assertion violations depend only on the read-from relation, we avoid a potentially significant source of redundancy. Our framework is based on a novel technique for determining whether a particular read-from relation is feasible under the RA semantics. We define an SMC algorithm which is provably optimal in the sense that it explores each program order and read-from relation exactly once. This optimality result is strictly stronger than previous analogous optimality results, which also take coherence order into account. We have implemented our framework in the tool Tracer. Experiments show that Tracer can be significantly faster than state-of-the-art tools that can handle the RA semantics.

    Fulltekst (pdf)
    FULLTEXT01
  • 5.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bouajjani, Ahmed
    IRIF Université Paris Diderot, Paris, France.
    Ngo, Tuan Phong
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Context-bounded analysis for POWER2017Inngår i: Tools and Algorithms for the Construction and Analysis of Systems: Part II, Springer, 2017, s. 56-74Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We propose an under-approximate reachability analysis algorithm for programs running under the POWER memory model, in the spirit of the work on context-bounded analysis initiated by Qadeer et al. in 2005 for detecting bugs in concurrent programs (supposed to be running under the classical SC model). To that end, we first introduce a new notion of context-bounding that is suitable for reasoning about computations under POWER, which generalizes the one defined by Atig et al. in 2011 for the TSO memory model. Then, we provide a polynomial size reduction of the context-bounded state reachability problem under POWER to the same problem under SC: Given an input concurrent program P, our method produces a concurrent program P' such that, for a fixed number of context switches, running P' under SC yields the same set of reachable states as running P under POWER. The generated program P' contains the same number of processes as P and operates on the same data domain. By leveraging the standard model checker CBMC, we have implemented a prototype tool and applied it on a set of benchmarks, showing the feasibility of our approach.

  • 6.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik.
    Bouajjani, Ahmed
    Ngo, Tuan Phong
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik.
    Replacing store buffers by load buffers in TSO2018Inngår i: Verification and Evaluation of Computer and Communication Systems, Springer, 2018, s. 22-28Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We consider the weak memory model of Total Store Ordering (TSO). In the classical definition of TSO, an unbounded buffer is inserted between each process and the shared memory. The buffers contains pending store operations of the processes. We introduce a new model where we replace the store buffers by load buffers. In contrast to the classical model, the buffers now contain load operations. We show that the models have equivalent behaviors in the sense that the processes reach identical sets of states when the input program is run under the two models.

  • 7.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bui, Phi Diep
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Counter-Example Guided Program Verification2016Inngår i: FM 2016: Formal Methods, Springer, 2016, s. 25-42Konferansepaper (Fagfellevurdert)
  • 8.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Chen, Yu-Fang
    Institute of Information Science, Academia Sinica .
    Holik, Lukas
    Brno University.
    Rezine, Ahmed
    Linköping University.
    Rümmer, Philipp
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    String Constraints for Verification2014Inngår i: Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Springer, 2014, s. 150-166Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We present a decision procedure for a logic that combines (i) word equations over string variables denoting words of arbitrary lengths, together with (ii) constraints on the length of words, and on (iii) the regular languages to which words belong. Decidability of this general logic is still open. Our procedure is sound for the general logic, and a decision procedure for a particularly rich fragment that restricts the form in which word equations are written. In contrast to many existing procedures, our method does not make assumptions about the maximum length of words. We have developed a prototypical implementation of our decision procedure, and integrated it into a CEGAR-based model checker for the analysis of programs encoded as Horn clauses. Our tool is able to automatically establish the correctness of several programs that are beyond the reach of existing methods.

  • 9.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Hofman, Piotr
    Mayr, Richard
    Kumar, K. Narayan
    Chennai Mathematical Institute, Chennai, India.
    Totzke, Patrick
    Infinite-state energy games2014Inngår i: Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, New York: ACM Press, 2014Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Energy games are a well-studied class of 2-player turn-based games on a finite graph where transitions are labeled with integer vectors which represent changes in a multidimensional resource (the energy). One player tries to keep the cumulative changes non-negative in every component while the other tries to frustrate this.

    We consider generalized energy games played on infinite game graphs induced by pushdown automata (modelling recursion) or their subclass of one-counter automata.

    Our main result is that energy games are decidable in the case where the game graph is induced by a one-counter automaton and the energy is one-dimensional. On the other hand, every further generalization is undecidable: Energy games on one-counter automata with a 2-dimensional energy are undecidable, and energy games on pushdown automata are undecidable even if the energy is one-dimensional. Furthermore, we show that energy games and simulation games are inter-reducible, and thus we additionally obtain several new (un)decidability results for the problem of checking simulation preorder between pushdown automata and vector addition systems.

  • 10.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Rezine, Othmane
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Verification of Directed Acyclic Ad Hoc Networks2013Inngår i: Formal Techniques for Distributed Systems: FORTE 2013, Springer Berlin/Heidelberg, 2013, s. 193-208Konferansepaper (Fagfellevurdert)
    Fulltekst (pdf)
    fulltext
  • 11.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Stenman, Jari
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Computing optimal reachability costs in priced dense-timed pushdown automata2014Inngår i: Language and Automata Theory and Applications: LATA 2014, Springer Berlin/Heidelberg, 2014, s. 62-75Konferansepaper (Fagfellevurdert)
  • 12.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Stenman, Jari
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Zenoness for Timed Pushdown Automata2014Inngår i: Proceedings 15th International Workshop on Verification of Infinite-State Systems, {INFINITY} 2013, Hanoi, Vietnam, 14th October 2013., 2014, s. -47Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Timed pushdown automata are pushdown automata extended with a finite set of real-valued clocks. Additionaly, each symbol in the stack is equipped with a value representing its age. The enabledness of a transition may depend on the values of the clocks and the age of the topmost symbol. Therefore, dense-timed pushdown automata subsume both pushdown automata and timed automata. We have previously shown that the reachability problem for this model is decidable. In this paper, we study the zenoness problem and show that it is EXPTIME-complete.

  • 13.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Clemente, Lorenzo
    Mayr, Richard
    Sandberg, Sven
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Stochastic Parity Games on Lossy Channel Systems2014Inngår i: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 10, nr 4, artikkel-id 21Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We give an algorithm for solving stochastic parity games with almost-sure winning conditions on lossy channel systems, under the constraint that both players are restricted to finitememory strategies. First, we describe a general framework, where we consider the class of 21/2-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game contains a finite attractor. An attractor is a set of states (not necessarily absorbing) that is almost surely re-visited regardless of the players' decisions. We present a scheme that characterizes the set of winning states for each player. Then, we instantiate this scheme to obtain an algorithm for stochastic game lossy channel systems.

    Fulltekst (pdf)
    fulltext
  • 14.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Dwarkadas, Sandhya
    University of Rochester, U.S.A..
    Rezine, Ahmed
    Linköping University.
    Shriraman, Arrvindh
    Simon Fraser University, Canada .
    Yunyun, Zhu
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Verifying safety and liveness for the FlexTM hybrid transactional memory2013Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We consider the verification of safety (strict serializability and abort consistency) and liveness obstruction and livelock freedom) for the hybrid transactional memory framework FlexTM. This framework allows for flexible implementations of transactional memories based on an adaptation of the MESI coherence protocol. FlexTM allows for both eager and lazy conflict resolution strategies. Like in the case of Software Transactional Memories, the verification problem is not trivial as the number of concurrent transactions, their size, and the number of accessed shared variables cannot be a priori bounded. This complexity is exacerbated by aspects that are specific to hardware and hybrid transactional memories. Our work takes into account intricate behaviours such as cache line based conflict detection, false sharing, invisible reads or non-transactional instructions. We carry out the first automatic verification of a hybrid transactional memory and establish, by adopting a small model approach, challenging properties such as strict serializability, abort consistency, and obstruction freedom for both an eager and a lazy conflict resolution strategies. We also detect an example that refutes livelock freedom. To achieve this, our prototype tool makes use of the latest antichain based techniques to handle systems with tens of thousands of states.

  • 15.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukás
    Block me if you can!: Context-sensitive parameterized verification2014Inngår i: Static Analysis: SAS 2014, Springer, 2014, s. 1-17Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We present a method for automatic verification of systems with a parameterized number of communicating processes, such as mutual exclusion protocols or agreement protocols. To that end, we present a powerful abstraction framework that uses an efficient and precise symbolic encoding of (infinite) sets of configurations. In particular, it generalizes downward-closed sets that have successfully been used in earlier approaches to parameterized verification. We show experimentally the efficiency of the method, on various examples, including a fine-grained model of Szymanski’s mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.

    Fulltekst (pdf)
    fulltext
  • 16.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukás
    Brno Univ Technol, Brno, Czech Republic.
    Parameterized verification through view abstraction2016Inngår i: International Journal on Software Tools for Technology Transfer, ISSN 1433-2779, E-ISSN 1433-2787, Vol. 18, nr 5, s. 495-516Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees. Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. 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. We show that the method is complete for a large class of well quasi-ordered systems including Petri nets. 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 verification problems. In particular, the method handles the fine-grained and full version of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.

  • 17.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukáš
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    All for the price of few: (Parameterized verification through view abstraction)2013Inngår i: Verification, Model Checking, and Abstract Interpretation, Springer Berlin/Heidelberg, 2013, s. 476-495Konferansepaper (Fagfellevurdert)
    Fulltekst (pdf)
    vmcai2013
  • 18.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik.
    Liang, Chencheng
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Rümmer, Philipp
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik. Univ Regensburg, Regensburg, Germany.
    Boosting Constrained Horn Solving by Unsat Core Learning2024Inngår i: Verification, Model Checking, and Abstract Interpretation / [ed] Rayna Dimitrova; Ori Lahav; Sebastian Wolff, Springer Nature, 2024, s. 280-302Konferansepaper (Fagfellevurdert)
    Abstract [en]

    The Relational Hyper-Graph Neural Network (R-HyGNN) was introduced in [1] to learn domain-specific knowledge from program verification problems encoded in Constrained Horn Clauses (CHCs). It exhibits high accuracy in predicting the occurrence of CHCs in counterexamples. In this research, we present an R-HyGNN-based framework called MUSHyperNet. The goal is to predict the Minimal Unsatisfiable Subsets (MUSes) (i.e., unsat core) of a set of CHCs to guide an abstract symbolic model checking algorithm. In MUSHyperNet, we can predict the MUSes once and use them in different instances of the abstract symbolic model checking algorithm. We demonstrate the efficacy of MUSHyperNet using two instances of the abstract symbolic modelchecking algorithm: Counter-Example Guided Abstraction Refinement (CEGAR) and symbolic model-checking-based (SymEx) algorithms. Our framework enhances performance on a uniform selection of benchmarks across all categories from CHC-COMP, solving more problems (6.1% increase for SymEx, 4.1% for CEGAR) and reducing average solving time (13.3% for SymEx, 7.1% for CEGAR).

  • 19.
    Abdulla, Parosh
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Trinh, Cong Quy
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Automated Verification of Linearization Policies2016Inngår i: Automated Verification of Linearization Policies: 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, 2016Konferansepaper (Annet vitenskapelig)
    Abstract [en]

    We present a novel framework for automated verification of linearizability for concurrent data structures that implement sets, stacks, and queues. The framework requires the user to provide a linearization policy, which describes how linearization point placement in different concurrent threads affect each other; such linearization policies are often provided informally together with descriptions of new algorithms. We present a specification formalism for linearization policies which allows the user to specify, in a simple and concise manner, complex patterns including non-fixed linearization points. To automate verification, we extend thread-modular reasoning to bound the number of considered threads, and use a novel symbolic representation for unbounded heap structures that store data from an unbounded domain. We have implemented our framework in a tool and successfully used it to prove linearizability for a wide range of algorithms, including all implementations of concurrent sets, stacks, and queues based on singly-linked lists that are known to us from the literature.

  • 20.
    Abdullah, Jakaria
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Dai, Gaoyang
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Mohaqeqi, Morteza
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Yi, Wang
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Schedulability Analysis and Software Synthesis for Graph-Based Task Models with Resource Sharing2018Inngår i: Proc. 24th Real-Time and Embedded Technology and Applications Symposium, IEEE Computer Society, 2018, s. 261-270Konferansepaper (Fagfellevurdert)
  • 21.
    Adler, Jeremy
    et al.
    Uppsala universitet, Science for Life Laboratory, SciLifeLab. Uppsala universitet, Medicinska och farmaceutiska vetenskapsområdet, Medicinska fakulteten, Institutionen för immunologi, genetik och patologi. Uppsala universitet, Medicinska och farmaceutiska vetenskapsområdet, Medicinska fakulteten, Institutionen för medicinsk cellbiologi. Uppsala Univ, Dept Immunol Genet & Pathol, BioVis, Uppsala, Sweden..
    Huang, Ainsley
    Univ Gothenburg, Sahlgrenska Acad, Inst Biomed, Dept Med Biochem & Cell Biol, Gothenburg, Sweden..
    Parmryd, Ingela
    Univ Gothenburg, Sahlgrenska Acad, Inst Biomed, Dept Med Biochem & Cell Biol, Gothenburg, Sweden..
    Find_plasma_membrane and measure_plasma_membrane: ImageJ macros for efficient identification of and measurements at and around the plasma membrane2023Inngår i: SoftwareX, E-ISSN 2352-7110, Vol. 24, artikkel-id 101570Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    The plasma membrane that encloses cells is difficult to precisely delineate but this is often required for quantitation of fluorescence images. We have created an ImageJ macro that efficiently maps the plasma membrane based on a few imprecisely marked points as the user input, to generate a one-pixel-wide region of interest. A second macro makes measurements from the plasma membrane and optionally from additional regions of interest, offset both inwards and outwards from the plasma membrane. While we are interested in membrane order quantified by generalized polarization, any measurements from two or more channels could easily be implemented.

  • 22.
    Adolfsson, Hampus
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Compiler Testing of C11 Atomics for Arm and RISC-V2022Independent thesis Advanced level (professional degree), 20 poäng / 30 hpOppgave
    Abstract [en]

    The C11 standard introduced atomic types and operations, with an accompanying memory model, to enable the use of shared variables in concurrent programs. In this thesis, I demonstrate how compilers can be tested, in a way that is deterministic and covers the entire set of atomic operations, to ensure they correctly implement C11 atomics and the C11 memory model. 

    I use a large set of short concurrent programs (”litmus tests”), generated from a model written in a specification language and based on a formalized C11 memory model. Each test program is compiled and run with a model checker, to determine the possible outcomes; any program with an outcome that is possible after compilation but not allowed by C11 is a failed test case. As an alternative to model checking, I also test a nondeterministic, hardware-based method for running tests, but I find that this method is too inaccurate to be useful. 

    I test IAR and gcc compilers for Arm and RISC-V; all of these compilers pass all tests. Out of three compilers with purposefully inserted bugs, all are correctly identified as faulty. This testing process thus shows some promise, but further evaluation is needed. 

    Fulltekst (pdf)
    fulltext
  • 23.
    Adolfsson, Mattias
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Developing a Graphical Application to Control Stepper Motors with Sensorless Load Detection2021Independent thesis Advanced level (professional degree), 20 poäng / 30 hpOppgave
    Abstract [en]

    For positioning of linear stages in absolute coordinates, there is a general need to find a reference position since the initial one is unknown. This is commonly called homing. To reduce costs and facilitate assembly, homing can be performed without additional sensors, known as sensorless homing. This thesis delves into sensorless homing, specifically with respect to stepper motors, and develops a graphical application for control of them. The commercial technology StallGuard is applied inconjunction with exploration into how it – and sensorless load detectionin general – functions. The resulting graphical application can be used to configure the stepper motors, perform homing using StallGuard, and automatically tune StallGuard to work despite varying conditions. In addition, rudimentary sensorless load detection independent from StallGuard is developed, demonstrating how it could work in practice. Testing shows homing with StallGuard resulting in a position within a ±5μm window in 94% of cases, less than 1/7 the width of an average strand of human hair. Additionally, homing is easily performed with a single button press from the graphical interface, with optional additional configuration available.

    Fulltekst (pdf)
    fulltext
  • 24. Afanasov, Mikhail
    et al.
    Anwar Bhatti, Naveed
    Dolui, Koustabh
    Mottola, Luca
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Tekniska sektionen, Institutionen för elektroteknik. Politecnico di Milano, Italy;RI.SE Sweden.
    Embedded Sensing through Energy Harvesting at the Mithræum of Circus Maximus2022Inngår i: Il Mitreo del Circo Massimo: Studio Preliminare di un Monumento Inedito tra Archeologia, Conservazione e Fruizione, EUT Edizioni Università di Trieste , 2022, s. 271-299Kapittel i bok, del av antologi (Annet vitenskapelig)
    Fulltekst (pdf)
    fulltext
  • 25. Afanasov, Mikhail
    et al.
    Bhatti, Naveed Anwar
    Campagna, Dennis
    Caslini, Giacomo
    Centonze, Fabio Massimo
    Dolui, Koustabh
    Maioli, Andrea
    Barone, Erica
    Alizai, Muhammad Hamad
    Siddiqui, Junaid Haroon
    Mottola, Luca
    Politecnico di Milano, Italy; RI.SE Sweden.
    Battery-less zero-maintenance embedded sensing at the mithræum of circus maximus2020Inngår i: SenSys '20: Proceedings of the 18th Conference on Embedded Networked Sensor Systems, 2020, s. 368-381Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We present the design and evaluation of a 3.5-year embedded sensing deployment at the Mithræum of Circus Maximus, a UNESCO-protected underground archaeological site in Rome (Italy). Unique to our work is the use of energy harvesting through thermal and kinetic energy sources. The extreme scarcity and erratic availability of energy, however, pose great challenges in system software, embedded hardware, and energy management. We tackle them by testing, for the first time in a multi-year deployment, existing solutions in intermittent computing, low-power hardware, and energy harvesting. Through three major design iterations, we find that these solutions operate as isolated silos and lack integration into a complete system, performing suboptimally. In contrast, we demonstrate the efficient performance of a hardware/software co-design featuring accurate energy management and capturing the coupling between energy sources and sensed quantities. Installing a battery-operated system alongside also allows us to perform a comparative study of energy harvesting in a demanding setting. Albeit the latter reduces energy availability and thus lowers the data yield to about 22% of that provided by batteries, our system provides a comparable level of insight into environmental conditions and structural health of the site. Further, unlike existing energy-harvesting deployments that are limited to a few months of operation in the best cases, our system runs with zero maintenance since almost 2 years, including 3 months of site inaccessibility due to a COVID19 lockdown.

  • 26. Afanasov, Mikhail
    et al.
    Djordjevic, Alessandro
    Liu, Feng
    Mottola, Luca
    Politecnico di Milano, Italy; RI.Se SICS Sweden.
    FlyZone: A Testbed for Experimenting with Aerial Drone Applications2019Inngår i: MobiSys '19 Proceedings of the 17th Annual International Conference on Mobile Systems, Applications, and Services, 2019, s. 67-78Konferansepaper (Fagfellevurdert)
    Fulltekst (pdf)
    fulltext
  • 27. Afanasov, Mikhail
    et al.
    Mottola, Luca
    Politecnico di Milano, Italy; RI.SE Sweden.
    The FlyZone Testbed Architecture for Aerial Drone Applications2020Inngår i: GetMobile: Mobile Computing and Communications, ISSN 2375-0529, E-ISSN 2375-0537, Vol. 24, nr 1Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Aerial drones represent a new breed of mobile computing. Compared to mobile phones and connected cars that only opportunistically sense or communicate, aerial drones offer direct control over their movements. They can thus implement functionality that were previously beyond reach, such as collecting high-resolution imagery, exploring near-inaccessible areas, or inspecting remote areas to gather fine-grain environmental data.

  • 28.
    Afanasov, Mikhail
    et al.
    Politecnico di Milano, Italy.
    Mottola, Luca
    Politecnico di Milano, Italy and SICS Swedish ICT.
    Ghezzi, Carlo
    Politecnico di Milano, Italy.
    Software Adaptation in Wireless Sensor Networks2018Inngår i: ACM Transactions on Autonomous and Adaptive Systems, ISSN 1556-4665, E-ISSN 1556-4703, Vol. 12, nr 4, artikkel-id 18Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present design concepts, programming constructs, and automatic verification techniques to support the development of adaptive Wireless Sensor Network (WSN) software. WSNs operate at the interface between the physical world and the computing machine and are hence exposed to unpredictable environment dynamics. WSN software must adapt to these dynamics to maintain dependable and efficient operation. However, developers are left without proper support to develop adaptive functionality in WSN software. Our work fills this gap with three key contributions: (i) design concepts help developers organize the necessary adaptive functionality and understand their relations, (ii) dedicated programming constructs simplify the implementations, (iii) custom verification techniques allow developers to check the correctness of their design before deployment. We implement dedicated tool support to tie the three contributions, facilitating their practical application. Our evaluation considers representative WSN applications to analyze code metrics, synthetic simulations, and cycle-accurate emulation of popular WSN platforms. The results indicate that our work is effective in simplifying the development of adaptive WSN software; for example, implementations are provably easier to test and to maintain, the run-time overhead of our dedicated programming constructs is negligible, and our verification techniques return results in a matter of seconds.

    Fulltekst (pdf)
    fulltext
  • 29.
    Ahmed, Jawwad
    et al.
    Ericsson Res, Stockholm, Sweden..
    Josefsson, Tim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Johnsson, Andreas
    Ericsson Res, Stockholm, Sweden..
    Flinta, Christofer
    Ericsson Res, Stockholm, Sweden..
    Moradi, Farnaz
    Ericsson Res, Stockholm, Sweden..
    Pasquini, Rafael
    Univ Fed Uberlandia, FACOM, Fac Comp, Uberlandia, MG, Brazil..
    Stadler, Rolf
    KTH Royal Inst Technol, ACCESS Linnaeus Ctr, Stockholm, Sweden.;RISE Swedish Inst Comp Sci SICS, Stockholm, Sweden..
    Automated Diagnostic of Virtualized Service Performance Degradation2018Inngår i: NOMS 2018 - 2018 IEEE/IFIP Network operations and management symposium, New York: IEEE, 2018Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Service assurance for cloud applications is a challenging task and is an active area of research for academia and industry. One promising approach is to utilize machine learning for service quality prediction and fault detection so that suitable mitigation actions can be executed. In our previous work, we have shown how to predict service-level metrics in real-time just from operational data gathered at the server side. This gives the service provider early indications on whether the platform can support the current load demand. This paper provides the logical next step where we extend our work by proposing an automated detection and diagnostic capability for the performance faults manifesting themselves in cloud and datacenter environments. This is a crucial task to maintain the smooth operation of running services and minimizing downtime. We demonstrate the effectiveness of our approach which exploits the interpretative capabilities of Self-Organizing Maps (SOMs) to automatically detect and localize different performance faults for cloud services.

  • 30. Ahmed, Saad
    et al.
    Bhakar, Abu
    Bhatti, Naveed Anwar
    Alizai, Muhammad Hamad
    Siddiqui, Junaid Haroon
    Mottola, Luca
    Politecnico di Milano, Italy; RI.SE SICS Sweden.
    The Betrayal of Constant Power × Time: Finding the Missing Joules of Transiently-powered Computers2019Inngår i: Proceedings of the 20th ACMSIGPLAN/SIGBED Conference on Languages, Compilers, and Toolsfor Embedded Systems (LCTES ’19), 2019Konferansepaper (Fagfellevurdert)
    Fulltekst (pdf)
    fulltext
  • 31. Ahmed, Saad
    et al.
    Bhatti, Naveed Anwar
    Alizai, Muhammad Hamad
    Siddiqui, Junaid Haroon
    Mottola, Luca
    Politecnico di Milano, Italy; RISE, Sweden.
    Fast and Energy-efficient State Checkpointing for Intermittent Computing2020Inngår i: ACM Transactions on Embedded Computing Systems, ISSN 1539-9087, E-ISSN 1558-3465, Vol. 19, nr 6, artikkel-id 45Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Intermittently powered embedded devices ensure forward progress of programs through state checkpointing in non-volatile memory. Checkpointing is, however, expensive in energy and adds to the execution times. To minimize this overhead, we present DICE, a system that renders differential checkpointing profitable on these devices. DICE is unique because it is a software-only technique and efficient because it only operates in volatile main memory to evaluate the differential. DICE may be integrated with reactive (Hibernus) or proactive (MementOS, HarvOS) checkpointing systems, and arbitrary code can be enabled with DICE using automatic code-instrumentation requiring no additional programmer effort. By reducing the cost of checkpoints, DICE cuts the peak energy demand of these devices, allowing operation with energy buffers that are one-eighth of the size originally required, thus leading to benefits such as smaller device footprints and faster recharging to operational voltage level. The impact on final performance is striking: with DICE, Hibernus requires one order of magnitude fewer checkpoints and one order of magnitude shorter time to complete a workload in real-world settings.

    Fulltekst (pdf)
    fulltext
  • 32. Ahmed, Saad
    et al.
    Bhatti, Naveed Anwar
    Alizai, Muhammad Hamad
    Siddiqui, Junaid
    Mottola, Luca
    Politecnico di Milano, Italy; RI.SE SICS Swedish.
    Efficient Intermittent Computing with Differential Checkpointing2019Inngår i: LCTES 2019 Proceedings of the 20th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, 2019, s. 70-81Konferansepaper (Fagfellevurdert)
    Fulltekst (pdf)
    fulltext
  • 33. Ahmed, Saad
    et al.
    Nawaz, Muhammad
    Bakar, Abu
    Bhatti, Naveed Anwar
    Alizai, Muhammad Hamad
    Siddiqui, Junaid Haroon
    Mottola, Luca
    Politecnico di Milano, Italy; RI.Se SICS, Sweden.
    Demystifying Energy Consumption Dynamics in Transiently powered Computers2020Inngår i: ACM Transactions on Embedded Computing Systems, ISSN 1539-9087, E-ISSN 1558-3465, Vol. 19, nr 6, artikkel-id 47Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Transiently powered computers (TPCs) form the foundation of the battery-less Internet of Things, using energy harvesting and small capacitors to power their operation. This kind of power supply is characterized by extreme variations in supply voltage, as capacitors charge when harvesting energy and discharge when computing. We experimentally find that these variations cause marked fluctuations in clock speed and power consumption. Such a deceptively minor observation is overlooked in existing literature. Systems are thus designed and parameterized in overly conservative ways, missing on a number of optimizations.

    We rather demonstrate that it is possible to accurately model and concretely capitalize on these fluctuations. We derive an energy model as a function of supply voltage and prove its use in two settings. First, we develop EPIC, a compile-time energy analysis tool. We use it to substitute for the constant power assumption in existing analysis techniques, giving programmers accurate information on worst-case energy consumption of programs. When using EPIC with existing TPC system support, run-time energy efficiency drastically improves, eventually leading up to a 350% speedup in the time to complete a fixed workload. Further, when using EPIC with existing debugging tools, it avoids unnecessary program changes that hurt energy efficiency. Next, we extend the MSPsim emulator and explore its use in parameterizing a different TPC system support. The improvements in energy efficiency yield up to more than 1000% time speedup to complete a fixed workload.

    Fulltekst (pdf)
    fulltext
  • 34. Ahmed, Saad
    et al.
    Ul Ain, Qurat
    Siddiqui, Junaid Haroon
    Mottola, Luca
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation. Politecnico di Milano, Italy; RI.SE Sweden.
    Alizai, Muhammad Hamad
    Intermittent Computing with Dynamic Voltage and Frequency Scaling2020Inngår i: EWSN '20: Proceedings of the 2020 International Conference on Embedded Wireless Systems and Networks / [ed] Christine Julien, Fabrice Valois, Omprakash Gnawali & Amy L. Murphy, 2020, s. 97-107Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We present D2VFS, a run-time technique to intelligently regulate supply voltage and accordingly reconfigure clock frequency of intermittently-computing devices. These devices rely on energy harvesting to power their operation and on small capacitors as energy buffer. Statically setting their clock frequency fails to achieve energy efficiency, as the setting remains oblivious of fluctuations in capacitor voltage and of their impact on a microcontroller operating range. In contrast, D2VFS captures these dynamics and places the microcontroller in the most efficient configuration by regulating the microcontroller supply voltage and changing its clock frequency. Our evaluation shows that D2VFS markedly increases energy efficiency; for example, ultimately enabling a 30-300% reduction of workload completion times.

  • 35.
    Aimoniotis, Pavlos
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation.
    Kvalsvik, Amund Bergland
    Norwegian University of Science and Technology (NTNU).
    Själander, Magnus
    Norwegian University of Science and Technology (NTNU).
    Kaxiras, Stefanos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation.
    Data-Out Instruction-In (DOIN!): Leveraging Inclusive Caches to Attack Speculative Delay Schemes2022Inngår i: 2022 IEEE International Symposium on Secure and Private Execution Environment Design (SEED 2022), Institute of Electrical and Electronics Engineers (IEEE), 2022, s. 49-60Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Although the cache has been a known side-channel for years, it has gained renewed notoriety with the introduction of speculative side-channel attacks such as Spectre, which were able to use caches to not just observe a victim, but to leak secrets. Because the cache continues to be one of the most exploitable side channels, it is often the primary target to safeguard in secure speculative execution schemes. One of the simpler secure speculation approaches is to delay speculative accesses whose effect can be observed until they become non-speculative. Delay-on-Miss, for example, delays all observable speculative loads, i.e., the ones that miss in the cache, and preserves the majority of the performance of the baseline (unsafe speculation) by executing speculative loads that hit in the cache, which were thought to be unobservable.

    However, previous work has failed to consider how instruction fetching can eject cache lines from the shared, lower level caches, and thus from higher cache levels due to inclusivity. In this work, we show how cache conflicts between instruction fetch and data accesses can extend previous attacks and present the following new insights:

    1. It is possible to use lower level caches to perform Prime+Probe through conflicts resulting from instruction fetching. This is an extension to previous Prime+Probe attacks that potentially avoids other developed mitigation strategies.

    2. Data-instruction conflicts can be used to perform a Spectre attack that breaks Delay-on-Miss. After acquiring a secret, secret-dependent instruction fetching can cause cache conflicts that result in evictions in the L1D cache, creating observable timing differences. Essentially, it is possible to leak a secret bit-by-bit through the cache, despite Delay-on-Miss defending against caches.

    We call our new attack Data-Out Instruction-In, DOIN!, and demonstrate it on a real commercial core, the AMD Ryzen 9. We demonstrate how DOIN! interacts with Delay-on-Miss and perform an analysis of noise and bandwidth. Furthermore, we propose a simple defense extension for Delay-on-Miss to maintain its security guarantees, at the cost of negligible performance degradation while executing the Spec06 workloads.

  • 36.
    Aimoniotis, Pavlos
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sakalis, Christos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sjalander, Magnus
    Norwegian Univ Sci & Technol, N-7491 Trondheim, Norway..
    Kaxiras, Stefanos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Reorder Buffer Contention: A Forward Speculative Interference Attack for Speculation Invariant Instructions2021Inngår i: IEEE COMPUTER ARCHITECTURE LETTERS, ISSN 1556-6056, Vol. 20, nr 2, s. 162-165Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Speculative side-channel attacks access sensitive data and use transmitters to leak the data during wrong-path execution. Various defenses have been proposed to prevent such information leakage. However, not all speculatively executed instructions are unsafe: Recent work demonstrates that speculation invariantinstructions are independent of speculative control-flow paths and are guaranteed to eventually commit, regardless of the speculation outcome. Compile-time information coupled with run-time mechanisms can then selectively lift defenses for speculation invariant instructions, reclaiming some of the lost performance. Unfortunately, speculation invariant instructions can easily be manipulated by a form of speculative interference to leak information via a new side-channel that we introduce in this paper. We show that forward speculative interference where older speculative instructions interfere with younger speculation invariant instructions effectively turns them into transmitters for secret data accessed during speculation. We demonstrate forward speculative interference on actual hardware, by selectively filling the reorder buffer (ROB) with instructions, pushing speculative invariant instructions in-or-out of the ROB on demand, based on a speculatively accessed secret. This reveals the speculatively accessed secret, as the occupancy of the ROB itself becomes a new speculative side-channel.

  • 37.
    Akbari, Saba
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Tekniska sektionen, Institutionen för elektroteknik, Nätverksbaserade inbyggda system.
    Bergman, Jan
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Fysiska sektionen, Institutet för rymdfysik, Uppsalaavdelningen.
    Voigt, Thiemo
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Tekniska sektionen, Institutionen för elektroteknik, Nätverksbaserade inbyggda system.
    Fredriksson, Jesper
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Fysiska sektionen, Institutet för rymdfysik, Uppsalaavdelningen.
    Hjort, Klas
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Tekniska sektionen, Institutionen för materialvetenskap, Mikrosystemteknik.
    Feasibility of Communication Between Sensor Nodes On-board Spacecraft Using Multi Layer Insulation2023Konferansepaper (Fagfellevurdert)
    Fulltekst (pdf)
    fulltext
  • 38.
    Akbari, Saba
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Tekniska sektionen, Institutionen för elektroteknik, Nätverksbaserade inbyggda system.
    Voigt, Thiemo
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Tekniska sektionen, Institutionen för elektroteknik, Nätverksbaserade inbyggda system.
    Hjort, Klas
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Tekniska sektionen, Institutionen för materialvetenskap, Mikrosystemteknik.
    Demo: Sensor Node Communication Through Conductive Mesh Placed on Cotton Knit Fabric2023Konferansepaper (Annet vitenskapelig)
    Fulltekst (pdf)
    fulltext
  • 39.
    Alipour, Mehdi
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Carlson, Trevor E.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Kaxiras, Stefanos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    A Taxonomy of Out-of-Order Instruction Commit2017Inngår i: 2017 Ieee International Symposium On Performance Analysis Of Systems And Software (Ispass), Los Alamitos: IEEE Computer Society, 2017, s. 135-136Konferansepaper (Fagfellevurdert)
    Abstract [en]

    While in-order instruction commit has its advantages, such as providing precise interrupts and avoiding complications with the memory consistency model, it requires the core to hold on to resources (reorder buffer entries, load/store queue entries, registers) until they are released in program order. In contrast, out-of-order commit releases resources much earlier, yielding improved performance without the need for additional hardware resources. In this paper, we revisit out-of-order commit from a different perspective, not by proposing another hardware technique, but by introducing a taxonomy and evaluating three different micro-architectures that have this technique enabled. We show how smaller processors can benefit from simple out-oforder commit strategies, but that larger, aggressive cores require more aggressive strategies to improve performance.

  • 40.
    Alipour, Mehdi
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation.
    Kumar, Rakesh
    Norwegian Univ Sci & Technol, Dept Comp Sci, Trondheim, Norway.
    Kaxiras, Stefanos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Black-Schaffer, David
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    FIFOrder MicroArchitecture: Ready-Aware Instruction Scheduling for OoO Processors2019Inngår i: 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE), IEEE, 2019, s. 716-721Konferansepaper (Fagfellevurdert)
    Abstract [en]

    The number of instructions a processor's instruction queue can examine (depth) and the number it can issue together (width) determine its ability to take advantage of the ILP in an application. Unfortunately, increasing either the width or depth of the instruction queue is very costly due to the content-addressable logic needed to wakeup and select instructions out-of-order. This work makes the observation that a large number of instructions have both operands ready at dispatch, and therefore do not benefit from out-of-order scheduling. We leverage this to place such ready-at-dispatch instructions in separate, simpler, in-order FIFO queues for scheduling. With such additional queues, we can reduce the size and width of the expensive out-of-order instruction queue, without reducing the processor's overall issue width and depth. Our design, FIFOrder, is able to steer more than 60% of instructions to the cheaper FIFO queues, providing a 50% energy savings over a traditional out-of-order instruction queue design, while delivering 8% higher performance.

    Fulltekst (pdf)
    Fiforder
  • 41.
    Alkhabbas, Fahed
    et al.
    Malmö Univ, Internet Things & People Res Ctr, S-21119 Malmö, Sweden.;Malmö Univ, Dept Comp Sci & Media Technol, S-21119 Malmö, Sweden..
    Alsadi, Mohammed
    Norwegian Univ Sci & Technol, Dept Comp Sci, N-7491 Trondheim, Norway..
    Alawadi, Sadi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för beräkningsvetenskap. Halmstad Univ, Ctr Appl Intelligent Syst Res, Sch Informat Technol, S-30118 Halmstad, Sweden..
    Awaysheh, Feras M.
    Univ Tartu, Delta Res Ctr, Inst Comp Sci, EE-51009 Tartu, Estonia..
    Kebande, Victor R.
    Blekinge Inst Technol, Dept Comp Sci DIDA, S-37179 Karlskrona, Sweden..
    Moghaddam, Mahyar T.
    Univ Southern Denmark, Maersk Mc Kinney Moller Inst MMMI, DK-5230 Odense, Denmark..
    ASSERT: A Blockchain-Based Architectural Approach for Engineering Secure Self-Adaptive IoT Systems2022Inngår i: Sensors, E-ISSN 1424-8220, Vol. 22, nr 18, artikkel-id 6842Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Internet of Things (IoT) systems are complex systems that can manage mission-critical, costly operations or the collection, storage, and processing of sensitive data. Therefore, security represents a primary concern that should be considered when engineering IoT systems. Additionally, several challenges need to be addressed, including the following ones. IoT systems' environments are dynamic and uncertain. For instance, IoT devices can be mobile or might run out of batteries, so they can become suddenly unavailable. To cope with such environments, IoT systems can be engineered as goal-driven and self-adaptive systems. A goal-driven IoT system is composed of a dynamic set of IoT devices and services that temporarily connect and cooperate to achieve a specific goal. Several approaches have been proposed to engineer goal-driven and self-adaptive IoT systems. However, none of the existing approaches enable goal-driven IoT systems to automatically detect security threats and autonomously adapt to mitigate them. Toward bridging these gaps, this paper proposes a distributed architectural Approach for engineering goal-driven IoT Systems that can autonomously SElf-adapt to secuRity Threats in their environments (ASSERT). ASSERT exploits techniques and adopts notions, such as agents, federated learning, feedback loops, and blockchain, for maintaining the systems' security and enhancing the trustworthiness of the adaptations they perform. The results of the experiments that we conducted to validate the approach's feasibility show that it performs and scales well when detecting security threats, performing autonomous security adaptations to mitigate the threats and enabling systems' constituents to learn about security threats in their environments collaboratively.

    Fulltekst (pdf)
    FULLTEXT01
  • 42.
    Alves, Ricardo
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. 2111 NE 25th Ave, Hillsboro, OR 97124 USA..
    Kaxiras, Stefanos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik.
    Black-Schaffer, David
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation.
    Early Address Prediction: Efficient Pipeline Prefetch and Reuse2021Inngår i: ACM Transactions on Architecture and Code Optimization (TACO), ISSN 1544-3566, E-ISSN 1544-3973, Vol. 18, nr 3, artikkel-id 39Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Achieving low load-to-use latency with low energy and storage overheads is critical for performance. Existing techniques either prefetch into the pipeline (via address prediction and validation) or provide data reuse in the pipeline (via register sharing or LO caches). These techniques provide a range of tradeoffs between latency, reuse, and overhead. In this work, we present a pipeline prefetching technique that achieves state-of-the-art performance and data reuse without additional data storage, data movement, or validation overheads by adding address tags to the register file. Our addition of register file tags allows us to forward (reuse) load data from the register file with no additional data movement, keep the data alive in the register file beyond the instruction's lifetime to increase temporal reuse, and coalesce prefetch requests to achieve spatial reuse. Further, we show that we can use the existing memory order violation detection hardware to validate prefetches and data forwards without additional overhead. Our design achieves the performance of existing pipeline prefetching while also forwarding 32% of the loads from the register file (compared to 15% in state-of-the-art register sharing), delivering a 16% reduction in L1 dynamic energy (1.6% total processor energy), with an area overhead of less than 0.5%.

    Fulltekst (pdf)
    FULLTEXT01
  • 43. Ansari, Iman
    et al.
    Barati, Masoud
    Sadeghi Moghadam, Mohammad Reza
    Ghobakhloo, Morteza
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Tekniska sektionen, Institutionen för samhällsbyggnad och industriell teknik, Industriell teknik.
    An Industry 4.0 readiness model for new technology exploitation2023Inngår i: International Journal of Quality & Reliability Management, ISSN 0265-671X, E-ISSN 1758-6682, Vol. 40, nr 10, s. 2519-2538Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Purpose

    Considering the importance and the broad applications of the Fourth Industrial Revolution in various organizations and industries and enjoying the many benefits of this digital transformation framework, organizations need to measure their Industry 4.0 readiness as a starting point and take steps to achieve the strategic goals of Industry 4.0. This study aims to design a comprehensive and practical model that can determine Industry 4.0 readiness level, allowing organizations to implement and exploit technological constituents of this phenomenon.

    Design/methodology/approach

    A systematic literature review (SLR) methodology was used to evaluate and summarize a clear and comprehensive literature overview of Industry 4.0 readiness models and to certify the validity and transparency of the review process. After reviewing 71 articles and survey and then the consensus of Industry 4.0 experts, the 10 dimensions of the 4.0 Industry readiness model were finalized with their indicators having the most frequency in the published articles and models.

    Findings

    The application of the SLR to the development of the new Industry 4.0 readiness model which includes 10 dimensions and 37 indicators and can assess the Industry 4.0 readiness of firms and industries accurately and effectively.

    Research limitations/implications

    An extensive review of the previous literature yielded the current Industry 4.0 readiness model. The comprehensiveness of this model leads to its wide application in different companies. Future research suggestions are presented at the end of the manuscript.

    Practical implications

    The concept of the Fourth Industrial Revolution and the application of its technologies are vague and complicated for many organizations and managers, while the need to implement the components and technologies of Industry 4.0 is essential to achieve organizational goals. The presented readiness model helps companies to measure their readiness to enter the Fourth Industrial Revolution and achieve long-term goals.

    Originality/value

    In this study, an attempt was made to examine the Industry 4.0 readiness models thoroughly and extensively and identify their different approaches. Finally, a comprehensive and multi-dimensional readiness model is presented to assess the position of organizations in order to enter Industry 4.0.

  • 44.
    Antonova, M.
    et al.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Asfandiyarov, R.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Bayes, R.
    Univ Glasgow, Sch Phys & Astron, Glasgow, Lanark, Scotland..
    Benoit, P.
    CERN, European Org Nucl Res, CH-1211 Geneva, Switzerland..
    Blondel, A.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Bogomilov, M.
    Univ Sofia, Dept Phys, Sofia, Bulgaria..
    Bross, A.
    Fermilab Natl Accelerator Lab, POB 500, Batavia, IL 60510 USA..
    Cadoux, F.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Cervera, A.
    CSIC, IFIC, Valencia, Spain.;Univ Valencia, Valencia, Spain..
    Chikuma, N.
    Univ Tokyo, Tokyo, Japan..
    Dudarev, A.
    CERN, European Org Nucl Res, CH-1211 Geneva, Switzerland..
    Ekelöf, Tord
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Fysiska sektionen, Institutionen för fysik och astronomi, Högenergifysik.
    Favre, Y.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Fedotov, S.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Hallsjo, S-P
    Univ Sofia, Dept Phys, Sofia, Bulgaria..
    Ichikawa, A. K.
    Kyoto Univ, Kyoto, Japan..
    Izmaylov, A.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Karadzhov, Y.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Khabibullin, M.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Khotyantsev, A.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Kleymenova, A.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Koga, T.
    Univ Tokyo, Tokyo, Japan..
    Kostin, A.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Kudenko, Y.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Likhacheva, V.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Martinez, B.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Matev, R.
    Univ Sofia, Dept Phys, Sofia, Bulgaria..
    Medvedeva, M.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Mefodiev, A.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Minamino, A.
    Yokohama Natl Univ, Yokohama, Kanagawa, Japan..
    Mineev, O.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Mitev, G.
    Bulgarian Acad Sci, Inst Nucl Res & Nucl Energy, Sofia, Bulgaria..
    Nessi, M.
    CERN, European Org Nucl Res, CH-1211 Geneva, Switzerland..
    Nicola, L.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Noah, E.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Ovsiannikova, T.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Da Silva, H. Pais
    CERN, European Org Nucl Res, CH-1211 Geneva, Switzerland..
    Parsa, S.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Rayner, M.
    Univ Geneva, Sect Phys, DPNC, Geneva, Switzerland..
    Rolando, G.
    CERN, European Org Nucl Res, CH-1211 Geneva, Switzerland..
    Shaykhiev, A.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Simion, P.
    Uppsala universitet.
    Soler, P.
    Univ Glasgow, Sch Phys & Astron, Glasgow, Lanark, Scotland..
    Suvorov, S.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Tsenov, R.
    Univ Sofia, Dept Phys, Sofia, Bulgaria..
    Ten Kate, H.
    CERN, European Org Nucl Res, CH-1211 Geneva, Switzerland..
    Vankova-Kirilova, G.
    Univ Sofia, Dept Phys, Sofia, Bulgaria..
    Yershov, N.
    Russian Acad Sci, Inst Nucl Res, Moscow, Russia..
    Synchronization of the distributed readout frontend electronics of the Baby MIND detector2017Inngår i: 2017 XXVI International Scientific Conference Electronics (ET), IEEE, 2017Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Baby MIND is a new downstream muon range detector for the WGASCI experiment. This article discusses the distributed readout system and its timing requirements. The paper presents the design of the synchronization subsystem and the results of its test.

  • 45.
    Areskog, Oskar
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för systemteknik.
    Labelling Customer Actions in an Autonomous Store Using Human Action Recognition2022Independent thesis Advanced level (professional degree), 20 poäng / 30 hpOppgave
    Abstract [en]

    Automation is fundamentally changing many industries and retail is no exception. Moonshopis a South African venture trying to solve the problem of autonomous grocery storesusing cameras and computer vision. This project is the continuation of a hackathon heldto explore different methods for Human Action Recognition in Moonshop’s stores.Throughout the project a pipeline for data processing has been developed and two typesof Graph-Convolutional Networks, CTR-GCN and ST-GCN, have been implementedand evaluated on the data produced by this pipeline. The resulting scores aren’t goodenough to call it a success. However, this is not necessarily a fault of the models. Rather,there wasn’t enough data to train on and the existing data was of varying to low quality.This makes it complicated to justly judge the models’ performances. In the future, moreresources should be spent on generating more and better data in order to really evaluatethe feasibility of using Human Action Recognition and Graph-Convolutional Networksat Moonshop.

    Fulltekst (pdf)
    Labelling-Customer-Actions-Using-HAR
  • 46.
    Aronis, Stavros
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Lystig Fritchie, Scott
    VMware, Cambridge, MA, USA.
    Testing And Verifying Chain Repair Methods For CORFU Using Stateless Model Checking2017Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Corfu is a distributed shared log that is designed to be scalable and reliable in the presence of failures and asynchrony. Internally, Corfu is fully replicated for fault tolerance, without sharding data or sacrificing strong consistency. In this case study, we present the modeling approaches we followed to test and verify, using Concuerror, the correctness of repair methods for the Chain Replication protocol suitable for Corfu. In the first two methods we tried, Concuerror located bugs quite fast. In contrast, the tool did not manage to find bugs in the third method, but the time this took also motivated an improvement in the tool that reduces the number of traces explored. Besides more details about all the above, we present experiences and lessons learned from applying stateless model checking for verifying complex protocols suitable for distributed programming.

    Fulltekst (pdf)
    fulltext
  • 47.
    Asad, Hafiz Areeb
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Wouters, Erik Henricus
    Bhatti, Naveed Anwar
    Mottola, Luca
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation. RISE.
    Voigt, Thiemo
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorarkitektur och datorkommunikation. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. RISE.
    On Securing Persistent State in Intermittent Computing2020Inngår i: ENSsys '20: Proceedings of the 8th International Workshop on Energy Harvesting and Energy-Neutral Sensing Systems, 2020, s. 8-14Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We present the experimental evaluation of different security mechanisms applied to persistent state in intermittent computing. Whenever executions become intermittent because of energy scarcity, systems employ persistent state on non-volatile memories (NVMs) to ensure forward progress of applications. Persistent state spans operating system and network stack, as well as applications. While a device is off recharging energy buffers, persistent state on NVMs may be subject to security threats such as stealing sensitive information or tampering with configuration data, which may ultimately corrupt the device state and render the system unusable. Based on modern platforms of the Cortex M* series, we experimentally investigate the impact on typical intermittent computing workloads of different means to protect persistent state, including software and hardware implementations of staple encryption algorithms and the use of ARM TrustZone protection mechanisms. Our results indicate that i) software implementations bear a significant overhead in energy and time, sometimes harming forward progress, but also retaining the advantage of modularity and easier updates; ii) hardware implementations offer much lower overhead compared to their software counterparts, but require a deeper understanding of their internals to gauge their applicability in given application scenarios; and iii) TrustZone shows almost negligible overhead, yet it requires a different memory management and is only effective as long as attackers cannot directly access the NVMs.

  • 48.
    Asada, Akira
    et al.
    Osaka Institute of Technology.
    Hayashi, Masaki
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    Hirayama, Makoto
    Osaka Institute of Technology.
    A museum video guide creation system with CG Made from scripts on the server2020Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Museums provide not only audio guides but also video guides. But the video guide production needs a lot of manpower. We have developed a museum guide creation system that facilitates the video guide production for the museums. The video guide creator uploads the script to the server, and the visitor accesses the script with a smartphone application and views it as a CG animation. We use an existing Content Management System - "Wordpress" for the script input. With this system, museum guide creators simply access the blog site by Wordpress and post an article which is in this case a scenario of a museum guide. As for the next step, we plan to make our museum guide creation system open to the public, and will allow many people to create and register movie guide scripts voluntarily just like the Wikipedia. 

  • 49.
    Asada, Akira
    et al.
    Osaka Inst Technol, Fac Informat Sci & Technol, Osaka, Japan.
    Hayashi, Masaki
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Institutionen för speldesign.
    Hirayama, Makoto J.
    Osaka Inst Technol, Fac Informat Sci & Technol, Osaka, Japan.
    TV production tool to make art programmes based on a simple scenario2019Inngår i: INTERNATIONAL WORKSHOP ON ADVANCED IMAGE TECHNOLOGY (IWAIT) 2019 / [ed] Kemao, Q Hayase, K Lau, PY Lie, WN Lee, YL Srisuk, S Yu, L, SPIE-INT SOC OPTICAL ENGINEERING , 2019, artikkel-id 1104921Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We have been studying and developing the real-time Computer Graphics (CG) based virtual museum where a user can walk through to appreciate artworks digitized in high-resolution. Our virtual museum also has a function to automatically create TV program-like CG animations using 3D CG models in the virtual space as it is so that the user can learn about individual works by watching the art shows. The CG animation is produced with TVML (TV program Making Language) engine implemented on the virtual museum. However, the current problem is that it requires a lot of work for a developer to write the complicated TVML scripts manually Therefore, this time we have developed a special tool to help the developer to prepare the TVML scripts easily. With this tool, the developer can produce the TVML-based art program simply by writing out a simple scenario on an ordinary text editor. In order to design this tool, TV art programs actually broadcasted are analyzed to determine the syntax of the simple scenario. Based on the analysis, we have developed the tool with TVML engine working on the Unity game Engine. We have also used this tool to imitate the broadcasted TV program to validate its usability.

  • 50. Ashjaei, Mohammad
    et al.
    Clegg, Kester
    Corneo, Lorenzo
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Hawkins, Richard
    Jaradat, Omar
    Gulisano, Vincenzo Massimiliano
    Nikolakopoulos, Yiannis
    Service Level Agreements for Safe and Configurable Production Environments2018Inngår i: 2018 IEEE 23rd International Conference on Emerging Technologies and Factory Automation (ETFA), IEEE, 2018, s. 1252-1255Konferansepaper (Fagfellevurdert)
    Abstract [en]

    This paper focuses on Service Level Agreements (SLAs) for industrial applications that aim to port some of the control functionalities to the cloud. In such applications, industrial requirements should be reflected in SLAs. In this paper, we present an approach to integrate safety-related aspects of an industrial application to SLAs. We also present the approach in a use case. This is an initial attempt to enrich SLAs for industrial settings to consider safety aspects, which has not been investigated thoroughly before.

1234567 1 - 50 of 503
RefereraExporteraLink til resultatlisten
Permanent link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf