|
|
About MeResearch InterestsPublicationsTalksToolsProfessional SevicesTeachingCESE |
My research interests lie in designing and verifying safety-critical software and hardware systems. The topics of my special interests include:
1. Model-based Design and Validation of Embedded SystemsToday embedded systems can be found in a wide range of applications from automobile Engine Management Systems (EMS) to deep space explorers. Ensuring the correct functioning of these embedded systems becomes an ever-challenging problem. Model-based design has been embraced as a promising technique for designing safety-critical embedded systems. By adopting a mathematical modeling process at early design stage, model-based design allows engineers to simulate and analyze a design before the actual implementation. An embedded system is typically an integration of software threads, special-purpose digital circuit, and analog devices continuously interacting with the environment. The model for such a system has both continuous dynamics and discrete behaviors, which often renders traditional verification techniques developed for discrete systems intractable in verifying embedded system design. We proposed and developed a new verification framework that incorporates traditional testing method and the state-of-the-art software runtime verification technique into model-based design [TKL03,TKLS04]. This new technique integrates verification mechanism as part of a system model. It synthesizes a self-monitoring model from the original system model and its temporal logic requirements. The self-monitoring model checks its own runtime behavior during model simulation. The result can then be used to refine the system design; furthermore, the self-monitoring model may also be used to generate a self-monitoring embedded program, which performs runtime checking on the target hardware in addition to its normal functions. The technique addresses validation on the design stage as well as on implementation level. Recently we show that the information obtained from runtime checking may be used to steer a program from bad states, and hence the framework can be extended to build adaptive embedded systems. We developed a model-instrumentation and monitor-synthesis toolkit M2IST [TKLS04] that fully automates the process of synthesizing self-monitoring models. Publications
Talks
Tools
2. Software Testing with Formal RequirementsTesting plays an indispensable role in developing reliable systems. Industrial practice shows that testing accounts for a large percentage of development cost. Testing can benefit from the recent advances in formal methods and automatic verification in several ways. Automatic verification supports the precise formulation of system requirements that facilitates the formal proof of systems. The available formal requirements turn out to be also a valuable asset to other elements in software development process since they eliminate ambiguity in understanding system requirements. We study the specification-based testing in which the system requirement is formally encoded in Linear Temporal Logic [TSL04,TSL03]. To have testing concentrated on the requirement, we propose a coverage metrics that measures how thoroughly the requirement is being tested and coverage criteria that select tests by the requirement [TSL03]. To make test generation efficient, we adapt the diagnostic mechanisms of model checkers to automate test generation. We also show that the technique may be combined with traditional structure-based testing, for which several structural coverage criteria can be encoded as part of the formal requirement. Ultimately, we wish to provide efficient test generation for specification-based testing and structural-based testing in a single framework based on model-checking technique. We also apply this technique to the testing of hybrid systems, a variety of systems with both discrete and continuous behaviors. We are currently integrating the predicate-abstraction-based model checking technique with the simulation-based test generator we developed to improve its efficiency and generate tests under formal requirements. Publication
Talks
3. Evidence-based VerificationIn automatic verification, learning the evidence for verification results, in other words why a system fails or passes a verification task, could be as important as the result itself. The evidence can be used and interpreted in many different ways to assist users' understanding on the correctness of the result. For instance, it could be given as a trace leading to the error or a tree-like structure, best known as a counterexample, or it could be presented as an interactive game between the verifier and the users [Tan02a, Tan02b]. Since the internal mechanisms of checkers are very different in term of algorithms and data structures, the way of retaining the evidence and generating diagnostic information also depends on underlying model checkers. This work is to seek a uniform presentation of evidence so that the evidence can be encoded, verified, and processed independently regardless of model checkers producing it. We have defined uniform evidence in the domain of equivalence checking, preorder checking, and model checking [TanCle02,Tan02a,Tan02b]. For equivalence and preordering checkings, the evidence is an extended partition refinement tree, named Kernel-Auxiliary partition refinement tree, or KA-PRT [Tan02a,Tan02b]. For model checking, it is support set [Tan02b]. We also propose an checker-independent algorithm that can validating support sets in ( O (M log ad) ), where M is the size of a mu-Calculus model checking problem and ad is its alternation depth. The fact that validating evidence costs less than model checking facillates an efficient and independent way of checking model-checking results and the integerity of a model checker. Support set may also be used as an independent certificate for the correctness of model-checking result. The evidence has been used for generating diagnostic information like counterexample, Hennessy-Miller logic formula, and the strategy for verification games. Recently we developed a generic game-based toolkit PlayGame [Tan04] that allows the user to diagnose a system design by interacting with the computer. PlayGame is built independent of model checkers by using support sets. Publications
Talks
Tools
4. Efficent Verification Algorithms and Tools DevelopmentI am interested in the research on efficient algorithms for all three major approaches for automatic verification: equivalence checking, preorder checking, and model checking. In model checking, I have been looking into on-the-fly algorithms. On-the-fly model checker is driven by the demand, in contrast to gobal algorithms. On-the-fly doesn't require the prior construction of transition system, which makes it less vulnerable to space explosion problem in explicit-state model checking. Nevertheless, the worst-case time complexities of on-the-fly model checkers are usually worse than those of their gobal peers. We proposed an on-the-fly algorithms for mu-calculus which can compete with the best gobal algorithms in the worst-case time complexity, and also preforms well in commonly-used fragments of mu-calculus such as Alternation-free fragment and L2. For preorder-checking algorithms, we are working on partition refinement-based simulation algorithms [3]. Partition-refinement approach is typically used to handle equivalence relation. We have shown that it may also be applied to computing preordering relations. A major advantage of refinement-based algorithms is space-saving. Refinement-based simulation algorithm stores and manipulates the preordering relation on sets of simulation classes, instead of states, which makes it less vulnerable to state-explosion problem. Publications
Tools Please see the tools section for the complete list of verification tools I have (co-)developed. |
Last updated 02/05/04