Open Access. Powered by Scholars. Published by Universities.®

Programming Languages and Compilers Commons™

Open Access. Powered by Scholars. Published by Universities.®

Singapore Management University

Discipline
Keyword
Publication Year
Publication
Publication Type

Articles 331 - 360 of 413

Full-Text Articles in Programming Languages and Compilers

Probabilistic Model Checking Multi-Agent Behaviors In Dispersion Games Using Counter Abstraction, Jianye Hao, Songzheng Song, Yang Liu, Jun Sun, Lin Gui, Jin Song Dong, Ho-Fung Leung Jul 2012

Probabilistic Model Checking Multi-Agent Behaviors In Dispersion Games Using Counter Abstraction, Jianye Hao, Songzheng Song, Yang Liu, Jun Sun, Lin Gui, Jin Song Dong, Ho-Fung Leung

Research Collection School Of Computing and Information Systems

Accurate analysis of the stochastic dynamics of multi-agent system is important but challenging. Probabilistic model checking, a formal technique for analysing a system which exhibits stochastic behaviors, can be a natural solution to analyse multi-agent systems. In this paper, we investigate this problem in the context of dispersion games focusing on two strategies: basic simple strategy (BSS) and extended simple strategies (ESS). We model the system using discrete-time Markov chain (DTMC) and reduce the state space of the models by applying counter abstraction technique. Two important properties of the system are considered: convergence and convergence rate. We show that these …

Go to article

A Model Checker For Hierarchical Probabilistic Real-Time Systems, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong Jul 2012

A Model Checker For Hierarchical Probabilistic Real-Time Systems, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong

Research Collection School Of Computing and Information Systems

Real-life systems are usually hard to control, due to their complicated structures, quantitative time factors and even stochastic behaviors. In this work, we present a model checker to analyze hierarchical probabilistic real-time systems. A modeling language called PRTS is used to specify such systems, and automatic zone-abstraction approach, which is probability preserving, is used to generate finite state MDP. We have implemented PRTS in model checking framework PAT so that friendly user interface can be used to edit, simulate and verify PRTS models. Some experiments are conducted to show our tool’s efficiency.

Go to article

Translating Pddl Into Csp# - The Pat Approach, Yi Li, Jing Sun, Jin Song Dong, Yang Liu, Jun Sun Jul 2012

Translating Pddl Into Csp# - The Pat Approach, Yi Li, Jing Sun, Jin Song Dong, Yang Liu, Jun Sun

Research Collection School Of Computing and Information Systems

Model checking provides a way to automatically verify hardware and software systems, whereas the goal of planning is to produce a sequence of actions that leads from the initial state to the desired goal state. Recently research indicates that there is a strong connection between model checking and planning problem solving. In this paper, we investigate the feasibility of using a newly developed model checking framework, Process Analysis Toolkit (PAT), to serve as a planning solution provider for upper layer applications. We first carried out a number of experiments on different planning tools in order to compare their performance and …

Go to article

Aligning Images In The Wild, Wen-Yan Lin, Linlin Liu, Yasuyuki Matsushita, Kok-Lim Low, Siying Liu Jun 2012

Aligning Images In The Wild, Wen-Yan Lin, Linlin Liu, Yasuyuki Matsushita, Kok-Lim Low, Siying Liu

Research Collection School Of Computing and Information Systems

Aligning image pairs with significant appearance change is a long standing computer vision challenge. Much of this problem stems from the local patch descriptors’ instability to appearance variation. In this paper we suggest this instability is due less to descriptor corruption and more the difficulty in utilizing local information to canonically define the orientation (scale and rotation) at which a patch’s descriptor should be computed. We address this issue by jointly estimating correspondence and relative patch orientation, within a hierarchical algorithm that utilizes a smoothly varying parameterization of geometric transformations. By collectively estimating the correspondence and orientation of all the …

Go to article

Complexity Of The Soundness Problem Of Bounded Workflow Nets, Guan Jun Liu, Jun Sun, Yang Liu, Jin Song Dong Jun 2012

