Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 6 of 6
Full-Text Articles in Physical Sciences and Mathematics
Understanding The Genetic Makeup Of Linux Device Drivers, Peter Senna Tschudin, Laurent Reveillere, Lingxiao Jiang, David Lo, Julia Lawall
Understanding The Genetic Makeup Of Linux Device Drivers, Peter Senna Tschudin, Laurent Reveillere, Lingxiao Jiang, David Lo, Julia Lawall
Research Collection School Of Computing and Information Systems
No abstract provided.
From Rssi To Csi: Indoor Localization Via Channel Response, Zheng Yang, Zimu Zhou, Yunhao Liu
From Rssi To Csi: Indoor Localization Via Channel Response, Zheng Yang, Zimu Zhou, Yunhao Liu
Research Collection School Of Computing and Information Systems
The spatial features of emitted wireless signals are the basis of location distinction and determination for wireless indoor localization. Available in mainstream wireless signal measurements, the Received Signal Strength Indicator (RSSI) has been adopted in vast indoor localization systems. However, it suffers from dramatic performance degradation in complex situations due to multipath fading and temporal dynamics.
Cell: A Compositional Verification Framework, Kun Ji, Yang Liu, Jun Sun, Jun Sun, Jin Song Dong, Truong Khanh Nguyen
Cell: A Compositional Verification Framework, Kun Ji, Yang Liu, Jun Sun, Jun Sun, Jin Song Dong, Truong Khanh Nguyen
Research Collection School Of Computing and Information Systems
This paper presents CELL, a comprehensive and extensible framework for compositional verification of concurrent and real-time systems based on commonly used semantic models. For each semantic model, CELL offers three libraries, i.e., compositional verification paradigms, learning algorithms and model checking methods to support various state-of-the-art compositional verification approaches. With well-defined APIs, the framework could be applied to build customized model checkers. In addition, each library could be used independently for verification and program analysis purposes. We have built three model checkers with CELL. The experimental results show that the performance of these model checkers can offer similar or often better …
Tower Of Babel: A Crowdsourcing Game Building Sentiment Lexicons For Resource-Scarce Languages, Yoonsung Hong, Haewoon Kwak, Youngmin Baek, Sue. Moon
Tower Of Babel: A Crowdsourcing Game Building Sentiment Lexicons For Resource-Scarce Languages, Yoonsung Hong, Haewoon Kwak, Youngmin Baek, Sue. Moon
Research Collection School Of Computing and Information Systems
With the growing amount of textual data produced by online social media today, the demands for sentiment analysis are also rapidly increasing; and, this is true for worldwide. However, non-English languages often lack sentiment lexicons, a core resource in performing sentiment analysis. Our solution, Tower of Babel (ToB), is a language-independent sentiment-lexicon-generating crowdsourcing game. We conducted an experiment with 135 participants to explore the difference between our solution and a conventional manual annotation method. We evaluated ToB in terms of effectiveness, efficiency, and satisfactions. Based on the result of the evaluation, we conclude that sentiment classification via ToB is accurate, …
Verifying Linearizability Via Optimized Refinement Checking, Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun, Shao Jie Zhang, Jin Song Dong Dong
Verifying Linearizability Via Optimized Refinement Checking, Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun, Shao Jie Zhang, Jin Song Dong Dong
Research Collection School Of Computing and Information Systems
Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that: 1) All executions of concurrent operations are serializable, and 2) the serialized executions are correct with respect to the sequential semantics. In this work, we describe a method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. The method does not require that linearization points in the implementations be given, which is often difficult or impossible. However, the method takes advantage of linearization points if they are given. The method is based on …
Modeling And Verifying Hierarchical Real-Time Systems Using Stateful Timed Csp, Jun Sun, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi, Étienne André
Modeling And Verifying Hierarchical Real-Time Systems Using Stateful Timed Csp, Jun Sun, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi, Étienne André
Research Collection School Of Computing and Information Systems
Modeling and verifying complex real-time systems are challenging research problems. The de facto approach is based on Timed Automata, which are finite state automata equipped with clock variables. Timed Automata are deficient in modeling hierarchical complex systems. In this work, we propose a language called Stateful Timed CSP and an automated approach for verifying Stateful Timed CSP models. Stateful Timed CSP is based on Timed CSP and is capable of specifying hierarchical real-time systems. Through dynamic zone abstraction, finite-state zone graphs can be generated automatically from Stateful Timed CSP models, which are subject to model checking. Like Timed Automata, Stateful …