Open Access. Powered by Scholars. Published by Universities.®
- Discipline
-
- Physical Sciences and Mathematics (8549)
- Computer Sciences (8532)
- Databases and Information Systems (3451)
- Software Engineering (2164)
- Artificial Intelligence and Robotics (1697)
-
- Information Security (1067)
- Numerical Analysis and Scientific Computing (1024)
- Engineering (956)
- Graphics and Human Computer Interfaces (933)
- Social and Behavioral Sciences (734)
- Business (686)
- Computer Engineering (512)
- Theory and Algorithms (493)
- Operations Research, Systems Engineering and Industrial Engineering (417)
- Programming Languages and Compilers (379)
- OS and Networks (323)
- Communication (310)
- Social Media (248)
- Public Affairs, Public Policy and Public Administration (227)
- Transportation (204)
- Medicine and Health Sciences (186)
- Education (180)
- Management Information Systems (178)
- Data Storage Systems (176)
- E-Commerce (151)
- International and Area Studies (125)
- Asian Studies (124)
- Digital Communications and Networking (123)
- Technology and Innovation (114)
- Health Information Technology (113)
- Keyword
-
- Machine learning (125)
- Deep learning (124)
- Social media (80)
- Artificial intelligence (72)
- Reinforcement learning (69)
-
- Data mining (65)
- Privacy (65)
- Cloud computing (58)
- Deep Learning (56)
- Empirical study (55)
- Optimization (55)
- Security (54)
- Singapore (52)
- Visualization (52)
- Task analysis (50)
- Twitter (50)
- Neural networks (49)
- Online learning (49)
- Software engineering (49)
- Training (49)
- Anomaly detection (47)
- Feature extraction (46)
- Collaboration (45)
- Large Language Models (45)
- Blockchain (44)
- Semantics (43)
- Access control (41)
- Algorithms (40)
- Android (39)
- Natural language processing (39)
- Publication Year
- File Type
Articles 6061 - 6090 of 8722
Full-Text Articles in Entire DC Network
Ropsteg: Program Steganography With Return Oriented Programming, Kangjie Lu, Siyang Xiong, Debin Gao
Ropsteg: Program Steganography With Return Oriented Programming, Kangjie Lu, Siyang Xiong, Debin Gao
Research Collection School Of Computing and Information Systems
Many software obfuscation techniques have been proposed to hide program instructions or logic and to make reverse engineering hard. In this paper, we introduce a new property in software obfuscation, namely program steganography, where certain instructions are "diffused" in others in such a way that they are non-existent until program execution. Program steganography does not raise suspicion in program analysis, and conforms to the W⊕X and mandatory code signing security mechanisms. We further implement RopSteg, a novel software obfuscation system, to provide (to a certain degree) program steganography using return-oriented programming. We apply RopSteg to eight Windows executables and evaluate …
Theorems About Quadrilaterals And Conics, Dorde Baralic, Branko Grbic, Dorde Zikelic
Theorems About Quadrilaterals And Conics, Dorde Baralic, Branko Grbic, Dorde Zikelic
Research Collection School Of Computing and Information Systems
We study quadrilaterals inscribed and circumscribed about conics and prove interesting theorems. Theorems are discovered by experimenting with dynamical geometry software. The Poncelet theorem for quadrilaterals is proved by elementary means together with Poncelet's grid property.
L-Opacity: Linkage-Aware Graph Anonymization, Sadegh Nobari, Panagiotis Karras, Hwee Hwa Pang, Stephane Bressan
L-Opacity: Linkage-Aware Graph Anonymization, Sadegh Nobari, Panagiotis Karras, Hwee Hwa Pang, Stephane Bressan
Research Collection School Of Computing and Information Systems
The wealth of information contained in online social networks has created a demand for the publication of such data as graphs. Yet, publication, even after identities have been removed, poses a privacy threat. Past research has suggested ways to publish graph data in a way that prevents the re-identification of nodes. However, even when identities are effectively hidden, an adversary may still be able to infer linkage between individuals with sufficiently high confidence. In this paper, we focus on the privacy threat arising from such link disclosure. We suggest L-opacity, a sufficiently strong privacy model that aims to control an …
Sampled Fictitious Play For Multi-Action Stochastic Dynamic Programs, Archis Ghate, Shih-Fen Cheng, Stephen Baumert, Daniel Reaume, Dushyant Sharma, Robert L. Smith
Sampled Fictitious Play For Multi-Action Stochastic Dynamic Programs, Archis Ghate, Shih-Fen Cheng, Stephen Baumert, Daniel Reaume, Dushyant Sharma, Robert L. Smith
Research Collection School Of Computing and Information Systems
We introduce a class of finite-horizon dynamic optimization problems that we call multi-action stochastic dynamic programs (DPs). Their distinguishing feature is that the decision in each state is a multi-dimensional vector. These problems can in principle be solved using Bellman's backward recursion. However, complexity of this procedure grows exponentially in the dimension of the decision vectors. This is called the curse of action-space dimensionality. To overcome this computational challenge, we propose an approximation algorithm rooted in the game theoretic paradigm of Sampled Fictitious Play (SFP). SFP solves a sequence of DPs with a one-dimensional action-space, which are exponentially smaller than …
Time-Series Data Mining In Transportation: A Case Study On Singapore Public Train Commuter Travel Patterns, Tin Seong Kam, Roy Ka Wei Lee
Time-Series Data Mining In Transportation: A Case Study On Singapore Public Train Commuter Travel Patterns, Tin Seong Kam, Roy Ka Wei Lee
Research Collection School Of Computing and Information Systems
The adoption of smart cards technologies and automated data collection systems (ADCS) in transportation domain had provided public transport planners opportunities to amass a huge and continuously increasing amount of time-series data about the behaviors and travel patterns of commuters. However the explosive growth of temporal related databases has far outpaced the transport planners’ ability to interpret these data using conventional statistical techniques, creating an urgent need for new techniques to support the analyst in transforming the data into actionable information and knowledge. This research study thus explores and discusses the potential use of time-series data mining, a relatively new …
Digital Certificate Management: Optimal Pricing And Crl Releasing Strategies, Jie Zhang, Nan Hu, M. K. Raka
Digital Certificate Management: Optimal Pricing And Crl Releasing Strategies, Jie Zhang, Nan Hu, M. K. Raka
Research Collection School Of Computing and Information Systems
The fast growth of e-commerce and online activities places increasing needs for authentication and secure communication to enable information exchange and online transactions. The public key infrastructure (PKI) provides a promising foundation for meeting such demand, in which certificate authorities (CAs) provide digital certificates. In practice, it is critical to understand consumer purchasing and revocation behaviors so that CAs can better manage the digital certificates and its CRL releasing process. To address this problem, we analytically model a CA's pricing and revocation releasing strategies taking into consideration the users' rational decisions. The model provides solutions two main research questions: (1) …
Examining The Growth Of Digital Wireless Phone Technology: A Take-Off Theory Analysis, Angsana A. Techatassanasoontorn, Robert J. Kauffman
Examining The Growth Of Digital Wireless Phone Technology: A Take-Off Theory Analysis, Angsana A. Techatassanasoontorn, Robert J. Kauffman
Research Collection School Of Computing and Information Systems
The early phase of diffusion plays a critical role in determining information technology (IT) success in a market. Takeoff, the transition point from the introduction to the growth phase in the IT life cycle, is viewed as an acid test for whether a technology will succeed. We develop a theory to understand global takeoff for digital wireless phones that can be extended to other technologies with related characteristics. Drawing on technology dominance and product life cycle theories, we build a model that consists of standards, market competition, technology costs, and technology substitution to explain takeoff and subsequent market penetration growth. …
Integrating Water Exclusion Theory Into Β Contacts To Predict Binding Free Energy Changes And Binding Hot Spots, Qian Liu, Steven C. H. Hoi, Chee Keong Kwoh, Limsoon Wong, Jinyan Li
Integrating Water Exclusion Theory Into Β Contacts To Predict Binding Free Energy Changes And Binding Hot Spots, Qian Liu, Steven C. H. Hoi, Chee Keong Kwoh, Limsoon Wong, Jinyan Li
Research Collection School Of Computing and Information Systems
Binding free energy and binding hot spots at protein-protein interfaces are two important research areas for understanding protein interactions. Computational methods have been developed previously for accurate prediction of binding free energy change upon mutation for interfacial residues. However, a large number of interrupted and unimportant atomic contacts are used in the training phase which caused accuracy loss. Results: This work proposes a new method, β ACV ASA , to predict the change of binding free energy after alanine mutations. β ACV ASA integrates accessible surface area (ASA) and our newly defined β contacts together into an atomic contact vector …
Representative Discovery Of Structure Cues For Weakly-Supervised Image Segmentation, Luming Zhang, Yue Gao, Yingjie Xia, Ke Lu, Jialie Shen, Rongrong Ji
Representative Discovery Of Structure Cues For Weakly-Supervised Image Segmentation, Luming Zhang, Yue Gao, Yingjie Xia, Ke Lu, Jialie Shen, Rongrong Ji
Research Collection School Of Computing and Information Systems
Weakly-supervised image segmentation is a challenging problem with multidisciplinary applications in multimedia content analysis and beyond. It aims to segment an image by leveraging its imagelevel semantics (i.e., tags). This paper presents a weakly-supervised image segmentation algorithm that learns the distribution of spatially structural superpixel sets from image-level labels. More specifically, we first extract graphlets from a given image, which are small-sized graphs consisting of superpixels and encapsulating their spatial structure. Then, an ecient manifold embedding algorithm is proposed to transfer labels from training images into graphlets. It is further observed that there are numerous redundant graphlets that are not …
Livelabs: Building An In-Situ Real-Time Mobile Experimentation Testbed, Rajesh Krishna Balan, Archan Misra, Youngki Lee
Livelabs: Building An In-Situ Real-Time Mobile Experimentation Testbed, Rajesh Krishna Balan, Archan Misra, Youngki Lee
Research Collection School Of Computing and Information Systems
We present LiveLabs, a mobile experimentation testbed that is currently deployed across our university campus with further deployments at a large shopping mall, a commercial airport, and a resort island soon to follow. The key goal of LiveLabs is to allow in-situ real-time experimentation of mobile applications and services that require context-specific triggers with real participants on their actual smart phones. We describe how LiveLabs works, and then explain the novel R&D required to realise it. We end with a descriptionof the current LiveLabs status (> 700 active participants to date) as well as present some key lessons learned.
Key-Aggregate Cryptosystem For Scalable Data Sharing In Cloud Storage, Cheng-Kang Chu, Sherman S. M. Chow, Wen-Guey Tzeng, Jiangying Zhou, Robert H. Deng
Key-Aggregate Cryptosystem For Scalable Data Sharing In Cloud Storage, Cheng-Kang Chu, Sherman S. M. Chow, Wen-Guey Tzeng, Jiangying Zhou, Robert H. Deng
Research Collection School Of Computing and Information Systems
Data sharing is an important functionality in cloud storage. In this article, we show how to securely, efficiently, and flexibly share data with others in cloud storage. We describe new public-key cryptosystems which produce constant-size ciphertexts such that efficient delegation of decryption rights for any set of ciphertexts are possible. The novelty is that one can aggregate any set of secret keys and make them as compact as a single key, but encompassing the power of all the keys being aggregated. In other words, the secret key holder can release a constant-size aggregate key for flexible choices of ciphertext set …
Ropecker: A Generic And Practical Approach For Defending Against Rop Attack, Yueqiang Cheng, Zongwei Zhou, Yu Miao, Xuhua Ding, Robert H. Deng
Ropecker: A Generic And Practical Approach For Defending Against Rop Attack, Yueqiang Cheng, Zongwei Zhou, Yu Miao, Xuhua Ding, Robert H. Deng
Research Collection School Of Computing and Information Systems
Return-Oriented Programming (ROP) is a sophisticated exploitation technique that is able to drive target applications to perform arbitrary unintended operations by constructing a gadget chain reusing existing small code sequences (gadgets). Existing defense mechanisms either only handle specific types of gadgets, require access to source code and/or a customized compiler, break the integrity of application binary, or suffer from high performance overhead. In this paper, we present a novel system, ROPecker, to efficiently and effectively defend against ROP attacks without relying on any other side information (e.g., source code and compiler support) or binary rewriting. ROPecker detects an ROP attack …
Sketch: Pen And Touch Recognition [Workshop Summary], Richard C. Davis, Aaron Adler
Sketch: Pen And Touch Recognition [Workshop Summary], Richard C. Davis, Aaron Adler
Research Collection School Of Computing and Information Systems
Sketch recognition has technically been around for 40 years, but it has come and gone several times due to the difficulty of the problem. With the rise of touch and pen enabled phones and tablets, sketch recognition is regaining popularity and public presence, and more people are becoming aware of and interested in this difficult, but valuable, problem. It is important to harness the Sketch Recognition community at this time to encourage the flourishing of this topic.
Democracy Is Good For Ranking: Towards Multi-View Rank Learning And Adaptation In Web Search, Wei Gao, Pei Yang
Democracy Is Good For Ranking: Towards Multi-View Rank Learning And Adaptation In Web Search, Wei Gao, Pei Yang
Research Collection School Of Computing and Information Systems
No abstract provided.
Sinabro: Opportunistic And Unobtrusive Mobile Ecg Monitoring System, Seungwoo Kang, Sungjun Kwon, Sangwon Seo, Chungkuk Yoo, Kwangsuk Park, Junehwa Song, Youngki Lee
Sinabro: Opportunistic And Unobtrusive Mobile Ecg Monitoring System, Seungwoo Kang, Sungjun Kwon, Sangwon Seo, Chungkuk Yoo, Kwangsuk Park, Junehwa Song, Youngki Lee
Research Collection School Of Computing and Information Systems
In this paper, we propose Sinabro, an opportunistic and unobtrusive mobile electrocardiogram (ECG) monitoring system that monitors the user’s ECG opportunistically during daily smartphone use. Daily ECG monitoring will open up an unprecedented opportunity for pervasive healthcare applications. It will enable the daily detection and prevention of heart problems and also allow inferences about stress, emotion, and even sleep quality. Despite its huge potential, daily ECG monitoring still has not become reality due to its obtrusiveness. In this paper, we first study the potential opportunity to capture ECGs from daily use of smartphones, without requiring the user’s explicit attention. Based …
Building Thinc: User Incentivization And Meeting Rescheduling For Energy Savings, Jun Young Kwak, Debarun Kar, William Haskell, Pradeep Reddy Varakantham, Milind Tambe
Building Thinc: User Incentivization And Meeting Rescheduling For Energy Savings, Jun Young Kwak, Debarun Kar, William Haskell, Pradeep Reddy Varakantham, Milind Tambe
Research Collection School Of Computing and Information Systems
This paper presents THINC, an agent developed for saving energy in real-world commercial buildings. While previous work has presented techniques for computing energy-efficient schedules, it fails to address two issues, centered on human users, that are essential in real-world agent deployments: (i) incentivizing users for their energy saving activities and (ii) interacting with users to reschedule key “energy-consuming” meetings in a timely fashion, while handling the uncertainty in such interactions. THINC addresses these shortcomings by providing four new major contributions. First, THINC computes fair division of credits from energy savings. For this fair division, THINC provides novel algorithmic advances for …
Visual Typo Correction By Collocative Optimization: A Case Study On Merchandize Images, Xiao-Yong Wei, Zhen-Qun Yang, Chong-Wah Ngo, Wei Zhang
Visual Typo Correction By Collocative Optimization: A Case Study On Merchandize Images, Xiao-Yong Wei, Zhen-Qun Yang, Chong-Wah Ngo, Wei Zhang
Research Collection School Of Computing and Information Systems
Near-duplicate retrieval (NDR) in merchandize images is of great importance to a lot of online applications on e-Commerce websites. In those applications where the requirement of response time is critical, however, the conventional techniques developed for a general purpose NDR are limited, because expensive post-processing like spatial verification or hashing is usually employed to compromise the quantization errors among the visual words used for the images. In this paper, we argue that most of the errors are introduced because of the quantization process where the visual words are considered individually, which has ignored the contextual relations among words. We propose …
Towards More Accurate Multi-Label Software Behavior Learning, Xin Xia, Feng Yang, David Lo, Zhenyu Chen, Xinyu Wang
Towards More Accurate Multi-Label Software Behavior Learning, Xin Xia, Feng Yang, David Lo, Zhenyu Chen, Xinyu Wang
Research Collection School Of Computing and Information Systems
In a modern software system, when a program fails, a crash report which contains an execution trace would be sent to the software vendor for diagnosis. A crash report which corresponds to a failure could be caused by multiple types of faults simultaneously. Many large companies such as Baidu organize a team to analyze these failures, and classify them into multiple labels (i.e., multiple types of faults). However, it would be time-consuming and difficult for developers to manually analyze these failures and come out with appropriate fault labels. In this paper, we automatically classify a failure into multiple types of …
Automated Construction Of A Software-Specific Word Similarity Database, Yuan Tian, David Lo, Julia Lawall
Automated Construction Of A Software-Specific Word Similarity Database, Yuan Tian, David Lo, Julia Lawall
Research Collection School Of Computing and Information Systems
Many automated software engineering approaches, including code search, bug report categorization, and duplicate bug report detection, measure similarities between two documents by analyzing natural language contents. Often different words are used to express the same meaning and thus measuring similarities using exact matching of words is insufficient. To solve this problem, past studies have shown the need to measure the similarities between pairs of words. To meet this need, the natural language processing community has built WordNet which is a manually constructed lexical database that records semantic relations among words and can be used to measure how similar two words …
Identity Based Identification From Algebraic Coding Theory, Guomin Yang, Chik How Tan, Yi Mu, Willy Susilo, Duncan S. Wong
Identity Based Identification From Algebraic Coding Theory, Guomin Yang, Chik How Tan, Yi Mu, Willy Susilo, Duncan S. Wong
Research Collection School Of Computing and Information Systems
Cryptographic identification schemes allow a remote user to prove his/her identity to a verifier who holds some public information of the user, such as the user public key or identity. Most of the existing cryptographic identification schemes are based on numbertheoretic hard problems such as Discrete Log and Factorization. This paper focuses on the design and analysis of identity based identification (IBI) schemes based on algebraic coding theory. We first revisit an existing code-based IBI scheme which is derived by combining the Courtois–Finiasz–Sendrier signature scheme and the Stern zero-knowledge identification scheme. Previous results have shown that this IBI scheme is …
Integrating Water Exclusion Theory Into Β Contacts To Predict Binding Free Energy Changes And Binding Hot Spots, Qian Liu, Steven C. H. Hoi, Chee Keong Kwoh, Limsoon Wong, Jinyan Li
Integrating Water Exclusion Theory Into Β Contacts To Predict Binding Free Energy Changes And Binding Hot Spots, Qian Liu, Steven C. H. Hoi, Chee Keong Kwoh, Limsoon Wong, Jinyan Li
Research Collection School Of Computing and Information Systems
Binding free energy and binding hot spots at protein-protein interfaces are two important research areas for understanding protein interactions. Computational methods have been developed previously for accurate prediction of binding free energy change upon mutation for interfacial residues. However, a large number of interrupted and unimportant atomic contacts are used in the training phase which caused accuracy loss. Results: This work proposes a new method, β ACV ASA , to predict the change of binding free energy after alanine mutations. β ACV ASA integrates accessible surface area (ASA) and our newly defined β contacts together into an atomic contact vector …
Los And Nlos Classification For Underwater Acoustic Localization, Roee Diamant, Hwee-Pink Tan, Lutz Lampe
Los And Nlos Classification For Underwater Acoustic Localization, Roee Diamant, Hwee-Pink Tan, Lutz Lampe
Research Collection School Of Computing and Information Systems
The low sound speed in water makes propagation delay (PD)-based range estimation attractive for underwater acoustic localization (UWAL). However, due to the long channel impulse response and the existence of reflectors, PD-based UWAL suffers from significant degradation when PD measurements of nonline-of-sight (NLOS) communication links are falsely identified as line-of-sight (LOS). In this paper, we utilize expected variation of PD measurements due to mobility of nodes and present an algorithm to classify the former into LOS and NLOS links. First, by comparing signal strength-based and PD-based range measurements, we identify object-related NLOS (ONLOS) links, where signals are reflected from objects …
Extended Comprehensive Study Of Association Measures For Fault Localization, Lucia Lucia, David Lo, Lingxiao Jiang, Ferdian Thung, Aditya Budi
Extended Comprehensive Study Of Association Measures For Fault Localization, Lucia Lucia, David Lo, Lingxiao Jiang, Ferdian Thung, Aditya Budi
Research Collection School Of Computing and Information Systems
Spectrum-based fault localization is a promising approach to automatically locate root causes of failures quickly. Two well-known spectrum-based fault localization techniques, Tarantula and Ochiai, measure how likely a program element is a root cause of failures based on profiles of correct and failed program executions. These techniques are conceptually similar to association measures that have been proposed in statistics, data mining, and have been utilized to quantify the relationship strength between two variables of interest (e.g., the use of a medicine and the cure rate of a disease). In this paper, we view fault localization as a measurement of the …
Predicting Response In Mobile Advertising With Hierarchical Importance-Aware Factorization Machine, Richard Jayadi Oentaryo, Ee Peng Lim, Jia Wei Low, David Lo, Michael Finegold
Predicting Response In Mobile Advertising With Hierarchical Importance-Aware Factorization Machine, Richard Jayadi Oentaryo, Ee Peng Lim, Jia Wei Low, David Lo, Michael Finegold
Research Collection School Of Computing and Information Systems
Mobile advertising has recently seen dramatic growth, fueled by the global proliferation of mobile phones and devices. The task of predicting ad response is thus crucial for maximizing business revenue. However, ad response data change dynamically over time, and are subject to cold-start situations in which limited history hinders reliable prediction. There is also a need for a robust regression estimation for high prediction accuracy, and good ranking to distinguish the impacts of different ads. To this end, we develop a Hierarchical Importance-aware Factorization Machine (HIFM), which provides an effective generic latent factor framework that incorporates importance weights and hierarchical …
An Empirical Study Of Bug Report Field Reassignment, Xin Xia, David Lo, Ming Wen, Shihab Emad, Bo Zhou
An Empirical Study Of Bug Report Field Reassignment, Xin Xia, David Lo, Ming Wen, Shihab Emad, Bo Zhou
Research Collection School Of Computing and Information Systems
A bug report contains many fields, such as product, component, severity, priority, fixer, operating system (OS), platform, etc., which provide important information for the bug triaging and fixing process. It is important to make sure that bug information is correct since previous studies showed that the wrong assignment of bug report fields could increase the bug fixing time, and even delay the delivery of the software. In this paper, we perform an empirical study on bug report field reassignments in open-source software projects. To better understand why bug report fields are reassigned, we manually collect 99 recent bug reports that …
Barometric Phone Sensors: More Hype Than Hope!, Kartik Muralidharan, Azeem Javed Khan, Archan Misra, Rajesh Krishna Balan, Sharad Agarwal
Barometric Phone Sensors: More Hype Than Hope!, Kartik Muralidharan, Azeem Javed Khan, Archan Misra, Rajesh Krishna Balan, Sharad Agarwal
Research Collection School Of Computing and Information Systems
The inclusion of the barometer sensor in smartphones signaled an opportunity for aiding indoor localization efforts. In this paper, we therefore investigate a possible use of the barometer sensor for detecting vertically oriented activities. We start by showing the accuracies of various commodity measurement devices and the challenges they bring forth. We then show how to use the barometer values to build a predictor that can detect floor changes and the mode (elevator, escalator, or stairs) used to change floors with nearly 100% accuracy. We validate these properties with data collected using 3 different measurement devices from 7 different buildings. …
Libol: A Library For Online Learning Algorithms, Steven C. H. Hoi, Jialei Wang, Peilin Zhao
Libol: A Library For Online Learning Algorithms, Steven C. H. Hoi, Jialei Wang, Peilin Zhao
Research Collection School Of Computing and Information Systems
LIBOL is an open-source library for large-scale online learning, which consists of a large family of efficient and scalable state-of-the-art online learning algorithms for large- scale online classification tasks. We have offered easy-to-use command-line tools and examples for users and developers, and also have made comprehensive documents available for both beginners and advanced users. LIBOL is not only a machine learning toolbox, but also a comprehensive experimental platform for conducting online learning research.
Parameter Synthesis For Hierarchical Concurrent Real-Time Systems, Étienne André, Yang Liu, Jun Sun, Jin Song Dong
Parameter Synthesis For Hierarchical Concurrent Real-Time Systems, Étienne André, Yang Liu, Jun Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
Modeling and verifying complex real-time systems, involving timing delays, are notoriously difficult problems. Checking the correctness of a system for one particular value for each delay does not give any information for other values. It is thus interesting to reason parametrically, by considering that the delays are parameters (unknown constants) and synthesizing a constraint guaranteeing a correct behavior. We present here Parametric Stateful Timed Communicating Sequential Processes, a language capable of specifying and verifying parametric hierarchical real-time systems with complex data structures. Although we prove that the synthesis is undecidable in general, we present several semi-algorithms for efficient parameter synthesis, …
Towards Verification Of Computation Orchestration, Jin Song Dong, Yang Liu, Jun Sun, Xian Zhang
Towards Verification Of Computation Orchestration, Jin Song Dong, Yang Liu, Jun Sun, Xian Zhang
Research Collection School Of Computing and Information Systems
Recently, a promising programming model called Orc has been proposed to support a structured way of orchestrating distributed Web Services. Orc is intuitive because it offers concise constructors to manage concurrent communication, time-outs, priorities, failure of Web Services or communication and so forth. The semantics of Orc is precisely defined. However, there is no automatic verification tool available to verify critical properties against Orc programs. Our goal is to verify the orchestration programs (written in Orc language) which invoke web services to achieve certain goals. To investigate this problem and build useful tools, we explore in two directions. Firstly, we …
Model Checking Approach To Automated Planning, Yi Li, Jin Song Dong, Jing Sun, Yang Liu, Jun Sun
Model Checking Approach To Automated Planning, Yi Li, Jin Song Dong, Jing Sun, Yang Liu, Jun Sun
Research Collection School Of Computing and Information Systems
Model checking provides a way to automatically explore the state space of a finite state system based on desired properties, whereas planning is to produce a sequence of actions that leads from the initial state to the target goal states. Previous research in this field proposed a number of approaches for connecting model checking with planning problem solving. In this paper, we investigate the feasibility of using an established model checking framework, Process Analysis Toolkit (PAT), as a planning solution provider for upper layer applications. To achieve this, we first carry out a number of experiments on different model checking …