Complexity Of The Soundness Problem Of Bounded 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) are an important class of Petri nets that are widely used to model and analyze workflow systems. Soundness is a crucial property that guarantees these systems are deadlock-free and bounded. Aalst et al. proved that the soundness problem is decidable, and proposed (but not proved) that the soundness problem is EXPSPACE-hard. In this paper, we show that the satisfiability problem of Boolean expression is polynomial time reducible to the liveness problem of bounded WF-nets, and soundness and liveness are equivalent for bounded WF-nets. As a result, the soundness problem of bounded WF-nets is co-NP-hard.Workflow nets with …

Go to article

Programming In A Socially Networked World: The Evolution Of The Social Programmer, Christoph Treude, Fernando Figueira Filho, Brendan Cleary, Margaret-Anne Storey Feb 2012

Programming In A Socially Networked World: The Evolution Of The Social Programmer, Christoph Treude, Fernando Figueira Filho, Brendan Cleary, Margaret-Anne Storey

Research Collection School Of Computing and Information Systems

Social media has changed how software developers collaborate, how they coordinate their work, and where they find information. Social media sites, such as the Question and Answer (Q&A) portal Stack Overflow, fill archives with millions of entries that contribute to what we know about software development, covering a wide range of topics. For today’s software developers, reusable code snippets, introductory usage examples, and pertinent libraries are often just a web search away. In this position paper, we discuss the opportunities and challenges for software developers that rely on web content curated by the crowd, and we envision the future of …

Go to article

Formal Modeling And Validation Of Stateflow Diagrams, Chunqing Chen, Jun Sun, Yang Liu, Jin Song Dong, Manchun Zheng Jan 2012

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, …

Go to article

A Hybridized Lagrangian Relaxation And Simulated Annealing Method For The Course Timetabling Problem, Aldy Gunawan, Kim Leng Poh Jan 2012

A Hybridized Lagrangian Relaxation And Simulated Annealing Method For The Course Timetabling Problem, Aldy Gunawan, Kim Leng Poh

Research Collection School Of Computing and Information Systems

This paper describes a timetabling problem at universities, where a master course timetable is given extrinsically and conflicts due to students' course enrollment do not need to be considered. A solver for the problem, which integrates both teacher assignment and course scheduling, is described. An initial solution is obtained by a mathematical programming approach based on Lagrangian relaxation. This solution is further improved by a simulated annealing algorithm. The proposed method has been tested on instances from a university in Indonesia, as well as on several randomly generated datasets, and the corresponding computational results are reported.

Go to article

An Efficient Algorithm For Learning Event-Recording Automata, Shang-Wei Lin, Étienne André, Jin Song Dong, Jun Sun, Yang Liu Oct 2011

An Efficient Algorithm For Learning Event-Recording Automata, Shang-Wei Lin, Étienne André, Jin Song Dong, Jun Sun, Yang Liu

Research Collection School Of Computing and Information Systems

In inference of untimed regular languages, given an unknown language to be inferred, an automaton is constructed to accept the unknown language from answers to a set of membership queries each of which asks whether a string is contained in the unknown language. One of the most well-known regular inference algorithms is the L* algorithm, proposed by Angluin in 1987, which can learn a minimal deterministic finite automaton (DFA) to accept the unknown language. In this work, we propose an efficient polynomial time learning algorithm, TL*, for timed regular language accepted by event-recording automata. Given an unknown timed regular language, …

Go to article

Verification Of Orchestration Systems Using Compositional Partial Order Reduction, Tian Huat Tan, Yang Liu, Jun Sun, Jin Song Dong Oct 2011

Verification Of Orchestration Systems Using Compositional Partial Order Reduction, Tian Huat Tan, Yang Liu, Jun Sun, Jin Song Dong

Research Collection School Of Computing and Information Systems

Orc is a computation orchestration language which is designed to specify computational services, such as distributed communication and data manipulation, in a concise and elegant way. Four concurrency primitives allow programmers to orchestrate site calls to achieve a goal, while managing timeouts, priorities, and failures. To guarantee the correctness of Orc model, effective verification support is desirable. Orc has a highly concurrent semantics which introduces the problem of state-explosion to search-based verification methods like model checking. In this paper, we present a new method, called Compositional Partial Order Reduction (CPOR), which aims to provide greater state-space reduction than classic partial …

