Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 9 of 9
Full-Text Articles in Entire DC Network
O2o Service Composition With Social Collaboration, Wenyi Qian, Xin Peng, Jun Sun, Yijun Yu, Bashar Nuseibeh, Wenyun Zhao
O2o Service Composition With Social Collaboration, Wenyi Qian, Xin Peng, Jun Sun, Yijun Yu, Bashar Nuseibeh, Wenyun Zhao
Research Collection School Of Computing and Information Systems
In Online-to-Offline (O2O) commerce, customer services may need to be composed from online and offline services. Such composition is challenging, as it requires effective selection of appropriate services that, in turn, support optimal combination of both online and offline services. In this paper, we address this challenge by proposing an approach to O2O service composition which combines offline route planning and social collaboration to optimize service selection. We frame general O2O service composition problems using timed automata and propose an optimization procedure that incorporates: (1) a Markov Chain Monte Carlo (MCMC) algorithm to stochastically select a concrete composite service, and …
Interpolation Guided Compositional Verification, Shang-Wei Lin, Jun Sun, Truong Khanh Nguyen, Yang Liu, Jin Song Dong
Interpolation Guided Compositional Verification, Shang-Wei Lin, Jun Sun, Truong Khanh Nguyen, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Model checking suffers from the state space explosion problem. Compositional verification techniques such as assume-guarantee reasoning (AGR) have been proposed to alleviate the problem. However, there are at least three challenges in applying AGR. Firstly, given a system M1 M2, how do we automatically construct and refine (in the presence of spurious counterexamples) an assumption A2, which must be an abstraction of M2? Previous approaches suggest to incrementally learn and modify the assumption through multiple invocations of a model checker, which could be often time consuming. Secondly, how do we keep the state space small when checking M1 A2 |= …
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, …
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.
Usmmc: A Self-Contained Model Checker For Uml State Machines, Shuang Liu, Yang Liu, Jun Sun, Manchun Zheng, Bimlesh Wadhwa, Jin Song Dong
Usmmc: A Self-Contained Model Checker For Uml State Machines, Shuang Liu, Yang Liu, Jun Sun, Manchun Zheng, Bimlesh Wadhwa, Jin Song Dong
Research Collection School Of Computing and Information Systems
UML diagrams are gaining increasing usage in Object-Oriented system designs. UML state machines are specifically used in modeling dynamic behaviors of classes. It has been widely agreed that verification of system designs at an early stage will dramatically reduce the development cost. Tool support for verification UML designs can also encourage consistent usage of UML diagrams throughout the software development procedure. In this work, we present a tool, named USMMC, which turns model checking of UML state machines into practice. USMMC is a self-contained toolkit, which provides editing, interactive simulation as well as powerful model checking support for UML state …
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 …
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 hence interesting to reason parametrically, by considering that the delays are parameters (unknown constants) and synthesize a constraint guaranteeing a correct behavior. We present here Parametric Stateful Timed CSP, a language capable of specifying hierarchical real-time systems with complex data structures. Although we prove that the synthesis is undecidable in general, we present an algorithm for efficient parameter synthesis that behaves well in practice.
Formal Modeling And Validation Of Stateflow Diagrams, Chunqing Chen, Jun Sun, Yang Liu, Jin Song Dong, Manchun Zheng
Formal Modeling And Validation Of Stateflow Diagrams, Chunqing Chen, Jun Sun, Yang Liu, Jin Song Dong, Manchun Zheng
Research Collection School Of Computing and Information Systems
Stateflow is an industrial tool for modeling and simulating control systems in model-based development. In this paper, we present our latest work on automatic verification of Stateflow using model-checking techniques. We propose an approach to systematically translate Stateflow diagrams to a formal modeling language called CSP# by precisely following Stateflow’s execution semantics, which is described by examples. A translator is developed inside the Process Analysis Toolkit (PAT) model checker to automate this process with the support of various Stateflow advanced modeling features. Formal analysis can be conducted on the transformed CSP# with PAT’s simulation and model-checking power. Using our approach, …
Model Checking In The Absence Of Code, Model And Properties, David Lo, Siau-Cheng Khoo
Model Checking In The Absence Of Code, Model And Properties, David Lo, Siau-Cheng Khoo
Research Collection School Of Computing and Information Systems
Model checking is a major approach in ensuring software correctness. It verifies a model converted from code against some formal properties. However, difficulties and programmers ’ reluctance to formalize formal properties have been some hurdles to its widespread industrial adoption. Also, with the advent of commercial off-the-shelf (COTS) components provided by third party vendors, model checking is further challenged as often only a binary version of the code is provided by vendors. Interestingly, latest instrumentation tools like PIN and Valgrind have enable execution traces to be collected dynamically from a running program. In this preliminary study, we investigate what can …