Open Access. Powered by Scholars. Published by Universities.®
- Discipline
-
- Physical Sciences and Mathematics (8519)
- Computer Sciences (8502)
- Databases and Information Systems (3446)
- Software Engineering (2153)
- Artificial Intelligence and Robotics (1686)
-
- Information Security (1056)
- Numerical Analysis and Scientific Computing (1023)
- Engineering (955)
- Graphics and Human Computer Interfaces (926)
- Social and Behavioral Sciences (734)
- Business (685)
- Computer Engineering (511)
- Theory and Algorithms (493)
- Operations Research, Systems Engineering and Industrial Engineering (417)
- Programming Languages and Compilers (379)
- OS and Networks (322)
- Communication (310)
- Social Media (248)
- Public Affairs, Public Policy and Public Administration (227)
- Transportation (204)
- Medicine and Health Sciences (183)
- Education (178)
- Management Information Systems (177)
- Data Storage Systems (175)
- E-Commerce (151)
- International and Area Studies (125)
- Asian Studies (124)
- Digital Communications and Networking (123)
- Technology and Innovation (114)
- Health Information Technology (110)
- Keyword
-
- Deep learning (124)
- Machine learning (124)
- Social media (80)
- Artificial intelligence (71)
- Reinforcement learning (69)
-
- Data mining (65)
- Privacy (61)
- Cloud computing (58)
- Deep Learning (56)
- Empirical study (55)
- Optimization (55)
- Security (53)
- Singapore (52)
- Visualization (52)
- Twitter (50)
- Neural networks (49)
- Online learning (49)
- Software engineering (49)
- Training (49)
- Task analysis (48)
- Anomaly detection (47)
- Collaboration (45)
- Feature extraction (45)
- Large Language Models (45)
- Blockchain (44)
- Semantics (43)
- Access control (41)
- Algorithms (40)
- Android (39)
- Classification (38)
- Publication Year
- File Type
Articles 7441 - 7470 of 8692
Full-Text Articles in Entire DC Network
Adoption Of 3-D Virtual Worlds For Education, X. Chen, Keng Siau, Fiona Fui-Hoon Nah
Adoption Of 3-D Virtual Worlds For Education, X. Chen, Keng Siau, Fiona Fui-Hoon Nah
Research Collection School Of Computing and Information Systems
As an emerging phenomenon, virtual world education is rarely researched in MIS literature. With stiff competition among institutions using virtual worlds for education, a legitimate research question is: What factors influence students’ intention to adopt 3-D virtual world environment for their education needs? Drawing on existing technology acceptance models and studies in other IS contexts, we developed a model to predict students’ acceptance of a 3-D virtual world education environment and plan to empirically test the model using survey data collected from college students. From the academic research perspective, studies on the use of the new technology for education will …
Chosen-Ciphertext Secure Proxy Re-Encryption Without Pairing, Robert H. Deng, Jian Weng, Shengli Liu, Kefei Chen
Chosen-Ciphertext Secure Proxy Re-Encryption Without Pairing, Robert H. Deng, Jian Weng, Shengli Liu, Kefei Chen
Research Collection School Of Computing and Information Systems
In a proxy re-encryption system, a semi-trusted proxy can convert a ciphertext originally intended for Alice into a ciphertext intended for Bob, without learning the underlying plaintext. Proxy re-encryption has found many practical applications, such as encrypted email forwarding, secure distributed file systems, and outsourced filtering of encrypted spam. In ACM CCS'07, Canetti and Hohenberger presented a proxy re-encryption scheme with chosen-ciphertext security, and left an important open problem to construct a chosen-ciphertext secure proxy re-encryption scheme without pairings. In this paper, we solve this open problem by proposing a new proxy re-encryption scheme without resort to bilinear pairings. Based …
Privacy Engine For Context-Aware Enterprise Application Services, Marion Blount, John Davis, Maria Ebling, William Jerome, Barry Leiba, Xuan Liu, Archan Misra
Privacy Engine For Context-Aware Enterprise Application Services, Marion Blount, John Davis, Maria Ebling, William Jerome, Barry Leiba, Xuan Liu, Archan Misra
Research Collection School Of Computing and Information Systems
Satisfying the varied privacy preferences of individuals, while exposing context data to authorized applications and individuals, remains a major challenge for context-aware computing. This paper describes our experiences in building a middleware component, the context privacy engine (CPE), that enforces a role-based, context-dependent privacy model for enterprise domains. While fundamentally an ACL-based access control scheme, CPE extends the traditional ACL mechanism with usage control and context constraints. This paper focuses on discussing issues related to managing and evaluating context-dependent privacy policies. Extensive experimental studies with a production-grade implementation and real-life context sources demonstrate that the CPE can support a large …
Innovation In The Programmable Web: Characterizing The Mashup Ecosystem, C. Jason Woodard, Shuli Yu
Innovation In The Programmable Web: Characterizing The Mashup Ecosystem, C. Jason Woodard, Shuli Yu
Research Collection School Of Computing and Information Systems
This paper investigates the structure and dynamics of the Web 2.0 software ecosystem by analyzing empirical data on web service APIs and mashups. Using network analysis tools to visualize the growth of the ecosystem from December 2005 to 2007, we find that the APIs are organized into three tiers, and that mashups are often formed by combining APIs across tiers. Plotting the cumulative distribution of mashups to APIs reveals a power-law relationship, although the tail is short compared to previously reported distributions of book and movie sales. While this finding highlights the dominant role played by the most popular APIs …
Making Sense Of Technology Trends In The Information Technology Landscape, Gediminas Adomavicius, Jesse C. Bockstedt, Alok Gupta, Robert J. Kauffman
Making Sense Of Technology Trends In The Information Technology Landscape, Gediminas Adomavicius, Jesse C. Bockstedt, Alok Gupta, Robert J. Kauffman
Research Collection School Of Computing and Information Systems
A major problem for firms making information technology investment decisions is predicting and understanding the effects of future technological developments on the value of present technologies. Failure to adequately address this problem can result in wasted organization resources in acquiring, developing, managing, and training employees in the use of technologies that are short-lived and fail to produce adequate return on investment. The sheer number of available technologies and the complex set of relationships among them make IT landscape analysis extremely challenging. Most IT-consuming firms rely on third parties and suppliers for strategic recommendations on IT investments, which can lead to …
On Visualizing Heterogeneous Semantic Networks From Multiple Data Sources, Maureen Maureen, Aixin Sun, Ee Peng Lim, Anwitaman Datta, Kuiyu Chang
On Visualizing Heterogeneous Semantic Networks From Multiple Data Sources, Maureen Maureen, Aixin Sun, Ee Peng Lim, Anwitaman Datta, Kuiyu Chang
Research Collection School Of Computing and Information Systems
In this paper, we focus on the visualization of heterogeneous semantic networks obtained from multiple data sources. A semantic network comprising a set of entities and relationships is often used for representing knowledge derived from textual data or database records. Although the semantic networks created for the same domain at different data sources may cover a similar set of entities, these networks could also be very different because of naming conventions, coverage, view points, and other reasons. Since digital libraries often contain data from multiple sources, we propose a visualization tool to integrate and analyze the differences among multiple social …
Beyond Semantic Search: What You Observe May Not Be What You Think, Chong-Wah Ngo, Yu-Gang Jiang, Xiaoyong Wei, Wanlei Zhao, Feng Wang, Xiao Wu, Hung-Khoon Tan
Beyond Semantic Search: What You Observe May Not Be What You Think, Chong-Wah Ngo, Yu-Gang Jiang, Xiaoyong Wei, Wanlei Zhao, Feng Wang, Xiao Wu, Hung-Khoon Tan
Research Collection School Of Computing and Information Systems
This paper presents our approaches and results of the four TRECVID 2008 tasks we participated in: high-level feature extraction, automatic video search, video copy detection, and rushes summarization
A Neural Network Model For A Hierarchical Spatio-Temporal Memory, Kiruthika Ramanathan, Luping Shi, Jianming Li, Kian Guan Lim, Zhi Ping Ang, Chong Chong Tow
A Neural Network Model For A Hierarchical Spatio-Temporal Memory, Kiruthika Ramanathan, Luping Shi, Jianming Li, Kian Guan Lim, Zhi Ping Ang, Chong Chong Tow
Research Collection School Of Computing and Information Systems
The architecture of the human cortex is uniform and hierarchical in nature. In this paper, we build upon works on hierarchical classification systems that model the cortex to develop a neural network representation for a hierarchical spatio-temporal memory (HST-M) system. The system implements spatial and temporal processing using neural network architectures. We have tested the algorithms developed against both the MLP and the Hierarchical Temporal Memory algorithms. Our results show definite improvement over MLP and are comparable to the performance of HTM.
Model-Driven Remote Attestation: Attesting Remote System From Behavioral Aspect, Liang Gu, Xuhua Ding, Robert H. Deng, Yanzhen Zou, Bing Xie, Weizhong Shao, Hong Mei
Model-Driven Remote Attestation: Attesting Remote System From Behavioral Aspect, Liang Gu, Xuhua Ding, Robert H. Deng, Yanzhen Zou, Bing Xie, Weizhong Shao, Hong Mei
Research Collection School Of Computing and Information Systems
Remote attestation was introduced in TCG specifications to determine whether a remote system is trusted to behave in a particular manner for a specific purpose; however, most of the existing approaches attest only the integrity state of a remote system and hence have a long way to go in achieving the above attestation objective. Behavior-based attestation and semantic attestation were recently introduced as solutions to approach the TCG attestation objective. In this paper, we extend behavior-based attestation to a model-driven remote attestation to prove that a remote system is trusted as defined by TCG. Our model-driven remote attestation verifies two …
Modality Mixture Projections For Semantic Video Event Detection, Jialie Shen, Dacheng Tao, Xuelong Li
Modality Mixture Projections For Semantic Video Event Detection, Jialie Shen, Dacheng Tao, Xuelong Li
Research Collection School Of Computing and Information Systems
Event detection is one of the most fundamental components for various kinds of domain applications of video information system. In recent years, it has gained a considerable interest of practitioners and academics from different areas. While detecting video event has been the subject of extensive research efforts recently, much less existing approach has considered multimodal information and related efficiency issues. In this paper, we use a subspace selection technique to achieve fast and accurate video event detection using a subspace selection technique. The approach is capable of discriminating different classes and preserving the intramodal geometry of samples within an identical …
Profile-Guided Program Simplification For Effective Testing And Analysis, Lingxiao Jiang, Zhendong Su
Profile-Guided Program Simplification For Effective Testing And Analysis, Lingxiao Jiang, Zhendong Su
Research Collection School Of Computing and Information Systems
Many testing and analysis techniques have been developed for inhouse use. Although they are effective at discovering defects before a program is deployed, these techniques are often limited due to the complexity of real-world code and thus miss program faults. It will be the users of the program who eventually experience failures caused by the undetected faults. To take advantage of the large number of program runs carried by the users, recent work has proposed techniques to collect execution profiles from the users for developers to perform post-deployment failure analysis. However, in order to protect users' privacy and to reduce …
Market Liquidity Provision For On-Demand Computing, Zhiling Guo
Market Liquidity Provision For On-Demand Computing, Zhiling Guo
Research Collection School Of Computing and Information Systems
This paper focuses on a market intermediary’s role of liquidity provision to support on-demand computing in a dynamic market trading environment. We outline a framework in which a number of distributed agents sell and buy assets based on their changing utilities over time and a service provider acts as a market maker performing market intervention. We present benchmark models based on socially optimal liquidity provision and a brokerage framework. We then examine the benefits and the dealer’s incentives to provide market liquidity.
Virtual World Affordances: Enhancing Brand Value, S. Park, Fiona Fui-Hoon Nah, D. Dewester, B. Eschenbrenner, S. Jeon
Virtual World Affordances: Enhancing Brand Value, S. Park, Fiona Fui-Hoon Nah, D. Dewester, B. Eschenbrenner, S. Jeon
Research Collection School Of Computing and Information Systems
Virtual worlds are three-dimensional, computer-generated worlds that are a natural extension of the existing Internet. Although many businesses are jumping on the bandwagon to maintain a presence in virtual worlds, there is no well-established knowledge or theory to guide businesses in their involvement in these environments. In this paper, we identify affordances in the virtual worlds that can be used to increase the state of flow experienced in a business virtual site, which in turn may enhance brand equity, or the perceived added value of a brand to customers. We present a conceptual model that can be used to guide …
A New Framework For The Design And Analysis Of Identity-Based Identification Schemes, Guomin Yang, Jing Chen, Duncan S. Wong, Xiaotie Deng, Dongsheng Wang
A New Framework For The Design And Analysis Of Identity-Based Identification Schemes, Guomin Yang, Jing Chen, Duncan S. Wong, Xiaotie Deng, Dongsheng Wang
Research Collection School Of Computing and Information Systems
Constructing an identification scheme is one of the fundamental problems in cryptography, and is very useful in practice. An identity-based identification (IBI) scheme allows a prover to identify himself to a public verifier who knows only the claimed identity of the prover and some public information. In this paper, we propose a new framework for both the design and analysis of IBI schemes. Our approach works in an engineering way. We first identify an IBI scheme as the composition of two building blocks, and then show that, with different security properties of these building blocks, the corresponding IBI schemes can …
Two-Factor Mutual Authentication Based On Smart Cards And Passwords, Guomin Yang, Duncan S. Wong, Huaxiong Wang, Xiaotie Deng
Two-Factor Mutual Authentication Based On Smart Cards And Passwords, Guomin Yang, Duncan S. Wong, Huaxiong Wang, Xiaotie Deng
Research Collection School Of Computing and Information Systems
One of the most commonly used two-factor user authentication mechanisms nowadays is based on smart-card and password. A scheme of this type is called a smart-card-based password authentication scheme. The core feature of such a scheme is to enforce two-factor authentication in the sense that the client must have the smart-card and know the password in order to gain access to the server. In this paper, we scrutinize the security requirements of this kind of schemes, and propose a new scheme and a generic construction framework for smart-card-based password authentication. We show that a secure password based key exchange protocol …
Bias And Controversy In Evaluation Systems, Hady Wirawan Lauw, Ee Peng Lim, Ke Wang
Bias And Controversy In Evaluation Systems, Hady Wirawan Lauw, Ee Peng Lim, Ke Wang
Research Collection School Of Computing and Information Systems
Evaluation is prevalent in real life. With the advent of Web 2.0, online evaluation has become an important feature in many applications that involve information (e.g., video, photo, and audio) sharing and social networking (e.g., blogging). In these evaluation settings, a set of reviewers assign scores to a set of objects. As part of the evaluation analysis, we want to obtain fair reviews for all the given objects. However, the reality is that reviewers may deviate in their scores assigned to the same object, due to the potential bias of reviewers or controversy of objects. The statistical approach of averaging …
Representative Entry Selection For Profiling Blogs, Jinfeng Zhuang, Steven C. H. Hoi, Aixin Sun, Rong Jin
Representative Entry Selection For Profiling Blogs, Jinfeng Zhuang, Steven C. H. Hoi, Aixin Sun, Rong Jin
Research Collection School Of Computing and Information Systems
Many applications on blog search and mining often meet the challenge of handling huge volume of blog data, in which one single blog could contain hundreds or even thousands of entries. We investigate novel techniques for profiling blogs by selecting a subset of representative entries for each blog. We propose two principles for guiding the entry selection task: representativeness and diversity. Further, we formulate the entry selection task into a combinatorial optimization problem and propose a greedy yet effective algorithm for finding a good approximate solution by exploiting the theory of submodular functions. We suggest blog classification for judging the …
Leveraging Social Context For Searching Social Media, Marc Smith, Vladimir Barash, Lise Getoor, Hady W. Lauw
Leveraging Social Context For Searching Social Media, Marc Smith, Vladimir Barash, Lise Getoor, Hady W. Lauw
Research Collection School Of Computing and Information Systems
The ability to utilize and benefit from today's explosion of social media sites depends on providing tools that allow users to productively participate. In order to participate, users must be able to find resources (both people and information) that they find valuable. Here, we argue that in order to do this effectively, we should make use of a user's "social context". A user's social context includes both their personal social context (their friends and the communities to which they belong) and their community social context (their role and identity in different communities).
Impacts Of Information And Communication Technologies On Country Development: Accounting For Area Interrelationships, Robert J. Kauffman, Ajay Kumar
Impacts Of Information And Communication Technologies On Country Development: Accounting For Area Interrelationships, Robert J. Kauffman, Ajay Kumar
Research Collection School Of Computing and Information Systems
Single-item composite indices gauge ICT readiness at the country level but do not represent the direct impact of ICTs on a country's development. This paper describes a new approach to measuring the macrolevel impacts of ICTs across a range of development areas. The indirect effects of one area on others is taken into consideration by a simultaneous equation model that permits the inclusion of multiple development areas. The model is applied to data pertaining to four development areas in 64 countries: trade flows, agricultural productivity, R&D, and quality of life. ICT readiness is found to have a positive association with …
Using English Information In Non-English Web Search, Wei Gao, Wei Gao, Ming Zhou
Using English Information In Non-English Web Search, Wei Gao, Wei Gao, Ming Zhou
Research Collection School Of Computing and Information Systems
The leading web search engines have spent a decade building highly specialized ranking functions for English web pages. One of the reasons these ranking functions are effective is that they are designed around features such as PageRank, automatic query and domain taxonomies, and click-through information, etc. Unfortunately, many of these features are absent or altered in other languages. In this work, we show how to exploit these English features for a subset of Chinese queries which we call linguistically non-local (LNL). LNL Chinese queries have a minimally ambiguous English translation which also functions as a good English query. We first …
Model Checking Csp Revisited: Introducing A Process Analysis Toolkit, Jun Sun, Yang Liu, Jin Song Dong
Model Checking Csp Revisited: Introducing A Process Analysis Toolkit, Jun Sun, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
FDR, initially introduced decades ago, is the de facto analyzer for Communicating Sequential Processes (CSP). Model checking techniques have been evolved rapidly since then. This paper describes PAT, i.e., a process analysis toolkit which complements FDR in several aspects. PAT is designed to analyze event-based compositional system models specified using CSP as well as shared variables and asynchronous message passing. It supports automated refinement checking, model checking of LTL extended with events, etc. In this paper, we highlight how partial order reduction is applied to improve refinement checking in PAT. Experiment results show that PAT outperforms FDR in some cases.
Event Detection With Common User Interests, Meishan Hu, Aixin Sun, Ee Peng Lim
Event Detection With Common User Interests, Meishan Hu, Aixin Sun, Ee Peng Lim
Research Collection School Of Computing and Information Systems
In this paper, we aim at detecting events of common user interests from huge volume of user-generated content. The degree of interest from common users in an event is evidenced by a significant surge of event-related queries issued to search for documents (e.g., news articles, blog posts) relevant to the event. Taking the stream of queries from users and the stream of documents as input, our proposed framework seamlessly integrates the two streams into a single stream of query profiles. A query profile is a set of documents matching a query at a given time. With the single stream of …
Specification Mining Of Symbolic Scenario-Based Models, David Lo, Shahar Maoz
Specification Mining Of Symbolic Scenario-Based Models, David Lo, Shahar Maoz
Research Collection School Of Computing and Information Systems
Many dynamic analysis approaches to specification mining, which extract behavioral models from execution traces, do not consider object identities. This limits their power when used to analyze traces of general object oriented programs. In this work we present a novel specification mining approach that considers object identities, and, moreover, generalizes from specifications involving concrete objects to their symbolic class-level abstractions. Our approach uses data mining methods to extract significant scenario-based specifications in the form of Damm and Harel's live sequence charts (LSC), a formal and expressive extension of classic sequence diagrams. We guarantee that all mined symbolic LSCs are significant …
Spreadsheet Data Resampling For Monte-Carlo Simulation, Thin Yin Leong, Wee Leong Lee
Spreadsheet Data Resampling For Monte-Carlo Simulation, Thin Yin Leong, Wee Leong Lee
Research Collection School Of Computing and Information Systems
The pervasiveness of spreadsheets software resulted in its increased application as a simulation tool for business analysis. Random values generation supporting such evaluations using spreadsheets are simple and yet powerful. However, the typical approach to Monte-Carlo simulations, which is what simulations with stochasticity are called, requires significant amount of time to be spent on data collection, data collation, and distribution function fitting. In fact, the latter can be overwhelming for undergraduate students to learn and do properly in a short time. Resampling eliminates both the need to fit distributions to the sample data, and to perform the ensuing tests of …
Remote Attestation On Program Execution, Liang Gu, Xuhua Ding, Robert H. Deng, Bing Xie, Hong Mei
Remote Attestation On Program Execution, Liang Gu, Xuhua Ding, Robert H. Deng, Bing Xie, Hong Mei
Research Collection School Of Computing and Information Systems
Remote attestation provides the basis for one platform to establish trusts on another. In this paper, we consider the problem of attesting the correctness of program executions. We propose to measure the target program and all the objects it depends on, with an assumption that the Secure Kernel and the Trusted Platform Module provide a secure execution environment through process separation. The attestation of the target program begins with a program analysis on the source code or the binary code in order to find out the relevant executables and data objects. Whenever such a data object is accessed or a …
Bayesian Tensor Approach For 3-D Face Modeling, Dacheng Tao, Mingli Song, Xuelong Li, Jialie Shen, Jimeng Sun, Xindong Wu, Christos Faloutsos, Stephen J. Maybank
Bayesian Tensor Approach For 3-D Face Modeling, Dacheng Tao, Mingli Song, Xuelong Li, Jialie Shen, Jimeng Sun, Xindong Wu, Christos Faloutsos, Stephen J. Maybank
Research Collection School Of Computing and Information Systems
Effectively modeling a collection of three-dimensional (3-D) faces is an important task in various applications, especially facial expression-driven ones, e.g., expression generation, retargeting, and synthesis. These 3-D faces naturally form a set of second-order tensors-one modality for identity and the other for expression. The number of these second-order tensors is three times of that of the vertices for 3-D face modeling. As for algorithms, Bayesian data modeling, which is a natural data analysis tool, has been widely applied with great success; however, it works only for vector data. Therefore, there is a gap between tensor-based representation and vector-based data analysis …
A Study Of Early Stage Game Design And Prototyping, Brien Colwell, Richard C. Davis, James A. Landay
A Study Of Early Stage Game Design And Prototyping, Brien Colwell, Richard C. Davis, James A. Landay
Research Collection School Of Computing and Information Systems
Computer games and simulations can be valuable teaching and communication tools, and they are a powerful form of self-expression. Unfortunately, creating games requires programming, and programming requires time and skill. Some tools facilitate game creation to motivate novice programmers, but programming is still necessary. Other systems require less programming, but they are narrowly focused. To enable faster, simpler, and more expressive tools for professionals and amateurs, we have explored the processes and tools used in the early stages of game and simulation design. Interviews with educators clarified the uses of simulations in the classroom, while interviews with professional game designers …
Understanding Evolution In Technology Ecosystems, Gediminas Adomavicius, Jesse Bockstedt, Alok Gupta, Robert J. Kauffman
Understanding Evolution In Technology Ecosystems, Gediminas Adomavicius, Jesse Bockstedt, Alok Gupta, Robert J. Kauffman
Research Collection School Of Computing and Information Systems
The current environment of information technology can be a complex place for analysts and firms to navigate, especially when making decisions about new product development, technology investment, and technology planning. Many industry analysts recognize that it is difficult, if not impossible, to accurately predict future technological advances. However, successful firms need to understand the nature of technological change and evolution in order to accurately forecast and take advantage of investment and market opportunities. For example, although RFID has been in the news for the past decade as the potential distribution and retail "killer technology", uncertainties about its future technical capabilities, …
An Effective Approach To 3d Deformable Surface Tracking, Jianke Zhu, Steven C. H. Hoi, Zenglin Xu, Michael R. Lyu
An Effective Approach To 3d Deformable Surface Tracking, Jianke Zhu, Steven C. H. Hoi, Zenglin Xu, Michael R. Lyu
Research Collection School Of Computing and Information Systems
The key challenge with 3D deformable surface tracking arises from the difficulty in estimating a large number of 3D shape parameters from noisy observations. A recent state-of-the-art approach attacks this problem by formulating it as a Second Order Cone Programming (SOCP) feasibility problem. The main drawback of this solution is the high computational cost. In this paper, we first reformulate the problem into an unconstrained quadratic optimization problem. Instead of handling a large set of complicated SOCP constraints, our new formulation can be solved very efficiently by resolving a set of sparse linear equations. Based on the new framework, a …
Specifying And Verifying Sensor Networks: An Experiment Of Formal Methods, Jin Song Dong, Jing Sun, Jun Sun, Kenji Taguchi, Xian Zhang
Specifying And Verifying Sensor Networks: An Experiment Of Formal Methods, Jin Song Dong, Jing Sun, Jun Sun, Kenji Taguchi, Xian Zhang
Research Collection School Of Computing and Information Systems
With the development of sensor technology and electronic miniaturization, wireless sensor networks have shown a wide range of promising applications as well as challenges. Early stage sensor network analysis is critical, which allows us to reveal design errors before sensor deployment. Due to their distinguishable features, system specification and verification of sensor networks are highly non-trivial tasks. On the other hand, numerous formal theories and analysis tools have been developed in formal methods community, which may offer a systematic method for formal analysis of sensor networks. This paper presents our attempt on applying formal methods to sensor network specification/verification. An …