Go to article

Prts: An Approach For Model Checking Probabilistic Real-Time Hierarchical Systems, Jun Sun, Yang Liu, Songzheng Song, Jin Song Dong, Xiaohong Li Oct 2011

Prts: An Approach For Model Checking Probabilistic Real-Time Hierarchical Systems, Jun Sun, Yang Liu, Songzheng Song, Jin Song Dong, Xiaohong Li

Research Collection School Of Computing and Information Systems

Model Checking real-life systems is always difficult since such systems usually have quantitative timing factors and work in unreliable environment. The combination of real-time and probability in hierarchical systems presents a unique challenge to system modeling and analysis. In this work, we develop an automated approach for verifying probabilistic, real-time, hierarchical systems. Firstly, a modeling language called PRTS is defined, which combines data structures, real-time and probability. Next, a zone-based method is used to build a finite-state abstraction of PRTS models so that probabilistic model checking could be used to calculate the probability of a system satisfying certain property. We …

Go to article

Towards A Model Checker For Nesc And Wireless Sensor Networks, Manchun Zheng, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu Oct 2011

Towards A Model Checker For Nesc And Wireless Sensor Networks, Manchun Zheng, Jun Sun, Yang Liu, Jin Song Dong, Yu Gu

Research Collection School Of Computing and Information Systems

Wireless sensor networks (WSNs) are expected to run unattendedly for critical tasks. To guarantee the correctness of WSNs is important, but highly nontrivial due to the distributed nature. In this work, we present an automatic approach to directly verify WSNs built with TinyOS applications implemented in the NesC language. To achieve this target, we firstly define a set of formal operational semantics for most of the NesC language structures for the first time. This allows us to capture the behaviors of sensors by labelled transition systems (LTSs), which are the underlying semantic models of NesC programs. Secondly, WSNs are modeled …

Go to article

Cooperative Reinforcement Learning In Topology-Based Multi-Agent Systems, Dan Xiao, Ah-Hwee Tan Oct 2011

Cooperative Reinforcement Learning In Topology-Based Multi-Agent Systems, Dan Xiao, Ah-Hwee Tan

Research Collection School Of Computing and Information Systems

Topology-based multi-agent systems (TMAS), wherein agents interact with one another according to their spatial relationship in a network, are well suited for problems with topological constraints. In a TMAS system, however, each agent may have a different state space, which can be rather large. Consequently, traditional approaches to multi-agent cooperative learning may not be able to scale up with the complexity of the network topology. In this paper, we propose a cooperative learning strategy, under which autonomous agents are assembled in a binary tree formation (BTF). By constraining the interaction between agents, we effectively unify the state space of individual …

Go to article

On Combining State Space Reductions With Global Fairness Assumptions, Shao Jie Zhang, Jun Sun, Jun Pang, Yang Liu, Jin Song Dong Jun 2011

On Combining State Space Reductions With Global Fairness Assumptions, Shao Jie Zhang, Jun Sun, Jun Pang, Yang Liu, Jin Song Dong

Research Collection School Of Computing and Information Systems

Model checking has established itself as an effective system analysis method, as it is capable of proving/dis-proving properties automatically. Its application to practical systems is however limited by state space explosion. Among effective state reduction techniques are symmetry reduction and partial order reduction. Global fairness often plays a vital role in designing self-stabilizing population protocols. It is known that combining fairness and symmetry reduction is nontrivial. In this work, we first show that global fairness, unlike weak/strong fairness, can be combined with symmetry reduction. We extend the PAT model checker with the technique and demonstrate its usability by verifying recently …

Go to article

Solving The Teacher Assignment Problem By Two Metaheuristics, Aldy Gunawan, Kien Ming Ng Jan 2011

Solving The Teacher Assignment Problem By Two Metaheuristics, Aldy Gunawan, Kien Ming Ng

Research Collection School Of Computing and Information Systems

