Selected Recent Publications by Subject

Run-time Monitoring and Checking

U. Sammapun, I. Lee, O. Sokolsky, and John Regehr, "Statistical Runtime Checking of Probabilistic Properties," Proceedings of the 7th Workshop on Run-time Verification, LNCS 4839, pp. 164-175, March 2007. 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. 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

A. Philippou, I. Lee, O. Sokolsky, and J.-Y. Choi, "A Process Algebraic Framework for Modeling Resource Demand and Supply," The 8th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2010), LNCS 6246, pp. 183-197, September 8 - 10, 2010 O. Sokolsky, I. Lee, and D. Clarke, "Process-Algebraic Interpretation of AADL Models," 14th International Conference on Reliable Software Technologies (Ada-Europe 2009), LNCS 5570, pp. 222-236, June 2009 A. Philippou and O. Sokolsky, "Process-Algebraic Analysis of Timing and Schedulability Properties," Handbook of Real-Time and Embedded Systems, Chapman and Hall/CRC, 2007. 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. Chen, L.T.X. Phan, J. Lee, I. Lee and O. Sokolsky, "Removing Abstraction Overhead in the Composition of Hierarchical Real-Time Systems," Proceedings of the 17th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2011), April 2011 L.T.X. Phan, I. Lee, and O. Sokolsky, " A Semantic Framework for Multi-Mode Systems," Proceedings of the 17th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2011), April 2011 L.T.X. Phan, I. Lee, and O. Sokolsky, "Compositional Analysis of Multi-Mode Systems," The 22nd Euromicro Conference on Real-Time Systems (ECRTS10), July 2010 A. Easwaran, I. Lee, O. Sokolsky and S. Vestal, "A Compositional Scheduling Framework for Digital Avionics Systems," IEEE Real-Time Computing Systems and Applications (RTCSA 2009), August 2009 A. Easwaran, I. Lee and O. Sokolsky, "Interface Algebra for Analysis of Hierarchical Real-Time Systems," Proceedings of the Workshop on Foundations of Interface Technologies (FIT'08), April 2008. 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), April 2006.

Medical Device Software and Systems

BG Kim, A. Ayoub, O. Sokolsky, I. Lee, P. Jones, Y. Zhang, and R. Jetley, "Safety-Assured Development of the GPCA Infusion Pump Software," Proceedings of the International Conference on Embedded Software (EMSOFT 2011), October 2011 E. Jee, I. Lee, and O. Sokolsky, " Assurance Cases in Model-Driven Development of the Pacemaker Software," Proceedings of the 4th International Symposium On Leveraging Application of Formal Methods, Verification and Validation (ISoLA 2010), LNCS 6416, pp. 343-356, October 2010 A. King, D. Arney, I. Lee, O. Sokolsky, J. Hatcliff, and S. Proctor, "Prototyping Closed Loop Physiologic Control with the Medical Device Coordination Framework," Proceedings of 2nd Workshop on Software Engineering in Health Care (SEHC 2010), May 2010 D. Arney, M. Pajic, J.M. Goldman, I. Lee, R. Mangharam, and O. Sokolsky, "Toward Patient Safety in Closed-Loop Medical Device Systems," Proceedings of the International Conference on Cyber-Physical Systems (ICCPS 2010), April 2010

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

V. Chinnapongse, I. Lee, O. Sokolsky, S. Wang, and P.L. Jones, "Model-Based Testing of GUI-Driven Applications," The Seventh IFIP Workshop on Software Technologies for Future Embedded and Ubiquitous Systems (SEUS 2009), LNCS 5860, pp. 203-214, November 2009 N. Dinesh, A.K. Joshi, I. Lee, and O. Sokolsky, "Reasoning about Conditions and Exceptions to Laws in Regulatory Conformance Checking," Proceedings of the Ninth International Conference on Deontic Logic in Computer Science (DEON'08), July 2008. N. Dinesh, A.K. Joshi, I. Lee, and O. Sokolsky, "Checking Traces for Regulatory Conformance," Proceedings of the Eighth Workshop on Runtime Verification (RV'08), Satellite workshop of ETAPS'08, March 2008 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), March 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.