Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Keyword
-
- Model Check (2)
- Model checking (2)
- Active learning (1)
- Adaptive reuse (1)
- Automatic assume-guarantee reasoning (1)
-
- Binary quadratic programming (1)
- Biological identification (1)
- Blended learning (1)
- Computer programming (1)
- Constraint logic programming (1)
- Convex Hull (1)
- DRL (1)
- Deterministic Finite Automaton (1)
- Discrete Time Markov Chain (1)
- DocBook (1)
- DocLine (1)
- Documentation reuse (1)
- Empirical study (1)
- Error-correcting codes (1)
- Event Trace (1)
- Flipped classroom (1)
- Gabor wavelet (1)
- Identification (1)
- Identity based cryptography (1)
- Input validation and sanitization (1)
- Markov Decision Process (1)
- Near-duplicate retrieval (1)
- Orc (1)
- Palm vein (1)
- Parametric timed verification (1)
Articles 1 - 14 of 14
Full-Text Articles in Physical Sciences and Mathematics
Web Application Vulnerability Prediction Using Hybrid Program Analysis And Machine Learning, Lwin Khin Shar, Lionel Briand, Hee Beng Kuan Tan
Web Application Vulnerability Prediction Using Hybrid Program Analysis And Machine Learning, Lwin Khin Shar, Lionel Briand, Hee Beng Kuan Tan
Research Collection School Of Computing and Information Systems
Due to limited time and resources, web software engineers need support in identifying vulnerable code. A practical approach to predicting vulnerable code would enable them to prioritize security auditing efforts. In this paper, we propose using a set of hybrid (staticþdynamic) code attributes that characterize input validation and input sanitization code patterns and are expected to be significant indicators of web application vulnerabilities. Because static and dynamic program analyses complement each other, both techniques are used to extract the proposed attributes in an accurate and scalable way. Current vulnerability prediction techniques rely on the availability of data labeled with vulnerability …
Event Analytics, Jin Song Dong, Jun Sun, Yang Liu, Yuan-Fang Li
Event Analytics, Jin Song Dong, Jun Sun, Yang Liu, Yuan-Fang Li
Research Collection School Of Computing and Information Systems
The process analysis toolkit (PAT) integrates the expressiveness of state, event, time, and probability-based languages with the power of model checking. PAT is a self-contained reasoning system for system specification, simulation, and verification. PAT currently supports a wide range of 12 different expressive modeling languages with many application domains and has attracted thousands of registered users from hundreds of organizations. In this invited talk, we will present the PAT system and its vision on “Event Analytics” (EA) which is beyond “Data Analytics”. The EA research is based on applying model checking to event planning, scheduling, prediction, strategy analysis and decision …
A Palm Vein Identification System Based On Gabor Wavelet Features, Ran Wang, Guoyou Wang, Zhong Chen, Zhigang Zeng, Yong Wang
A Palm Vein Identification System Based On Gabor Wavelet Features, Ran Wang, Guoyou Wang, Zhong Chen, Zhigang Zeng, Yong Wang
Research Collection School Of Computing and Information Systems
As a new and promising biometric feature, thermal palm vein pattern has drawn lots of attention in research and application areas. Many algorithms have been proposed for authentication since palm vein has special characteristics, such as liveness detection and hard to forgery. However, the detection accuracy of palm vein quite depends on the preprocessing and feature representation, which is supposed to be translation and rotation invariant to some extent. In this paper, we proposed an effective method for palm vein identification based on Gabor wavelet features which contains five steps: image acquisition, ROI detection, image preprocessing, features extraction, and matching. …
Diamonds Are A Girl's Best Friend: Partial Order Reduction For Timed Automata With Abstractions, Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, Jun Sun
Diamonds Are A Girl's Best Friend: Partial Order Reduction For Timed Automata With Abstractions, Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, Jun Sun
Research Collection School Of Computing and Information Systems
A major obstacle for using partial order reduction in the context of real time verification is that the presence of clocks and clock constraints breaks the usual diamond structure of otherwise independent transitions. This is especially true when information of the relative values of clocks is preserved in the form of diagonal constraints. However, when diagonal constraints are relaxed by a suitable abstraction, some diamond structure is re-introduced in the zone graph. In this article, we introduce a variant of the stubborn set method for reducing an abstracted zone graph. Our method works with all abstractions, but especially targets situations …
Scc-Based Improved Reachability Analysis For Markov Decision Processes, Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong
Scc-Based Improved Reachability Analysis For Markov Decision Processes, Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Markov decision processes (MDPs) are extensively used to model systems with both probabilistic and nondeterministic behavior. The problem of calculating the probability of reaching certain system states (hereafter reachability analysis) is central to the MDP-based system analysis. It is known that existing approaches on reachability analysis for MDPs are often inefficient when a given MDP contains a large number of states and loops, especially with the existence of multiple probability distributions. In this work, we propose a method to eliminate strongly connected components (SCCs) in an MDP using a divide-and-conquer algorithm, and actively remove redundant probability distributions in the MDP …
Teaching Tip: The Flipped Classroom, Heng Ngee Mok
Teaching Tip: The Flipped Classroom, Heng Ngee Mok
Research Collection School Of Computing and Information Systems
The flipped classroom has been gaining popularity in recent years. In theory, flipping the classroom appears sound: passive learning activities such as unidirectional lectures are pushed to outside class hours in the form of videos, and precious class time is spent on active learning activities. Yet the courses for information systems (IS) undergraduates at the university that the author is teaching at are still conducted in the traditional lecture-in-class, homework-after-class style. In order to increase students’ engagement with the course content and to improve their experience with the course, the author implemented a trial of the flipped classroom model 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 …
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 …
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 …
Learning Assumptions For Compositional Verification Of Timed Systems, Shang-Wei Lin Lin, Yang Liu, Jun Sun, Jun Sun
Learning Assumptions For Compositional Verification Of Timed Systems, Shang-Wei Lin Lin, Yang Liu, Jun Sun, Jun Sun
Research Collection School Of Computing and Information Systems
Compositional techniques such as assume-guarantee reasoning (AGR) can help to alleviate the state space explosion problem associated with model checking. However, compositional verification is difficult to be automated, especially for timed systems, because constructing appropriate assumptions for AGR usually requires human creativity and experience. To automate compositional verification of timed systems, we propose a compositional verification framework using a learning algorithm for automatic construction of timed assumptions for AGR. We prove the correctness and termination of the proposed learning-based framework, and experimental results show that our method performs significantly better than traditional monolithic timed model checking.
An Approach For Clone Detection In Documentation Reuse, Dmitry V. Lutsiv, Dmitry Koznov, Hamid A. Basit, Eng Lieh Ouh, Mikhail N. Smirnov, Konstantin Y. Romanovsky
An Approach For Clone Detection In Documentation Reuse, Dmitry V. Lutsiv, Dmitry Koznov, Hamid A. Basit, Eng Lieh Ouh, Mikhail N. Smirnov, Konstantin Y. Romanovsky
Research Collection School Of Computing and Information Systems
The paper focuses on the searching method for repetitions in DocBook/DRL or plain text documents. An algorithm has been designed based on software clone detection. The algorithm supports filtering results: clones are rejected if clone length in the group is less than 5 symbols, intersection of clone groups is eliminated, meaningfulness clones are removed, the groups containing clones consisting only of XML are eliminated. Remaining search is supported: found clones are extracted from the documentation, and clone search is repeated. One step is proved to be enough. Adaptive reuse technique of Paul Bassett – Stan Jarzabek has been implemented. A …
Complexity Of The Soundness Problem Of Workflow Nets, Guan Jun Liu, Jun Sun, Yang Liu, Jin Song Dong
Complexity Of The Soundness Problem Of Workflow Nets, Guan Jun Liu, Jun Sun, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Classical workflow nets (WF-nets for short) are an important subclass of Petri nets that are widely used to model and analyze workflow systems. Soundness is a crucial property of workflow systems and guarantees that these systems are deadlock-free and bounded. Aalst et al. proved that the soundness problem is decidable for WF-nets and can be polynomially solvable for free-choice WF-nets. This paper proves that the soundness problem is PSPACE-hard for WF-nets. Furthermore, it is proven that the soundness problem is PSPACE-complete for bounded WF-nets. Based on the above conclusion, it is derived that the soundness problem is also PSPACE-complete for …