The timetabling problem arising from a university in Indonesia is addressed in this paper.It involves the assignment of teachers to the courses and course sections. We formulate theproblem as a mathematical programming model. Two different algorithms, mainly basedon simulated annealing (SA) and tabu search (TS) algorithms, are proposed for solving theproblem. The proposed algorithms consist of two phases. The first phase involves allocatingthe teachers to the courses and determining the number of courses to be assigned to eachteacher. The second phase involves assigning the teachers to the course sections in order tobalance the teachers’ load. The performance of the proposed …

Go to article

Solving The Quadratic Assignment Problem By A Hybrid Algorithm, Aldy Gunawan, Kien Ming Ng, Kim Leng Poh Jan 2011

Solving The Quadratic Assignment Problem By A Hybrid Algorithm, Aldy Gunawan, Kien Ming Ng, Kim Leng Poh

Research Collection School Of Computing and Information Systems

This paper presents a hybrid algorithm to solve the Quadratic Assignment Problem (QAP). The proposed algorithminvolves using the Greedy Randomized Adaptive Search Procedure (GRASP) to obtain an initial solution, and then using a combinedSimulated Annealing (SA) and Tabu Search (TS) algorithm to improve the solution. Experimental results indicate that the hybridalgorithm is able to obtain good quality solutions for QAPLIB test problems within reasonable computation time.

Go to article

Model Checking Hierarchical Probabilistic Systems, Jun Sun, Songzheng Song, Yang Liu Nov 2010

Model Checking Hierarchical Probabilistic Systems, Jun Sun, Songzheng Song, Yang Liu

Research Collection School Of Computing and Information Systems

Probabilistic modeling is important for random distributed algorithms, bio-systems or decision processes. Probabilistic model checking is a systematic way of analyzing finite-state probabilistic models. Existing probabilistic model checkers have been designed for simple systems without hierarchy. In this paper, we extend the PAT toolkit to support probabilistic model checking of hierarchical complex systems. We propose to use PCSP#, a combination of Hoare’s CSP with data and probability, to model such systems. In addition to temporal logic, we allow complex safety properties to be specified by non-probabilistic PCSP# model. Validity of the properties (with probability) is established by refinement checking. Furthermore, …

Go to article

Model Checking A Model Checker: A Code Contract Combined Approach, Jun Sun, Yang Liu, Bin Cheng Nov 2010

Model Checking A Model Checker: A Code Contract Combined Approach, Jun Sun, Yang Liu, Bin Cheng

Research Collection School Of Computing and Information Systems

Model checkers, like any complex software, are subject to bugs. Unlike ordinary software, model checkers are often used to verify safety critical systems. Their correctness is thus vital. Verifying model checkers is extremely challenging because they are always complicated in logic and highly optimized. In this work, we propose a code contract combined approach for checking model checkers and apply it to a home-grown model checker PAT. In this approach, we firstly embed programming contracts (i.e., pre/post-conditions and invariants) into its source code, which can capture correctness of model checking algorithms, underlying data structures, consistency between different model checking parameters, …

Go to article

Developing Model Checkers Using Pat, Yang Liu, Jun Sun, Jin Song Dong Sep 2010

Developing Model Checkers Using Pat, Yang Liu, Jun Sun, Jin Song Dong

Research Collection School Of Computing and Information Systems

During the last two decades, model checking has emerged as an effective system analysis technique complementary to simulation and testing. Many model checking algorithms and state space reduction techniques have been proposed. Although it is desirable to have dedicated model checkers for every language (or application domain), implementing one with effective reduction techniques is rather challenging. In this work, we present a generic and extensible framework PAT, which facilitates users to build customized model checkers. PAT provides a library of state-of-art model checking algorithms as well as support for customizing language syntax, semantics, state space reduction techniques, graphic user interfaces, …

Go to article

A Verification System For Interval-Based Specification Languages, Chunqing Chen, Jin Song Dong, Jun Sun, Andrew P. Martin Apr 2010

A Verification System For Interval-Based Specification Languages, Chunqing Chen, Jin Song Dong, Jun Sun, Andrew P. Martin

Research Collection School Of Computing and Information Systems

