Open Access. Powered by Scholars. Published by Universities.®
- Discipline
- Institution
- Publication Year
Articles 1 - 18 of 18
Full-Text Articles in Entire DC Network
Formal Modeling And Verification Of A Blockchain-Based Crowdsourcing Consensus Protocol, Hamra Afzaal, Muhammad Imran, Muhammad Umar Janjua, Sarada Prasad Gochhayat
Formal Modeling And Verification Of A Blockchain-Based Crowdsourcing Consensus Protocol, Hamra Afzaal, Muhammad Imran, Muhammad Umar Janjua, Sarada Prasad Gochhayat
VMASC Publications
Crowdsourcing is an effective technique that allows humans to solve complex problems that are hard to accomplish by automated tools. Some significant challenges in crowdsourcing systems include avoiding security attacks, effective trust management, and ensuring the system’s correctness. Blockchain is a promising technology that can be efficiently exploited to address security and trust issues. The consensus protocol is a core component of a blockchain network through which all the blockchain peers achieve an agreement about the state of the distributed ledger. Therefore, its security, trustworthiness, and correctness have vital importance. This work proposes a Secure and Trustworthy Blockchain-based Crowdsourcing (STBC) …
A Method And Tool For Finding Concurrency Bugs Involving Multiple Variables With Application To Modern Distributed Systems, Zhuo Sun
FIU Electronic Theses and Dissertations
Concurrency bugs are extremely hard to detect due to huge interleaving space. They are happening in the real world more often because of the prevalence of multi-threaded programs taking advantage of multi-core hardware, and microservice based distributed systems moving more and more applications to the cloud. As the most common non-deadlock concurrency bugs, atomicity violations are studied in many recent works, however, those methods are applicable only to single-variable atomicity violation, and don't consider the specific challenge in distributed systems that have both pessimistic and optimistic concurrency control. This dissertation presents a tool using model checking to predict atomicity violation …
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 |= …
Compositional Model Checking Of Concurrent Systems, Hao Zheng, Zhen Zhang, Chris J. Myers, Emmanuel Rodriguez, Yingying Zhang
Compositional Model Checking Of Concurrent Systems, Hao Zheng, Zhen Zhang, Chris J. Myers, Emmanuel Rodriguez, Yingying Zhang
Electrical and Computer Engineering Faculty Publications
This paper presents a compositional framework to address the state explosion problem in model checking of concurrent systems. This framework takes as input a system model described as a network of communicating components in a high-level description language, finds the local state transition models for each individual component where local properties can be verified, and then iteratively reduces and composes the component state transition models to form a reduced global model for the entire system where global safety properties can be verified. The state space reductions used in this framework result in a reduced model that contains the exact same …
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 …
Methods For Modeling And Analyzing Concurrent Software, Reng Zeng
Methods For Modeling And Analyzing Concurrent Software, Reng Zeng
FIU Electronic Theses and Dissertations
Concurrent software executes multiple threads or processes to achieve high performance. However, concurrency results in a huge number of different system behaviors that are difficult to test and verify. The aim of this dissertation is to develop new methods and tools for modeling and analyzing concurrent software systems at design and code levels. This dissertation consists of several related results. First, a formal model of Mondex, an electronic purse system, is built using Petri nets from user requirements, which is formally verified using model checking. Second, Petri nets models are automatically mined from the event traces generated from scientific workflows. …
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 …
A Novel Framework For Model Checking Udp Network Interactions, Billy Rathje
A Novel Framework For Model Checking Udp Network Interactions, Billy Rathje
Summer Research
This poster presents the first Java Pathfinder extension to model realistic User Datagram Protocol (UDP) networking communications, which is used to verify a UDP network software simulator, RF. Java Pathfinder is a model checking software system developed by NASA and used frequently for verifying that concurrent software systems avoid deadlock states and other errors. It does not natively support network modeling. NetIOCache is a Java Pathfinder extension for verifying TCP/IP networks, but no similar UDP extensions currently exist. NetStub, a Java Pathfinder extension, can simulate UDP behavior as a collection of threads, but it does not simulate important and common …
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, …
Test Case Generation Using Model Checking For Software Components Deployed Into New Environments, Tonglaga Bao, Michael D. Jones
Test Case Generation Using Model Checking For Software Components Deployed Into New Environments, Tonglaga Bao, Michael D. Jones
Faculty Publications
In this paper, we show how to generate test cases for a component deployed into a new software environment. This problem is important for software engineers who need to deploy a component into a new environment. Most existing model based testing approaches generate models from high level specifications. This leaves a semantic gap between the high level specification and the actual implementation. Furthermore, the high level specification often needs to be manually translated into a model, which is a time consuming and error prone process. We propose generating the model automatically by abstracting the source code of the component using …
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 …
A Context-Sensitive Structural Heuristic For Guided Search Model Checking, Eric G. Mercer, Neha Rungta
A Context-Sensitive Structural Heuristic For Guided Search Model Checking, Eric G. Mercer, Neha Rungta
Faculty Publications
Software verification using model checking often translates programs into corresponding transition systems that model the program behavior. As software systems continue to grow in complexity and size, exhaustively checking a property on a transition graph becomes difficult. The goal of guided search heuristics in model checking is to find a counterexample to the property being verified as quickly as possible in the transition graph. The FSM distance heuristic builds an interprocedural control flow graph of the program to estimate distance to a possible error state. It ignores calling context and underestimates the true distance to the error.
Model Checking For E-Business Control And Assurance, Bonnie B. Anderson, James V. Hansen, Paul B. Lowry, Scott L. Summers
Model Checking For E-Business Control And Assurance, Bonnie B. Anderson, James V. Hansen, Paul B. Lowry, Scott L. Summers
Faculty Publications
Model checking is a promising technique for the verification of complex software systems. As the use of the Internet for conducting e-business extends the reach of many organizations, well-designed software becomes the foundation of reliable implementation of e-business processes. These distributed, electronic methods of conducting transactions place reliance on the control structures embedded in the transaction processes. Deficiencies in control structures of processes that support e-business can lead to loss of physical assets, digital assets, money, and consumer confidence. Yet, assessing the reliability of e-business processes is complex and time-consuming. This paper explicates how model-checking technology can aid in the …
Accelerated Hazards Model: Method, Theory And Applications, Ying Qing Chen, Nicholas P. Jewell, Jingrong Yang
Accelerated Hazards Model: Method, Theory And Applications, Ying Qing Chen, Nicholas P. Jewell, Jingrong Yang
U.C. Berkeley Division of Biostatistics Working Paper Series
In an accelerated hazards model, the hazard functions of a failure time are related through the time scale-change, which is often a function of covariates and associated parameters. When the hazard functions have special properties, such as monotonicity in time, the parameters may be clinically meaningful in measuring a treatment effect. This paper reviews methodological and theoretical development of this model. Applications of the accelerated hazards model including sample size calculation in clinical trials, are also explored.