Selected Recent Publications by Subject

Run-time Monitoring and Checking

U. Sammapun, I. Lee and O. Sokolsky, "RT-MaC: Runtime Monitoring and Checking of Quantitative and Probabilistic Properties," Proceedings of the 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA'05), Hong Kong, August 17-19, 2005. O. Sokolsky, U. Sammapun, I. Lee, and J. Kim, "Run-Time Checking of Dynamic Properties," Proceedings of the Fifth Workshop on Runtime Verification (RV'05), The University of Edinburgh, Scotland, UK, July 12, 2005. M. Kim, S. Kannan, I. Lee, O. Sokolsky, M. Viswanathan, "Java-MaC: a Rigorous Run-time Assurance Tool for Java Programs," Formal Methods in Systems Design, Vol 24, No 2, March 2004. Preliminary version appeared in the Proceedings of Workshop on Run-time Verification, July 2001. U. Sammapun, A. Easwaran, I. Lee, and O. Sokolsky, "Simulation of Simultaneous Events in Regular Expressions for Run-Time Verification ," Proceedings of the Workshop on Runtime Verification Workshop (RV'04), April 2004. K. Bhargavan, C.A. Gunter, M. Kim, I. Lee, D. Obradovic, O. Sokolsky, and M. Viswanathan, " Verisim: Formal Analysis of Network Simulations," Transactions on Software Engineering, Vol. 28, No. 2, Feb. 2002, pp. 129-145. Preliminary version appeared in the Proceedings of ISSTA'00. D. Gordon, W. Spears, O. Sokolsky, and I. Lee "Distributed Spatial Control and Global Monitoring of Mobile Agents" , IEEE International Conference on Information, Intelligence, and Systems, November 1999. I. Lee, S. Kannan, M. Kim, O. Sokolsky, and M. Viswanathan "Runtime Assurance Based On Formal Specifications", International Conference on Parallel and Distributed Processing Techniques and Applications, June 28 - July 1, 1999. M. Kim, M. Viswanathan, H. Ben-Abdallah, S. Kannan, I. Lee, and O. Sokolsky "Formally Specified Monitoring of Temporal Properties", European Conference on Real-Time Systems, June 1999

Process Algebras for Real-Time and Probabilistic Systems

I. Lee, A. Philippou, O. Sokolsky, " Resources in process algebra," Journal of Logic and Algebraic Programming, Vol. 72, pp. 98-122, May/June 2007. O. Sokolsky, A. Philippou, I. Lee, and K. Christou, "Modeling and Analysis of Power-Aware Systems," International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS '03), LNCS 2619, pp. 409--424, April 2003. I. Lee, A. Philippou, and O. Sokolsky, " A General Resource Framework for Real-Time Systems," Workshop on Radical Innovations of Software and Systems Engineering in the Future, LNCS 2941, pp. 234--248, October 2002 I. Lee, A. Philippou, and O. Sokolsky, " Process Algebraic Modelling and Analysis of Power-Aware Real-Time Systems," IEE Computing and Control Engineering Journal, 13(4), August 2002, pp. 180-188. H.-H. Kwak, I. Lee and O. Sokolsky, "Parametric approach to the specification and analysis of real-time scheduling based on ACSR-VP," Science of Computer Programming, Vol. 42, Issue 1, Jan 2002, pp. 49--60. I. Lee, J.-Y. Choi, H. H. Kwak, A. Philippou, O. Sokolsky, " A Family of Resource-Bound Real-Time Process Algebras," Proceedings of International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2001), pp 443-458, August 2001. A. Philippou, O. Sokolsky, I. Lee, R. Cleaveland, and S.A. Smolka, "Hiding Resources that Can Fail: An Axiomatic Perspective," Information Processing Letters, Vol. 80, Issue 1, Oct. 2001, pp. 3-13. A. Philippou, I. Lee, and O. Sokolsky " Weak Bisimulation for Probabilistic Systems", CONCUR'00, August 2000. H.-H. Kwak, I. Lee, A. Philippou, J.-Y. Choi, and O. Sokolsky, "Symbolic Schedulability Analysis of Real-time Systems," IEEE Real-Time Systems Symposium, December 1998. A. Philippou, O. Sokolsky, I. Lee, R. Cleaveland, and S. Smolka, "Probabilistic Resource Failure in Real-Time Process Algebra," CONCUR'98, September 1998. A. Philippou, O. Sokolsky, I. Lee, R. Cleaveland, and S. Smolka, "Specifying Failures and Recoveries in PACSR", Workshop on Probabilistic Methods in Verification, University of Birmingham Technical Report CSR-98-4, pp. 153-167, June 1998. O. Sokolsky, M. Younis, I. Lee, H.-H. Kwak, and J. Zhou, "Verification of the Redundancy Management System for Space Launch Vehicle", Real-Time Applications and Technology Symposium, June 1998. H. Ben-Abdallah, I. Lee, and O. Sokolsky, "Operational Semantics for Visual Simulation in PARAGON" , IEEE National Aerospace and Electronics Conference, July 1997.

Composition of Real-Time Systems

S. Fischmeister, O. Sokolsky, and I. Lee, "A Verifiable Language for Programming Communication Schedules," IEEE Transactions on Computers, Vol. 56, pp. 1505-1519, November 2007. A. Easwaran, I. Shin, O. Sokolsky, and I. Lee, " Incremental Schedulability Analysis of Hierarchical Real-Time Components," Proceedings of the 6th ACM International Conference on Embedded Software (EMSOFT 2006), Seoul, South Korea, October 22-25, 2006 O. Sokolsky, I. Lee, and D. Clarke, "Schedulability Analysis of AADL Models," 14th International Workshop on Parallel and Distributed Real-Time Systems (WPDRTS'06), Island of Rhodes, Greece, April25-26, 2006.

Hybrid Systems

R. Alur, R. Grosu, I. Lee, and O. Sokolsky, "Compositional modeling for refinement for hierarchical hybrid systems," Journal of Logic and Algebraic Programming, Volume 68, Issue 1-2, 2006, pp. 105-128. F. Kratz, O. Sokolsky, G. Pappas, and I. Lee, "R-Charon, a Modeling Language for Reconfigurable Hybrid Systems," Proceedings of the 9th International Workshop on Hybrid Systems: Computation and Control (HSCC 2006), Santa Barbara, CA, USA, March 29-31, 2006, LNCS 3927, pages 392-406. O. Sokolsky and G. Pappas, " Platform-Independent Autonomy Modeling," Proceedings of the 4th International Conference on Intelligent Systems Design and Applications (ISDA 2004), August 2004. R. Alur, F. Ivancic, J. Kim, I. Lee, and O. Sokolsky, "Generating Embedded Software from Hierarchical Hybrid Models," International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES '03), pp. 171-182, June 2003. R. Alur, T. Dang, J. Esposito, R. Fierro, Y. Hur, F. Ivancic, V. Kumar, I. Lee, P. Mishra, G. Pappas, O. Sokolsky, " Hierarchical Modeling and Analysis of Embedded Systems," Proceedings of the IEEE , Vol. 90 (1), January 2003, pp. 11-28. Preliminary version appeared in the Proceedings of Workshop on Embedded Software, Lecture Notes in Computer Science, volume 2211, October 2001. O. Sokolsky and H.S. Hong, " Qualitative Modeling of Hybrid Systems," Workshop on Formal Models in Software Development, June 2001. R. Alur, R. Grosu, I. Lee, and O. Sokolsky, Compositional Refinement for Hierarchical Hybrid Systems, International Workshop on Hybrid Systems: Computation and Control, LNCS 2034, pp. 33-48. March 28-30, 2001.

Model-driven Test Generation

L. Tan, O. Sokolsky, and I. Lee, "Specification-based Testing with Linear Temporal Logic," IEEE International Conference on Information Reuse and Integration (IEEE IRI-2004), November 2004. H.S. Hong, S.D. Cha, I. Lee, O. Sokolsky, and H. Ural, "Data Flow Testing as Model Checking," International Conference on Software Engineering (ICSE '03), pp. 232--242, May 2003, H. Hong, I. Lee, O. Sokolsky, and H. Ural, "A Temporal Logic Based Theory of Test Coverage and Generation," International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS2002), April 8-11, 2002.

Model Checking

O. Sokolsky, S.A. Smolka, "Local Model Checking for Real-Time Systems" Computer-Aided Verification '95, Lecture Notes in Computer Science 939, Springer-Verlag, July 1995. S.A. Smolka, O. Sokolsky, S. Zhang, "On the Parallel Complexity of Bisimulation and Modal Checking", in "Modal Logic and Process Algebra", Cambridge University Press, 1995. S. Zhang, S.A. Smolka, and O. Sokolsky, "On the Parallel Complexity of Model Checking in the Modal Mu-Calculus," Proceedings of Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 154-163, IEEE Computer Society Press, July 1994. O. Sokolsky and S.A. Smolka, "Incremental Model Checking in the Modal Mu-Calculus", Computer-Aided Verification '94, Lecture Notes in Computer Science 818, Springer-Verlag, June 1994.

Modeling and Analysis Tools

H. Ben-Abdallah, I. Lee, and O. Sokolsky, "Specification and Analysis of Real-Time Systems with PARAGON", Annals of Software Engineering, vol. 7 (1999), pp. 211-234. D.Clarke, H. Ben-Abdallah, I. Lee, O. Sokolsky, "PARAGON: A Paradigm for the Specification, Verification and Testing of Real-Time Systems", 1997 IEEE Aerospace Conference, IEEE Computer Society Press, February 1997. R. Cleaveland, J.N. Gada, P.M. Lewis, S.A. Smolka, O. Sokolsky, and S. Zhang, "The Concurrency Factory - Practical Tools for Specification, Simulation, Verification, and Implementation of Concurrent Systems" , Proceedings of DIMACS Workshop on Specification of Parallel Algorithms, Princeton, NJ, American Mathematical Society, May 1994.

Miscellaneous

O. Sokolsky, S. Kannan, and I. Lee, "Simulation-Based Graph Similarity," Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), Vienna, Austria, March 27-30, 2006, LNCS 3920, pages 426-440. R. Cleaveland and O. Sokolsky, "Equivalence and Preorder Checking for Finite-State Systems," in "Handbook of Process Algebra," pp. 391-424, Elsevier, 2001. N. Prywes, P. Rehmet, O. Sokolsky and I. Lee, "Retrospective Exploration of Safety Properties in Real-Time Concurrent Systems," IEEE Digital Avionics Systems Conference, October 1997. I. Lee and O. Sokolsky, "A Graphical Property Specification Language," 2nd IEEE Workshop on High-Assurance Systems Engineering, pp. 42-47, IEEE Computer Society Press, August 1997.