"State Coverage Metrics for Specification-Based Testing with Buchi Automata". Li Tan. In Proceedings of the 5th International Conference on Tests and Proofs. Zurich, Switzerland. In the Lecture Notes in Computer Science. Springer-Verlag. June 30-July 01, 2011.
Buchi automata have been widely used for specifying linear temporal properties of reactive systems and they are also instrumental for designing efficient model-checking algorithms. In this paper we extend specification-based testing to Buchi automata. A key question in specification-based testing is how to measure the quality (relevancy) of test cases with respect to system specification. We propose two state coverage metrics for measuring how well a test suite covers a Buchi-automaton-based requirement. We also develop test generation algorithms that use counter-example generation capability of an off-the-shelf model checker to generate test cases for the coverage criteria inferred by these metrics. In our experiment we demonstrate the feasibility and performance of the coverage criteria and test generation algorithms for these criteria. In [TSL04] we proposed testing coverage metrics and criteria for properties in Linear Temporal Logic (LTL) and referred to the new approach as property-coverage testing. This research shares the same motivation as in [TSL04] and it extends property-coverage testing to specifications in Buchi automata. Since automaton minimization techniques can be used to reduce the structural diversity of semantically equivalent Buchi automata, we argue that a coverage metric based on \buchi\ automata is less susceptible to syntactic changes of a property than a LTL-based coverage metric, and hence the proposed coverage metrics measure the relevancy of a test suite to the semantics of a linear temporal property. We also discuss an algorithm for refining a Buchi-automaton-based requirement based on its strong state coverage metric. Our experiment demonstrates the feasibility and performance of our coverage criteria and test generation algorithms.
"An Adaptive N-variant Software Architecture for Multi-Core Platforms: Models and Performance Analysis". Li Tan and Axel Krings. In Proceedings of the The 11th International Conference on Computational Science and Its Applications. Santander, Spain. In the Lecture Notes in Computer Science, Springer-Verlag. June 20-23, 2011.
This paper discusses the models and performance analysis for an adaptive software architecture,
which supports multiple levels of fault detection, masking, and recovery through reconfiguration.
The architecture starts with a formal requirement model defining multiple levels of functional capability and information assurance.
The architecture includes a multi-layer design to implement the requirements using N-variant techniques.
It also integrates a reconfiguration mechanism that uses lower layers to monitor higher layers,
and if a fault is detected, it reconfigures a system to maintain essential services.
We first provide a general reliability model (based on generalized stochastic Petri nets) for such a system with cross-monitoring for reconfiguration.
Next, we define a probabilistic automaton-based model for behavioral modeling of the system.
This model is especially suitable for modeling security problems induced by value faults.
Whereas the Petri net allows for reliability modeling and reconfiguration, the performance analysis of the system is given via probabilistic model checking.
The models are experimentally evaluated and compared.
With the current widespread deployment of multi-core processors,
one question in software engineering is how to effectively harness the parallel computing power provided by these processors.
The architecture presented here allows us to explore the parallel computing power that otherwise may be wasted, and
uses it to improve the dependability and survivability of a system, which is validated by our performance analysis.
"An Automated Verification Based Approach for Analyzing Safety Stock in Probabilistic Supply Chains". Li Tan and Shenghan Xu. In Proceedings ofIn Proceedings of the 2011 annual meeting of Production and Operation Management Society. Reno, NV. April, 2011.
Probabilistic model checking is an automated verification technique that provides a “push-button” approach for algorithmatically analyzing probabilistic systems. Probabilistic model checking has been successfully used for analyzing the performance of a variety of dynamic systems in Computer Science and other fields such as bioinformatics. In this research we will apply probabilistic model checking to the performance analysis of probabilistic supply chains. Particularly we formulate the cost structure of supply chains using reward mechanism in probabilistic model checking. As an application, we will use probabilistic model checking to analyze the impact of different risk factors on the holding of safety stock. We will show that a probabilistic model checker such as PRISM provides an efficient decision procedure for safety stock.
"Entropy and Software Systems: Towards an Information-Theoretic Foundation of Software Testing". Linmin Yang, Zhe Dang, Thomas R. Fischer, Min Sik Kim and Li Tan. In Proceedings of the ACM Sigsoft FSE/SDP workshop on Future of software engineering research (FSE-FoSER'10). ACM press. Santa Fe, New Mexico. November, 2010.
We integrate information theory into software testing. In
particular, we use entropy in information theory to measure
the amount of uncertainty in a software system before
it is fully tested, and we show how the amount decreases
when we test the system. Moreover, we introduce behaviorial
complexity as a novel complexity metric for labeled
graphs (which can be interpreted as control flow graphs, design
specifications, etc.), which is also based on information
theory. We seek practical approaches in testing real systems
using the above theories, and we apply our novel approaches
in testing model-based embedded systems and network intrusion
detection systems. Our information-theoretic approach
is syntax-independent, which is a desired property
in software testing.
"A Hierarchical Formal Framework for Adaptive N-variant Programs in Multi-core Systems". Li Tan and Axel Kring. In Proceedings of The 9th International Workshop on Assurance in Distributed Systems and Networks (ICDCS-ASDN'10). IEEE press. Genoa, Italy. June, 2010.
We propose a formal framework for designing and developing adaptive N-variant programs.
The framework supports multiple levels of fault detection, masking, and recovery though reconfiguration.
Our approach is two-fold:
we introduce an Adaptive Functional Capability Model (AFCM) to define levels of functional capabilities for each service provided by the system.
The AFCM specifies how, once a fault is detected, a system shall scale back its functional capabilities while still maintaining essential services.
Next, we propose a Multi-layered Assured Architecture Design (MAAD) to implement reconfiguration requirements specified by AFCMs.
The layered design improves system resilience in two dimensions:
(1) unlike traditional fault-tolerant architectures that treat functional requirements uniformly,
each layer of the assured architecture implements a level of functional capability defined in AFCM.
The architecture design uses lower-layer functionalities (which are simpler and more reliable) as reference to monitor high-layer functionalities.
The layered design also facilitates an orderly system reconfiguration (graceful degradation) while maintaining essential
system services.
(2) each layer of the assured architecture uses N-variant techniques to improve fault detection.
The degree of redundancy introduced by N-variant implementation determines the mix of faults that can be tolerated at each layer.
Our hybrid fault model allows us to consider fault types ranging from benign faults to Byzantine faults. Last but not the least, multi-layers combined with N-variant implementations are especially suitable for multi-core systems.
"A Formal Stochastic Analysis Approach for Order Splitting Policy". Li Tan and Shenghan Xu. In Proceedings of the 2010 annual meeting of Production and Operation Management Society. Vancouver, Cananda. May, 2010.
The policy of pooling lead-time risk by simultaneously splitting replenishment orders among several suppliers continues to attract the attention of researchers and industrial practitioners in past two decades. Nevertheless, traditional risk analysis approaches used in studying order splitting policy have their limitation on scalability (e.g. stochastic modeling and proving) and/or accuracy (e.g. statistic experiments). To address these shortcomings, in this paper we propose a probabilistic-model-checking-based approach to study the impact of different factors of order splitting policy on risk reduction. We model stochastic behaviors of supply chains using an extension of Markov Decision Processes and translate the goal of risk analysis into a temporal logic. We then use probabilistic model checking to analyze different risk factors in a stochastic supply chain model with order splitting policy, and to identify some key factors that can help reduce lead-time risk.
"An Extensible Object-Oriented and Agent-Based Framework for Modeling and Simulating Supply Chains." Li Tan, Shenghan Xu, Benjamin Meyer, and Brock Erwin. To appear in International Journal of Information and Decision Sciences. InderScience.
We propose an extensible object-oriented agent-based framework
for modeling and simulating supply chains. In today's economy many companies
rely on diversified global supply chains to reduce cost and attain
competitive edge. The structures and behaviors of these supply chains vary based
on underlying business models and markets. However, most of existing
supply-chain analysis tools are designed only for specific subsets of
supply chains. The primary goal of this work is to provide an open and extensible
framework for analyzing supply chains with heterogenous elements and
network structures. To improve extensibility, the framework has incorporated
the following features: 1) the framework adopts an agent-based approach to handle interactions among elements of a supply chain: elements are modeled as autonomous agents and their interactions decide the behavior of the supply chain. The framework provides common functionalities for studying interactions among elements, and an analyst has freedom to define new types of elements required for a specific supply-chain application; and, 2) to improve the design reusability and ease the difficulty in defining a new type of element, we propose an object-oriented type system that supports behavior inheritance. An analyst can focus on defining functions unique to a new type of element, and inherit common behaviors from existing types; and, 3) the framework includes a meta-model for elements of a supply chain. The meta-model abstracts the interface and behavior of an element from its role. We define the formal semantics of the meta-model. The formal semantics helps remove ambiguity in defining a supply-chain model and interpreting analysis result; and, 4) the framework includes a discrete-event simulation algorithm. While the meta-model defines the interface and behavior of individual element, the simulation algorithm defines interactions among elements of a supply chain via messages and deliveries. We will also discuss SimRisk, our Java implementation of the proposed framework.
"An Extensible Object-Oriented and Agent-Based Framework for Modeling and Simulating Supply Chains." Li Tan, Shenghan Xu, Benjamin Meyer, and Brock Erwin. To appear in International Journal of Information and Decision Sciences. InderScience.
We propose an extensible object-oriented agent-based framework
for modeling and simulating supply chains. In today's economy many companies
rely on diversified global supply chains to reduce cost and attain
competitive edge. The structures and behaviors of these supply chains vary based
on underlying business models and markets. However, most of existing
supply-chain analysis tools are designed only for specific subsets of
supply chains. The primary goal of this work is to provide an open and extensible
framework for analyzing supply chains with heterogenous elements and
network structures. To improve extensibility, the framework has incorporated
the following features: 1) the framework adopts an agent-based approach to handle interactions among elements of a supply chain: elements are modeled as autonomous agents and their interactions decide the behavior of the supply chain. The framework provides common functionalities for studying interactions among elements, and an analyst has freedom to define new types of elements required for a specific supply-chain application; and, 2) to improve the design reusability and ease the difficulty in defining a new type of element, we propose an object-oriented type system that supports behavior inheritance. An analyst can focus on defining functions unique to a new type of element, and inherit common behaviors from existing types; and, 3) the framework includes a meta-model for elements of a supply chain. The meta-model abstracts the interface and behavior of an element from its role. We define the formal semantics of the meta-model. The formal semantics helps remove ambiguity in defining a supply-chain model and interpreting analysis result; and, 4) the framework includes a discrete-event simulation algorithm. While the meta-model defines the interface and behavior of individual element, the simulation algorithm defines interactions among elements of a supply chain via messages and deliveries. We will also discuss SimRisk, our Java implementation of the proposed framework.
"Modeling and Analysis of the Impact of Demand Seasonality on Post-merger Synergy". Li Tan and Shenghan Xu. In Proceedings of INFORMS annual conference (INFORMS'09). San Diego, CA. October, 2009.
M&As bring opportunity for companies to streamline supply chains. To fully benefit from the possible synergy, a merged company has to consider how the seasonal demand patterns of its original and adopted products may affect logistic cost. We model and analyze supply-chain consolidation of various settings, and we study the seasonal demand variance of products and study its impact on post-merger synergy. We propose two metrics for demand seasonality and identify their relations to the synergy.
"An Agent-Based Formal Framework for Modeling and Simulating Supply Chains". Li Tan, Shenghan Xu, Benjamin Meyer, and Brock Erwin. In Proceedings of the IEEE International Conference on Information Reuse and Integration (IRI'09). Las Vegas, NV. August, 2009.
We propose an open and extensible agent-based formal framework for modeling and simulating supply chains. Since structures and behaviors of supply chains can be very different based on underlying business models and markets, most of existing simulation and modeling tools are only applicable to specific subsets of supply chains. To improve extensibility, a distinctive feature of our approach is that it separates the functionalities of an element from its role and handles interactions among elements in an agent-based framework: elements are modeled as agents and their interactions decide the behavior of a supply chain. Our framework provides formal definitions for the syntax and semantics of an element. The framework separates internal behaviors of an element from its interface. These features make it easier to define new types of elements and customize their behaviors for a variety of supply-chain applications. The framework also gives rigid simulation-based semantics for a supply-chain model. The formalism it introduced helps an analyst understand and validate simulation results precisely and rigorously. The formal framework also facilitates automated formal analysis of a supply chain [TanXu08]. We discuss the implementation of our framework in context of SimRisk, a supply chain simulation and analysis tool we developed.
"Resilient Multi-core Systems: A Hierarchical Formal Model for N-variant Executions ", Axel Krings, Li Tan, Clint Jeffrey, and Robert Rink. In Proceedings of ACM Cyber Security and Information Intelligence Research Workshop (CSIIRW'09), Oak Ridge National Lab, Oak Ridge, TN, April 13-15, 2009.
This research presents a hierarchical formal model capable
of providing adjustable levels of service and quality of assurance, which is especially suitable for multicore processor systems. The multi-layered architecture supports multiple levels of fault detection, masking, and dynamic load balancing. Unlike traditional fault-tolerant architectures that treat service requirements uniformly, each layer of the assured architecture implements a di erent level of services and information assurances. The system achieves load balancing by moving between layers of di erent complexity. Functionalities at di erent layers range from essential services necessary to satisfy the most stringent requirements for information assurance and system survivability at the lowest layer, to increasingly sophisticated functionalities with extended capabilities and complexity at higher layers. Low-layer functionalities can be used to monitor the behavior of high-layer functionalities.
At each layer of the assured architecture, N-variant implementations make effecient use of multi-core hardware. The degree of the introduced redundancy in each layer determines the mix of faults that can be tolerated. The use of hybrid fault models allows us to consider fault types ranging from benign faults to Byzantine faults. Our framework extends recent work in N-variant systems for intrusion detection, which are demonstrated to be special cases. Furthermore, it allows the movement in a tradeo space between (1) the levels of assurance provided at different layers, (2) the levels of redundancy used at speci c layers, which determine the fault types that can be tolerated, and (3) the desired run-time overhead.
"A Model-Checking-Based Approach to Risk Analysis in Supply Chain Consolidations", Li Tan and Shenghan Xu. To appear in Integrated Computer-Aided Engineering. IOS Press. 2009.
Supply chain strategy has become an important factor that
dictates the successes of companies in today's competitive
world. Nowadays more and more companies are tapping into the
mergers and acquisitions activity in hope of getting the
synergistic gain in supply chain consolidation. In this paper
we use a model-checking-based approach to study the impact of
different consolidation strategies on risks in supply chains
and compare their capacity of risk reduction. We model
stochastic behaviors of supply chains using an extension of
Markov Decision Processes and translate the goal of risk
analysis into a temporal logic. We then apply probabilistic
model checking to analyzing risks inherent in a stochastic
supply chain model. In our computational study, we consider
three different consolidation strategies initially modeled in
[19] and compare their capability of risk reduction in
a generic three-echelon supply chain network. Our results
reveal some key factors that improve the benefit of supply
chain consolidation on risk reduction.
"Formal Analysis of Risks in Stochastic Supply Chains", Shenghan Xu and Li Tan. In the proceedings of the INFORMS annual meeting(INFORMS'08). Washington, DC, 2008.
We propose a formal-verification-based approach for evaluating risks in supply chains. The new “push-button” approach improves the efficiency and scalability of risk analysis algorithms by extending decision procedures developed in Computer Science for analyzing large-scale computer-based systems. It enables us to query a rich set of stochastic behaviors of a supply chain using temporal logics. To facilitate formal analysis, we also establish a formal modeling framework for risk analysis of a stochastic supply chain.
"Model Check Stochastic Supply Chains", Li Tan and Shenghan Xu. In the proceedings of the IEEE International Conference on Information Reuse and Integration (IRI'08). Las Vegas, NV, 2008.
Supply chain [2], [6] is an important componentof business operations. Understanding its stochastic behaviors is the key to risk analysis and performance evaluation in supply
chain design and management.We propose a novel computational
framework for modeling and analyzing the stochastic behaviors
of a supply chain. The framework is based on probabilistic model
checking, a formal verification technique for analyzing stochastic
systems. Our approach is two-fold: first, we developed Stochastic
Supply Chain Model (SMF), a formal framework for modeling
stochastic supply chains based on Extended Markov Decision
Process (EMDP); second, we proposed a model-checking-based
formal technique to automate the analysis of a stochastic supply
chain. Our model-checking-based approach leverages benefits
of recent advances in symbolic probabilistic model checking to
improve the efficiency and scalability of decision procedures.
Using the temporal logic PCTL [1] and the symbolic probabilistic
model checker PRISM [4], we are able to express and check
complicate temporal and stochastic properties on supply chains.
Finally, we demonstrate the capability of our model-checkingbased
approach by testing it on a variety of stochastic supply
chain models.
"Model-based Self-Adaptive Embedded Systems with Temporal Logic Specifications"". Li Tan. In the proceedings of the 6th IEEE International Conference on Quality Software (QSIC'06). Beijing, China., October 27-28, 2006.
We propose a model-based framework for developing a self-adaptive
embedded program, which monitors its own execution and reconfigures
itself at runtime to avoid failure and improve performance. Our
approach uses formal methods at different design stages to reduce
the complexity of developing a self-adaptive embedded program. In
our framework system requirement is rigidly encoded in temporal
logics, and the original embedded system behavior is captured in a
hybrid automaton-based model. We introduce a reconfiguration
specification language \redl\ to specify reconfiguration
requirements, and define a formal semantics of reconfiguration in
context of hybrid automaton. Using formal methods also help automate
design and implementation: we use model-based runtime verification
techniques introduced in \cite{TanKim04} to extend a system model to
a self-monitoring model based on its temporal logic requirements; we
then extend the self-monitoring model with a reconfiguration
mechanism based on its \redl\ specification. Our approach works with
models, and hence it may be incorporated into existing model-based
design workflow: the resulting self-adaptive model can be analyzed
using an existing model simulator and may be used to generate a
self-adaptive embedded program for targeted platform.
"Model-based Self-monitoring Embedded Systems with Temporal Logic Specifications". Li Tan. In the proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE'05). Long Beach, CA., November 7-11, 2005.
We propose a model-based framework for developing self-monitoring embedded programs with temporal logic specifications. In our framework the requirement specification of an embedded program is encoded in the temporal logic MEDL. We propose an algorithm that synthesizes a model-based monitor from a MEDL script. We also introduce a technique that instruments a system model to emit events defined in the model-based primitive event definition language mPEDL. The synthesized model-based monitor may be composed with the instrumented model to form a self-monitoring model, which can be simulated for design-level verification; the composed
self-monitoring model can also be used to generate a self-monitoring embedded program, which can monitor its own execution on the target platform in addition to its normal functions. Our approach combines the rigidness of temporal logic specifications with the easy use of a toolkit \mist\ that we developed to automate the process of building a self-monitoring embedded program from a system model and its requirement specification.
"PlayGame: A Platform for Diagnostic Games". Li Tan. In the proceedings of the 16th International Conference on Computer-Aided Verification (CAV'04), Boston, MA, Volume 3114 of Lecture Notes in Computer Science, Springer-Verlag, 2004
We introduce an integrated tool for implementing and playing various diagnostic games. The tool uses a semantics hierarchy introduced in [Tan02] to improve code sharing among different diagnostic games and reduce the cost of introducing a new game. PlayGame synthesizes the winning strategy for a game using the evidence that is an abstract and uniform encoding of the proof computed by a checker, and hence instead of relying on a particular checker the tool works on a variety of checkers that can be extended to produce such evidence. PlayGame implements a µ-calculus game and a full range of equivalence/preorder games on the Concurrency Workbench-New Century (CWB-NC).
"Specification-based
Testing with Linear Temporal Logic", Li Tan, Oleg Sokolsky, and
Insup Lee. In the proceedings of
IEEE Internation Conference on Information Reuse and Integration (IRI'04),
Las Vegas, NV, IEEE society, 2004.
This paper considers the specification-based testing
in which the requirement is given in the linear temporal logic (LTL).
The required LTL property must hold on all the executions of the system.
The central piece of our framework is a property-coverage metrics.
Based on the requirement mutation, the metrics measures how well a property
has been tested by a test suite. We define a coverage criteria based on the metric
that selects a finite set of tests from all the possible executions
of the system. We also discuss the technique of generating a test suite for
specification testing by using the
counterexample mechanism of a model checker. By exploiting the special
structure of a generated test, we are able to reduce a test with the
infinite length to an equivalent one of finite length. Our framework provides
a model-checking-assisted approach that generates a test suite that is finite
in size and in length for testing linear temporal properties on an
implementation.
Model-based Testing and
Monitoring for Hybrid Embedded Systems, Li Tan, Jesung Kim, Insup
Lee, and Oleg Sokolsky. In the proceedings of
IEEE Internation Conference on Information Reuse and Integration (IRI'04),
Las Vegas, NV, IEEE society, 2004.
We propose an integrated framework for testing and
monitoring the model-based embedded systems. The framework incorporates
three separately developed techniques: 1) test generation based on
hybrid system models, 2) run-time verification, and 3) modular code
generation for hybrid systems. To analyze behaviors of the system,
the system model is augmented with a testing automaton that represents
a given test case, and with a monitoring automaton that captures formally
specified properties of the system. The augmented model allows us
to perform model-level validation. In the next step, we use the modular
code generator to convert the testing and monitoring automata into
code that can be linked with a system implementation to perform the
same analysis on the implementation level. The paper presents an overview
of the framework, illustrated by a case study using the Sony AIBO
robot platform.
Model-based Self-Monitoring
Embedded Programs, Li Tan. Submitted to IEEE International Conference
on Dependable Systems and Networks (DSN'04), Florence, Italy, 2004.
We propose an integrated framework for monitoring
model-based embedded systems based on formal specifications of system
requirements. In our framework the safety requirements of embedded
systems are formally encoded in a temporal logic. A model-based monitor
is synthesized from the logic specification and composed with the
instrumented system model to form a self-monitoring model, which facilitates
the design-level validation via simulation. Using an existing code
generation process, we convert the self-monitoring model to a self-monitoring
embedded program that performs the runtime analysis on the target
embedded systems in addition to its normal function. Our technique
works on models, and hence it avoids the changes on existing model-based
design tools and the development of costly code-based monitoring mechanism.
We developed MI2ST, a model instrumentation and monitor synthesis
toolkit for supporting this new framework. We discuss in detail through
a hands-on case study on SONY AIBO Robot dog how the framework provides
both design-level and implementation-level validations.
"Testing and Monitoring
Model-based Generated Program". L. Tan, J. Kim, and I. Lee. The
third workshop on Runtime Verification. Boulder, Colorado, 2003. Electronic
Notes in Theoretic Computer Science, Volume 89, No. 2. Elsevier Science.
We propose an integrated framework to test and monitor
code generated from hybrid models for embedded systems. The framework
consists of the following elements: First, we create testing automata
as a controlled environment to produce test traces achieving the desired
testing criteria; Second, we synthesize monitoring automata from the
behavior specification to check the run-time behavior of the tested
system in response to the test traces; Finally, since both automata
are encoded in the same language as the system model, the same code
generator may be used to generate a tester and a monitor from the
testing automata and the monitoring automata, and link them with the
code generated from the system model. Our approach yields self-testing
and self-monitoring code which may be run both on the simulation level
and on the code level. We discuss our approach in its full details
through an example on a SONY AIBO robotic dog.
"Simulation
Revisited". L. Tan and R. Cleaveland. In Tools and Algorithms
for the Construction and Analysis of Systems, Vol. 2031 of Lecture
Notes on Computer Science. 2001.
This paper develops an efficient algorithm for determining
when one system is capable of simulating the behavior of another.
The method combines an iterative algorithm for computing behavioral
preorders with an algorithm that simultaneously computes the bisimulation
equivalence classes of the systems in question. Experimental data
indicate that the new routine dramatically outperforms the best-known
algoritm for computing simulation, even when the systems are minimized
with respect to bisimulation before the simulation algorithm is invoked.
"Property-Coverage
Testing", L. Tan, O. Sokolsky, and I. Lee. Submitted to CAV'03.
Also available as technical report MS-CIS-03-02.
Department of Computer and Information Science, University of Pennsylvania.
This paper presents a faster on-the-fly algorithm
for full mu-calculus. The algorithm evaluates the fixpoints for a
revised version of hierachical equation system. The procedure to evaluate
components of equation systems are derived from LAFP while avoids
the construction of dependence set. Our main result, SLP, shows in
practice how ``counter'' and ``reverse list'' may be used to eliminate
the extra cost in implementation. SLP is a linear-space algorithm
and matches the best global linear-space algorithms. In practice,
it shows the superior performance comparable to the on-the-fly algorithm
designed for a special fragment of mu-calculus.
"Two Fast Local Algorithms
for Full mu-calculus". L. Tan and R. Cleaveland. In submission
to a Journal publication.
This paper presents a faster on-the-fly algorithm
for full mu-calculus. The algorithm evaluates the fixpoints for a
revised version of hierachical equation system. The procedure to evaluate
components of equation systems are derived from LAFP while avoids
the construction of dependence set. Our main result, SLP, shows in
practice how ``counter'' and ``reverse list'' may be used to eliminate
the extra cost in implementation. SLP is a linear-space algorithm
and matches the best global linear-space algorithms. In practice,
it shows the superior performance comparable to the on-the-fly algorithm
designed for a special fragment of mu-calculus.
"Evidence-Based Model
Checking". L. Tan and R. Cleaveland. In Computer-Aided Verification
2002, volume 2404 of Lecture Notes in Computer Science, Copenhagen,
July 2002. Springer Verlag.
This paper shows that different ``meta-model-checking''
analyses can be conducted efficiently on a generic data structure
we call a support set. Support sets may be viewed as abstract encodings
of the ``evidence'' a model checker uses to justify the yes/no answers
it computes. We indicate how model checkers may be modified to compute
supports sets without compromising their time or space complexity.
We also show how support sets may be used for a variety of different
analyses of model-checking results, including: the generation of diagnostic
information for explaining negative model-checking results; and certifying
the results of model checking (is the evidence internally consistent?).
"An Abstract Schema
for Equivalence Games". L. Tan. In Verification, Model Checking,
and Abstract Interpretation 2002 (VMCAI'02). Volume 2294 of Lecture
Notes in Computer Science, Venice, Italy. Jan. 2002. Springer Verlag
Equivalence games have been shown as an efficient
way to diagnose design systems. Nevertheless, like other diagnostic
routines, equivalence games utilize the information already computed
by equivalence checker during verification. Therefore, these diagnostic
routines tightly gear to the data structure of checker being used,
and their ability of migrating to a different checker is not always
guaranteed. Moreover, different equivalence relations demand different
game schemas, which makes it tedious to implement equivalence games.
We solve the first problem by utilizing a generalized version of partition
refinement tree (PRT) as an abstract of proof structures. With a little
bookkeeping, a partition refinement-based checker is able to supply
PRT as the evidence to support its result. The diagnostic routines
built on PRTs are independent of equivalence checkers being used.
PRTs may also be used to certify the equivalence-checking result.
To solve the second problem, we introduce a {\em
semantics hierarchy}. Implementation following this hierarchy enjoys
greater code sharing among different games. The prototype of this
schema, including \textsf{PRT}-friendly algorithms and the architecture
of semantics hierarchy, has been implemented on the Concurrency
Workbench.
"Evidence-Based Verification".
L. Tan. Ph.D. Thesis. Computer Science Department, State University
of New York at Stony Brook.
The ability of generating diagnostic information
and performing other ``post-verification" analyses is an important
feature of verification tools. Traditionally these analyses rely on
the proof computed during verification and hence are tightly geared
to the infrastructures of these checkers. We present a framework for
certifying verification results and efficiently generating diagnostic
information in the domain of equivalence checking, preorder checking,
and model checking of finite-state system. The central idea is to
use a generic data structure called ``abstract proof structure''(APS)
to abstractly encode the proof structure by which a verification engine
(checker) reaches its result. APS carries checker-independent evidence
for justifying verification result and provides the basis for a variety
of ``post-verification" analyses.
In this framework, APS serves as interface data structure
betweencheckers and analysis routines. Checkers are enhanced with
bookkeeping code to produce APSs as their results instead of simple
``yes/no" answer. A wide range of existing checkers can be modified
to produce APS without compromising their time and space complexities.
We then show how APSs may be used to perform an array
of ``post-verification" analyses, including certification of
verification result and generation of different forms of diagnostic
information.
An immediate usage of APS is to certify verification
result by checking the internal consistency of \APS submitted by checker.
We provide efficient algorithms to preform such checking.
The primary goal of this framework is to improve
the efficiency and flexibility of diagnostic generation routines.
We show that many diagnostic analyses can be preformed using APSs,
including some traditional (e.g., counterexamples [CGMZ95] in model
checking and HML formulas [HennessyMilner] for bisimulation) and novel(e.g.,
vacuity detection [BBER97]) diagnostic schema. We also show how winning
strategies for property-checking games [Stirling95] can be built from
APS. The analysis routines based on APS enjoy independence from checkers;
hence they can be easily modified and migrated from one checker to
another. In essence APSs help standardize the output of checkers,
and analysis routines therefore can be created and executed independently,
which has other interesting applications such as a client-server architectures
for verification.
"A Partition Refinement
Algorithm for Computing Simulation Equivalence". L. Tan and R.
Cleaveland. Manuscript under preparation.
We gives an improved partition refinement algorithm
to compute the simulation equivalence relation. It significantly reduces
the space usage in the practice because the preordering relation is
stored and retrieved in the pairs of classes, instead of states. It
is also the first partition-refinement based algorithm whose has the
same time complexity as the best simulation algorithm. Besides the
applications where a computation of simulation preordering is called,
it can be used for minimizing processes in the term of simulation
equivalence. Since the minimized process preserves all ACTL* formula,
the simulation-based abstraction utilizing this algorithm can enable
us to check ACTL*
formula on larger systems.
"N-dimension scheduling
algorithms". L. Tan, R. S. Lou and G. Q. Xu. In the Journal of
Computers. Vol. 20, Page 105-110, 1997.
Geometry method has been proven as an sucessful way
to study the safety problem of scheduling two transations. We extend
it to N dimension space to handle the arbitrary number of concurrent
transaction. The forbidden area in the case of two transitions will
be therefore generilized as a prism in N dimension space. We give
a sufficient condition for ensuring seriability of N transitions.
Consequently the polcy based on this condition, called BOLP, extends
traditional two phrase locking policy to schedule N transactions safely.