Interval-based specification languages have been used to formally model and rigorously reason about real-time computing systems. This usually involves logical reasoning and mathematical computation with respect to continuous or discrete time. When these systems are complex, analyzing their models by hand becomes error-prone and difficult. In this article, we develop a verification system to facilitate the formal analysis of interval-based specification languages with machine-assisted proof support. The verification system is developed using a generic theorem prover, Prototype Verification System (PVS). Our system elaborately encodes a highly expressive set-based notation, Timed Interval Calculus (TIC), and can rigorously carry out the verification …

Go to article

Creating An Immersive Game World With Evolutionary Fuzzy Cognitive Maps, Yundong Cai, Ah-Hwee Tan, Zhiqi Shen, Boyang Li Mar 2010

Creating An Immersive Game World With Evolutionary Fuzzy Cognitive Maps, Yundong Cai, Ah-Hwee Tan, Zhiqi Shen, Boyang Li

Research Collection School Of Computing and Information Systems

An increasing number of serious games have been developed to enhance the user experiences in education and training. In order to bridge the gap of game experiences in the virtual environment and in the real life, it is crucial to generate believable characters and contexts in real-time. However, the variables to be simulated for a large-scale serious game are numerous. These variables are involved in complex causal relationships and their values change over time. In view that world modeling has not been well addressed with conventional models, this paper uses a computational model Evolutionary Fuzzy Cognitive Map (EFCM) to model …

Go to article

Scalable Multi-Core Model Checking Fairness Enhanced Systems, Yang Liu, Jun Sun, Jin Song Dong Dec 2009

Scalable Multi-Core Model Checking Fairness Enhanced Systems, Yang Liu, Jun Sun, Jin Song Dong

Research Collection School Of Computing and Information Systems

Rapid development in hardware industry has brought the prevalence of multi-core systems with shared-memory, which enabled the speedup of various tasks by using parallel algorithms. The Linear Temporal Logic (LTL) model checking problem is one of the difficult problems to be parallelized or scaled up to multi-core. In this work, we propose an on-the-fly parallel model checking algorithm based on the Tarjan’s strongly connected components (SCC) detection algorithm. The approach can be applied to general LTL model checking or with different fairness assumptions. Further, it is orthogonal to state space reduction techniques like partial order reduction. We enhance our PAT …

Go to article

Verifying Stateful Timed Csp Using Implicit Clocks And Zone Abstraction, Jun Sun, Yang Liu, Jin Song Dong, Xian Zhang Sep 2009

Verifying Stateful Timed Csp Using Implicit Clocks And Zone Abstraction, Jun Sun, Yang Liu, Jin Song Dong, Xian Zhang

Research Collection School Of Computing and Information Systems

In this work, we study model checking of compositional real-time systems. A system is modeled using mutable data variables as well as a compositional timed process. Instead of explicitly manipulating clock variables, a number of compositional timed behavioral patterns are used to capture quantitative timing requirements, e.g. delay, timeout, deadline, timed interrupt, etc. A fully automated abstraction technique is developed to build an abstract finite state machine from the model. The idea is to dynamically create/delete clocks, and maintain/solve a constraint on the clocks. The abstract machine weakly bi-simulates the model and, therefore, LTL model checking or trace-refinement checking are …

Go to article

Towards Expressive Specification And Efficient Model Checking, Jin Song Dong, Jun Sun Jul 2009

Towards Expressive Specification And Efficient Model Checking, Jin Song Dong, Jun Sun

Research Collection School Of Computing and Information Systems

System modeling is important and highly non-trivial. The choice of specification language is an important factor in the success of the entire development. The language should cover several facets of the requirements and the model should precisely capture (up to abstraction of irrelevant details) an existing system or a system to be built. The language should have a semantic model suitable to study the behaviors of the system and to establish the validity of desired properties. A formal model can be the basis for a variety of system development activities, e.g., system simulation, visualization, verification or prototype synthesis.

Go to article

Verification Of Population Ring Protocols In Pat, Yang Liu, Jun Pang, Jun Sun, Jianhua Zhao Jul 2009

Verification Of Population Ring Protocols In Pat, Yang Liu, Jun Pang, Jun Sun, Jianhua Zhao

Research Collection School Of Computing and Information Systems

