Farn Wang

TCS Journal 2018 Journal Article

Theoretical aspects of computing

• Augusto Sampaio
• Farn Wang

TCS Journal 2015 Journal Article

Complexity of node coverage games

• Farn Wang
• Sven Schewe
• Jung-Hsuan Wu

Modern software systems may exhibit a nondeterministic behavior due to many unpredictable factors. In this work, we propose the node coverage game, a two-player turn-based game played on a finite game graph, as a formalization of the problem to test such systems. Each node in the graph represents a functional equivalence class of the software under test (SUT). One player, the tester, wants to maximize the node coverage, measured by the number of nodes visited when exploring the game graphs, while his opponent, the SUT, wants to minimize it. An optimal test would maximize the cover, and it is an interesting problem to find the maximal number of nodes that the tester can guarantee to visit, irrespective of the responses of the SUT. We show that the decision problem of whether the guarantee is less than a given number is NP-complete. We also discuss two extensions of our result and present a testing procedure based on our result when the SUT is not so hostile.

TCS Journal 2013 Journal Article

Efficient model-checking of dense-time systems with time-convexity analysis

• Farn Wang

To overcome the sky-rocketing verification cost of embedded software, symbolic model-checking technology of dense-time automata has been proposed as an automated solution. The construction of a timed precondition is a central component in the technology. The general formulation for a timed precondition operator needs to check the continuity of time progress and usually results in high complexity in the construction. However, when the state space characterized by the path condition is convex, we can use a more efficient convex timed precondition operator. In this work, we discuss the concept of time-convexity that allows us to relax the restrictions on the application of the convex timed precondition operator in place of the general one. We present examples in model-checking that engender a non-time-convex space of time progress. Nevertheless, we have also identified a class of timed computation tree logic (TCTL) formulas that only characterize time-convex state spaces. This class includes several important types of TCTL formulas, including some timed inevitabilities with deadlines. We then present a new formulation for the efficient evaluation of general timed inevitabilities with non-time-convex path conditions. The new formulation also leads to a new technique for the approximate evaluation of timed inevitabilities with better precision. Finally, we report our implementation and experiments.

GandALF Workshop 2012 Workshop Paper

Rapid Recovery for Systems with Scarce Faults

• Chung-Hao Huang
• Doron Peled
• Sven Schewe
• Farn Wang

Our goal is to achieve a high degree of fault tolerance through the control of a safety critical systems. This reduces to solving a game between a malicious environment that injects failures and a controller who tries to establish a correct behavior. We suggest a new control objective for such systems that offers a better balance between complexity and precision: we seek systems that are k-resilient. In order to be k-resilient, a system needs to be able to rapidly recover from a small number, up to k, of local faults infinitely many times, provided that blocks of up to k faults are separated by short recovery periods in which no fault occurs. k-resilience is a simple but powerful abstraction from the precise distribution of local faults, but much more refined than the traditional objective to maximize the number of local faults. We argue why we believe this to be the right level of abstraction for safety critical systems when local faults are few and far between. We show that the computational complexity of constructing optimal control with respect to resilience is low and demonstrate the feasibility through an implementation and experimental results.

TCS Journal 2004 Journal Article

Reachability solution characterization of parametric real-time systems

• Farn Wang
• Hsu-Chun Yen

We investigate the problem of characterizing the solution spaces for timed automata augmented by unknown timing parameters (called timing parameter automata (TPA)). The main contribution of this paper is that we identify three non-trivial subclasses of TPAs, namely, upper-bound, lower-bound and bipartite TPAs, and analyze how hard it is to characterize the solution spaces. As it turns out, we are able to give complexity bounds for the sizes of the minimal (resp. , maximal) elements which completely characterize the upward-closed (resp. , downward-closed) solution spaces of upper-bound (resp. , lower-bound) TPAs. For bipartite TPAs, it is shown that their solution spaces are not semilinear in general. We also extend our analysis to TPAs equipped with counters without zero-test capabilities.