Selected Publications

I Journal articles

  1. Real-Time Distributed System Specification and Verification in APTL. ACM Transactions on Software Engineering and Methodology, Vol. 2, No. 4, Octobor 1993, pp. 346-378. (with A.K. Mok and E.A. Emerson)
  2. Parametric Timing Analysis of Real-Time Systems. Information and Computation, Vol. 130, Nr 2, Academic Press, ISSN 0890-5401, Nov. 1996; pp.131-150.
  3. A Temporal Logic for Real-Time Partial-Ordering with Named Transactions. Theoretical Computer Science, Vol. 181, Nr. 1, 15 July 1997, pp. 195-225; Guest Editor : R. Baeza Yates, E. Coles. A preliminary version also appears in Proceedings of Latin American Theoretical INformatics Symposium, Santiago, Chile, April, 1995. LNCS 911, Springer-Verlag.
  4. Symbolic Model Checking for Event-Driven Real-Time Systems. ACM Transactions on Programming Languages and Systems, Vol. 19, Nr. 2, March 1997, pages 386-412. (with J. Yang, A.K. Mok)
  5. Procedure-Level verification of Real-Time Concurrent Systems. the Journal of Real-Time Systems, vol. 16, Nr. 1, January 1999, pp.81-114, Kluwer Academic Publishers. (with Chia-Tien Lo)
  6. Parametric Analysis of Computer Systems. accepted by the Journal of Formal Methods in Systems Design, Kluwer Academic Publishers.
  7. Efficient and User-Friendly Verification. Accepted by IEEE Transactions on Computers.  (with P.-A. Hsiung)

II Conference and workshop articles

  1. Formal Specification of Asynchronous Distributed Real-Time Systems by APTL. In Proceedings of International Conference on Software Engineering, Melbourne, Australia, May, 1992. (with A.K. Mok and E.A. Emerson)
  2. Asynchronous Real-time Event Logic. In Proceedings of International Computer Symposium, Taichung, Taiwan, December, 1992. (with A.K. Mok)
  3. Symbolic Model-Checking for Distributed Real-Time Systems. In Proceedings of Formal Methods Europe Symposium, Odense, Denmark, April, 1993, LNCS 670. (with A.K. Mok and E.A. Emerson)
  4. A Verifier for Distributed Real-Time Systems with Bounded Integer Variables. In Proceedings of COMPASS Conference, Paithersburg, Maryland, June, 1993. (with A.K. Mok)
  5. Symbolic Model Checking for Event-Driven Real-Time Systems. In Proceedings of the 1993 IEEE Real-Time System Symposium. (with J. Yang and A.K. Mok)
  6. RTL and Refutation by Positive Cycles. In Proceedings of Formal Methods Europe Symposium, Barcelona, Spain, October, 1994, LNCS 873. (with A.K. Mok)
  7. Timing Behavior Analysis for Real-Time Systems. In Proceedings of IEEE Symposium on Logic in Computer Science, San Diego, California, U.S.A., June, 1995.
  8. Reachability Analysis at Procedure Level Through Timing Coincidence. In Proceedings of the 6th International Conference on Concurrency Theory, Philadelphia, U.S.A., August, 1995. LNCS 962, Springer-Verlag.
  9. An Experiment on Efficient Real-Time System Verification through Refutation by Positive Cycles. In Proceedings of the 1st RAMS (Real-time And Media Symposium), Taipei, ROC, July, 1995.
  10. Procedure-Level Verification of Real-time Concurrent Systems. In Proceedings of the 3rd FME (Formal Method Europe) Symposium, Oxford, England, March, 1996; LNCS 1051, Springer-Verlag. (with Chia-Tien Lo)
  11. Scalable Compositional Reachability Analysis of Real-Time Concurrent Systems. In Proceedings of the 2nd IEEE RTAS (Real-Time Technology and Applications Symposium), Boston, June, 1996.
  12. Scalable Compositional Verification of High-Level Real-Time Concurrent Systems : From 10^7 to 10^{85} states. In Proceedings of the 3rd RTCSA (Real-Time Computing Systems and Applications), Seoul, Korea, October, 1996
  13. High-Level Execution Time Analysis. in Proceedings of the Fourth International AMAST Worshop on Real-Time Systems, Concurrent, and Distributed Software (ARTS'97), Mallorca, Spain, May, 1997; LNCS 1231, Springer-Verlag.
  14. Error Propagation Analysis of Real-Time Data-Intensive Applications. work-in-progress paper, in Proceedings of the 3rd IEEE RTAS (Real-Time Technology and Applications Symposium), Montreal, Canada, June, 1997. (with T.-W. Kuo, D. Locke)
  15. PASS: A Prototyping, Analysis, Simulation, and Synthesis Environment for Real-Time Systems. to appear in Proceedings of the 4th RTCSA (Real-Time Computing Systems and Applications), Taipei, Taiwan, October, 1997 (with T.-W. Kuo, S.-J. Ho, J.-H. Wey)
  16. Parametric Analysis of Computer Systems. In Proceedings of the 6th AMAST (Algebraic Methodology And Software Technology) Conference, Sydney, Australia, December, 1997; LNCS 1349, Springer-Verlag. (with P.-A. Hsiung)
  17. Automatic Verification on the Large. Invited for presentation in 1998 IEEE HASE (High-Assurance Systems Engineering) Symposium, Nov. 13-14, Washington, D.C., USA. (with P.-A. Hsiung)
  18. A State Graph Manipulator Tool for Real-Time System Specification and Verification. 1998 RTCSA (Real-Time Computing Systems and Applications) Workshop, October 1998, Hiroshima, Japan. (with P.-A. Hsiung)
  19. Scheduling System Verification. accepted to appear in proceedings of 1999 TACAS (Tools and Algorithms for the Construction and Analysis of Systems), March 1999, LNCS 1579, Springer-Verlag. (with P.-A. Hsiung, Y.-S. Kuo)
  20. Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes. accepted to appear in proceedings of FM'99 (Formal Method World Congress), September 1999, in LNCS, Springer-Verlag.
  21. User-Friendly Verification. accepted to appear in proceedings of FORTE/PSTV'99 (FORmal description TEchnique/Protocol Specification, Testing, Verification), October, 1999. (with P.-A. Hsiung)
  22. Verification of Concurrent Client-Server Real-Time Scheduling Systems. in proceedings of RTCSA'99, Dec., 1999, IEEE press. (with P.-A. Hsiung, Y.-S. Kuo)
  23. Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems. to appear in proceedings of TACAS'2000, LNCS 1785, Springer-Verlag.
  24. Region Encoding Diagram for Fully Symbolic Verification of Real-Time Systems. to appear in proceedings of 24'th IEEE COMPSAC'2000 (Computer Software and Applications Conference), Oct, 2000.
  25. Parametric Optimization of Open Real-Time Systems, to appear in proceedings of SAS 2001 (Static Analysis Symposium), Paris, France, 16-18 July, 2001; in LNCS Springer-Verlag. 
  26. Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram, to appear in proceedings of FORTE 2001(the 21st International Conference on Formal Techniques for Networked and Distributed Systems), Cheju Island, Korea.  25-28 Aug, 2001.  
  27. RED: Model-Checker for Timed Automata with Clock-Restriction Diagram.  In proceedings of Workshop on Real-Time Tools, Aalborg University, Denmark, August 20, 2001.  Technical Report 2001-014, ISSN 1404-3203, Department of Information Technology, Uppsala University.