The population protocol model has emerged as an elegant paradigm for describing mobile ad hoc networks, consisting of a number of nodes that interact with each other to carry out a computation. One essential property of self-stabilizing population protocols is that all nodes must eventually converge to the correct output value, with respect to all possible initial configurations. It has been shown that fairness constraints play a crucial role in designing population protocols. The Process Analysis Toolkit (PAT) has been developed to perform verifications under different fairness constraints efficiently. In particular, it can handle global fairness, which is required for …

Go to article

Integrating Specification And Programs For System Modeling And Verification, Jun Sun, Yang Liu, Jin Song Dong, Chunqing Chen Jul 2009

Integrating Specification And Programs For System Modeling And Verification, Jun Sun, Yang Liu, Jin Song Dong, Chunqing Chen

Research Collection School Of Computing and Information Systems

High level specification languages like CSP use mathematical objects as abstractions to represent systems and processes. System behaviors are described as process expressions combined with compositional operators, which are associated with elegant algebraic laws for system analysis. Nonetheless, modeling systems with non-trivial data and functional aspects using CSP remains difficult. In this work, we propose a modeling language named CSP# (short for communicating sequential programs) which integrates high-level modeling operators with low-level procedural codes, for the purpose of efficient mechanical system verification. We demonstrate that data operations can be modeled as terminating sequential programs, which can be composed using high-level …

Go to article

Fair Model Checking With Process Counter Abstraction, Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu, Jin Song Dong Jun 2009

Fair Model Checking With Process Counter Abstraction, Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu, Jin Song Dong

Research Collection School Of Computing and Information Systems

Parameterized systems are characterized by the presence of a large (or even unbounded) number of behaviorally similar processes, and they often appear in distributed/concurrent systems. A common state space abstraction for checking parameterized systems involves not keeping track of process identifiers by grouping behaviorally similar processes. Such an abstraction, while useful, conflicts with the notion of fairness. Because process identifiers are lost in the abstraction, it is difficult to ensure fairness (in terms of progress in executions) among the processes. In this work, we study the problem of fair model checking with process counter abstraction. Even without maintaining the process …

Go to article

Model Checking Linearizability Via Refinement, Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun Jun 2009

Model Checking Linearizability Via Refinement, Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun

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 be serializable, and 2) the serialized executions be correct with respect to the sequential semantics. This paper describes a new method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. Our method avoids the often difficult task of determining linearization points in implementations, but can also take advantage of linearization points if they are given. The method exploits model checking of finite state systems specified as concurrent …

Go to article

A Formal Framework For Modeling And Validating Simulink Diagrams, Chunqing Chen, Jin Song Dong, Jun Sun May 2009

A Formal Framework For Modeling And Validating Simulink Diagrams, Chunqing Chen, Jin Song Dong, Jun Sun

Research Collection School Of Computing and Information Systems

Simulink has been widely used in industry to model and simulate embedded systems. With the increasing usage of embedded systems in real-time safety-critical situations, Simulink becomes deficient to analyze (timing) requirements with high-level assurance. In this article, we apply Timed Interval Calculus (TIC), a realtime specification language, to complement Simulink with TIC formal verification capability. We elaborately construct TIC library functions to model Simulink library blocks which are used to compose Simulink diagrams. Next, Simulink diagrams are automatically transformed into TIC models which preserve functional and timing aspects. Important requirements such as timing bounded liveness can be precisely specified in …

Go to article

Pat: Towards Flexible Verification Under Fairness, Jun Sun, Yang Liu, Jin Song Dong, Jun Pang Feb 2009

Pat: Towards Flexible Verification Under Fairness, Jun Sun, Yang Liu, Jin Song Dong, Jun Pang

Research Collection School Of Computing and Information Systems

Recent development on distributed systems has shown that a variety of fairness constraints (some of which are only recently defined) play vital roles in designing self-stabilizing population protocols. Current practice of system analysis is, however, deficient under fairness. In this work, we present PAT, a toolkit for flexible and efficient system analysis under fairness. A unified algorithm is proposed to model check systems with a variety of fairness effectively in two different settings. Empirical evaluation shows that PAT complements existing model checkers in terms of fairness. We report that previously unknown bugs have been revealed using PAT against systems functioning …

Go to article

First Prev Next Last