Books

1. Modeling and Verification Using UML Statecharts, A Working Guide to Reactive System Design, Runtime Monitoring and Execution-based Model Checking.
Book corrections

2. Practical UML-based Specification, Validation, and Verification of Mission-critical Software. Space Exploration and Defense Software Examples in Practice. ISBN: 978-145750-494-5.

Recent Articles

• D. Drusinsky. The Temporal Rover and the ATG Rover. Springer-Verlag Lecture Notes in Computer Science, 1885, p. 323-329.
• D. Drusinsky, G. Watney, Applying Run-Time Monitoring to the Deep-Impact Fault Protection Engine, 28th IEEE/NASA ICECCS workshop, 2003.
• D. Drusinsky, Real-time,On-line,Low Impact, Temporal Pattern Matching, 7th World Multiconference on Systemics, Cybernetics and Informatics (SCI 2003).
• D. Drusinsky, Monitoring Temporal Logic Specifications Combined with Time Series, Proc. IEEE 4th Formal Specifications Symposium, FSCBS2003.
• D. Drusinsky, Monitoring Temporal Rules Combined with Time Series, Proc. 2003 Computer Aided Verification Conference (CAV).
• D. Drusinsky and M. Shing. Verification of Timing Properties in Rapid System Prototyping, Proc. Rapid System
• D. Drusinsky and M. Shing. Verification of Timing Properties in Rapid System Prototyping, Proc. Rapid System Prototyping Conference 2003 (RSP'2003).
• D. Drusinsky and M. Shing, Monitoring Temporal Logic Specifications Combined with Time Series Constraints, Journal of Universal Computer Science (JUCS), vol. 9, no. 11 (2003), 1261-1276.
• D. Drusinsky and K. Havelund, Execution-Based Real-Time and Time Series Model Checking, Workshop on Model-Checking for Dependable Software-Intensive Systems (International Conference on Dependable Systems and Networks, San Francisco, 2003).
• C. Artho, D. Drusinsky, A. Goldeberg, K. Havelund, M. Lowry, C. Pasareanu, G. Rosu, W. Visser, Experiments with Test Case Generation and Runtime Analysis, 10th International Workshop on Abstract State Machines, Sicily, Italy, 2003, (Invited).
• D. Drusinsky, "Semantics and Runtime Monitoring of TLCharts: Statechart Automata with Temporal Logic Conditioned Transitions," Proc. 4th Runtime Verification Workshop (RV 04), Electronic Notes in Theoretical Computer Science, vol. 113, Elsevier, 2005, pp. 3-21.
• D. Drusinsky, Visual Formal Specification using (N)TLCharts: Statechart Automata with Temporal Logic and Natural Language Conditioned Transitions. International Workshop on Parallel and Distributed Systems: Testing and Debugging (PADTAD), 2004.
• D. Drusinsky and M. Shing, TLCharts: Armor-plating Harel Statecharts with Temporal Logic Conditions, Proc. Rapid System Prototyping Conference 2004.
• M Auguston, D. Drusinsky, B. Michael, and N. Rowe- Research on Deception in Defense of Information Systems, Command and Control Research and Technology Symposium (CCRTS) 2004.
• D. Drusinsky, J. B. Michael and M. Shing - Behavioral Modeling and Run-Time Verification of System-of-Systems Architectural Requirements, International Conference on Computing, Communications and Control Technologies: CCCT'04.
• D. Drusinsky, Runtime Monitoring and Software Verification, August 2004, pp. 68-72.
• D. Drusinsky and J.L. Fobes, Executable Specifications: Language and Applications, DoD Crosstalk Magazine, September 2004.
• D. Drusinsky, M. Shing and K. Demir, Test-time, Run-time, and Simulation-time Assertions for RSP., Proceedings of the 16th IEEE International Workshop on Rapid Systems Prototyping, Montreal, Canada, 8-10 June 2005, pp. 105-110.
• D. Drusinsky, Run-time Monitoring of Knowledge Temporal Logic Specifications, 2.nd International Conference on Informatics in Control, Automation and Robotics, Barcelona 2005 (ICINCO 2005), accepted for publication.
• D. Drusinsky, Run-time Monitoring and Recovery of Harel Statecharts using Prioritized Non-deterministic Statechart Specifications, 48.th IEEE International Midwest Symposium on Circuits and Systems, Cincinnati OH, 2005 (MWSCAS 2005), pp. 323-326.
• D. Drusinsky, Model Checking of Statecharts using Automatic White Box Test Generation, 48.th IEEE International Midwest Symposium on Circuits and Systems, Cincinnati OH, 2005 (MWSCAS 2005). pp. 327-332.
• D. Drusinsky and M. Shing, Creation and Evaluation of Formal Specifications for System-of-Systems Development., Proceedings of the 2005 IEEE International Conference on Systems, Man and Cybernetics, Waikoloa, Hawaii, 10-12 October, 2005, pp. 1864-1869.
• D. Drusinsky, D. P. Hinchcliffe, C. Kauffman, E. Stein, G.S. Pringle, Improving Battle Management Software Quality through Formal Specification and Model-Based Development, 4th Annual Missile Defense Conference, April 2006, Arlington, VA.
• K. Demir, D. Drusinsky, M. Shing, Creation and Evaluation of Embedded Assertion Statecharts, 17th IEEE International Workshop on Rapid Systems Prototyping, 2006, Chania, Greece, 14-16 June 2006, pp. 17-23.
• M. Shing, D. Drusinsky and T. Cook, Quality Assurance of the Timing Properties of Real-time, Reactive System-of-systems., Proceedings of the 2006 IEEE International Conference on System of Systems Engineering, Los Angeles, CA, 24-26 April, 2006, pp. 224-229.
• D. Drusinsky "On-line Monitoring of Metric Temporal Logic with Time-Series Constraints Using Alternating Finite Automata", Journal of Universal Computer Science, Vol. 12, No. 5, pp. 482-498.
• M. Shing and D. Drusinsky, Architectural Design, Behavior Modeling and Run-Time Verification of Network Embedded Systems, Proceedings of the Monterey Workshop 2005: Reliable Systems on Unreliable Networked Platforms, Lecture Notes in Computer Science 4322, Springer, 2007, pp. 281-303.
• K. Demir, D. Drusinsky and M. Shing, Creating and Validating Embedded Assertion Statecharts, IEEE Distributed Systems Online, http://dsonline.computer.org/portal/pages/dsonline/2007/05/o5003.html.
• D. Drusinsky and M. Shing, .Verifying Distributed Protocols using MSC-Assertions, Run-time Monitoring, and Automatic Test Generation., Proceedings of the 18th IEEE/IFIP International Workshop on Rapid Systems Prototyping, Porto Alegre, Brazil, 28-30 June 2007, pp. 82-88.
• D. Drusinsky, M. Shing, and K. Demir, "Creating and Validating Embedded Assertion Statecharts," IEEE Distributed Systems Online, 8(5), 2007, art. no. 0705-o5003.
• Tom Cook, D. Drusinsky, and M. Shing, Specification, Validation and Run-time Monitoring of SOA Based System-of-Systems Temporal Behaviors Proceedings of the 2007 IEEE International Conference on System of Systems Engineering, San Antonio, TX, 16-18 April 2007.
• T. W. Otani, M. Auguston, T. S. Cook, D. Drusinsky, J. B. Michael, and M. Shing, "A design pattern for using non-developmental items in real-time Java", Proceedings of the 5th international workshop on Java technologies for real-time and embedded systems (JTRES 2007), Vienna, Austria, September 26 - 28, 2007, pp. 135-143.
• D. Drusinsky and M. Shing, Verifying Distributed Protocols using MSC-Assertions, Run-time Monitoring, and Automatic Test Generation., Proceedings of the 18th IEEE/IFIP International Workshop on Rapid Systems Prototyping, Porto Alegre, Brazil, 28-30 June 2007, pp. 82-88.
• D. Drusinsky, B. Michael, M. Shing, Dimensions of Formal Validation and Verification, Sept, 24, 2007, NASA SAS Workshop on Validation, Morgantown, WV.
• D. Drusinsky, B. Michael, M. Shing, A framework for computer-aided validation, Innovations in Systems and Software Engineering, 4(2), June 2008, pp. 161-168.
• D. Drusinsky, J.B. Michael, T.W. Otani and M. Shing, Integrating Statechart Assertions into Java Components Using AspectJ., Proceedings of the 2008 IEEE International Conference on System of Systems Engineering, Monterey, CA, 2-4 June 2008.
• D. Drusinsky, From UML Activity Diagrams to Specification Requirements, Proceedings of the 2008 IEEE International Conference on System of Systems Engineering, Monterey, CA, 2-4 June 2008.
• D. Drusinsky, B. Michael, T. Otani, M. Shing, .Validating UML Statechart-Based Assertions Libraries for Improved Reliability and Assurance,. Proceedings of the Second International Conference on Secure System Integration and Reliability Improvement (SSIRI 2008), Yokohama, Japan, 14-17 July 2008, pp. 47-51. Best paper award.
• Drusinsky, D. Michael, J. B., and Shing, M. T. , A Visual Tradeoff Space for Formal Verification and Validation Techniques, IEEE Systems Journal, Vol. 2, No. 4, Dec 2008, pp. 513-519. ISSN: 1932-8184.
• Drusinsky, et-al., Removing the Boundaries: steps Toward a Cloud Nirvana,Proc. 2010 IEEE Intl. Conf. on Granular Computing, August 2010, pp. 167-171.
• D. Drusinsky and M. Shing, "Validating Quality Attribute Requirements via Execution-based Model Checking", Proceedings of the 21st IEEE International Symposium on Rapid Systems Prototyping, George Mason University, Fairfax, VA, 8-11 June 2010.
• D. Drusinsky, B. Michael, T. Otani, M. Shing and D. Wijesekera, .Computer-Assisted Validation and Verification of Cybersecurity Requirements,. Proceedings of the 2010 IEEE International Conference on Technologies for Homeland Security, Waltham , MA , 8-10 November, 2010.
• Miriam Alves, Doron Drusinsky, Mantak Shing, Making space systems more dependable: a paradigm change for Verification and Validation, 62nd International Astronautical Congress (IAC), Cape Town, South Africa, October 2011
• D. Drusinsky, TLtoSQL: Rapid post-mortem verification using temporal logic to SQL code generation in the Eclipse PDE," System of Systems Engineering, 2009. SoSE 2009. IEEE International Conference on , vol., no., pp.1-5, May 30 2009-June 3 2009.
• D. Drusinsky., "Guarding the guard: Using meta formal specifications to guard assertions," System of Systems Engineering, 2009. SoSE 2009. IEEE International Conference on , vol., no., pp.1-5, May 30 2009-June 3 2009.
• D. Drusinsky and M. Shing, .Using UML Statecharts with Knowledge Logic Guards., in the Proceedings of the 12th International Conference on Model Driven Engineering Languages and Systems (MODELS 2009), Denver, CO, USA, October 4-9, 2009. Published as the Lecture Notes in Computer Science Vol 5795.
• Drusinsky, et-al., Removing the Boundaries: steps Toward a Cloud Nirvana,Proc. 2010 IEEE Intl. Conf. on Granular Computing, August 2010, pp. 167-171.
D. Drusinsky and M. Shing, "Validating Quality Attribute Requirements via Execution-based Model Checking", Proceedings of the 21st IEEE International Symposium on Rapid Systems Prototyping, George Mason University, Fairfax, VA, 8-11 June 2010.
• D. Drusinsky, B. Michael, T. Otani, M. Shing and D. Wijesekera, .Computer-Assisted Validation and Verification of Cybersecurity Requirements,. Proceedings of the 2010 IEEE International Conference on Technologies for Homeland Security, Waltham , MA , 8-10 November, 2010.
• Miriam Alves, Doron Drusinsky, Mantak Shing, Making space systems more dependable: a paradigm change for Verification and Validation, 62nd International Astronautical Congress (IAC), Cape Town, South Africa, October 2011
• Alves, M.C.B., Drusinsky, D., Shing, M. "A Practical Formal Approach for Requirements Validation and Verification of Dependable Systems", Proceeding of the Fifth Latin-American Symposium on Dependable Computing (LADC 2011), San Jose dos Campos, San Paulo, Brazil, April 25-29, 2011, pp. 47-51. DOI: 10.1109/LADCW.2011.14
• Miriam C. Bergue Alves, Doron Drusinsky, James Bret Michael, Man-Tak Shing, .Formal validation and verification of space flight software using statechart-assertions and runtime execution monitoring,. Proc. 6th International Conference on System of Systems Engineering, Albuquerque, NM, 27-30 June 2011, pp. 155 . 160.
• Doron Drusinsky, James Bret Michael, Thomas Otani, Man-Tak Shing. Putting order into the cloud: Object-oriented UML-based enforcement for document and application organization,. Proc. 6th International Conference on System of Systems Engineering, Albuquerque, NM, 27-30 June 2011, pp. 119 . 124.
• Doron Drusinsky, James Bret Michael, Man-Tak Shing. Rapid runtime system verification using automatic source code instrumentation,. Proc. 6th International Conference on System of Systems Engineering, Albuquerque, NM, 27-30 June 2011, pp. 1 . 6.
• Doron Drusinsky, James Bret Michael, Thomas Otani, Man-Tak Shing. Verification and Validation for Trustworthy Software Systems. IEEE Software, November 2011, pp. 86-92.
• Doron Drusinsky and Mantak Shing, Validating Quality Attribute Requirements via Execution-based Model Checking, Journal of, Software: Practice and Experience, accepted for publication, 2011.

Other

• D. Drusinsky and David Harel. Using Statecharts for Hardware Description and Synthesis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 8(7): 798-807, July 1989.
• D. Drusinsky-Yoresh. Symbolic Cover minimization for Fully I/O Specified Finite state Machines, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 9(7): 779-781, 1990.
• D. Drusinsky-Yoresh. A State Assignment for single-block Implementation of Statecharts. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 10(12): 1569-1575, December 1991.
• D. Drusinsky-Yoresh. Decision Problems for Interacting Finite State Machines. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 10(12): 1576-1578, December 1991.
• D. Drusinsky and David Harel. On the power of bounded concurrency I: Finite Automata. Journal of the ACM, 41(3): 517-539, May 1994.
• D. Drusinsky and M. Shing, Monitoring Temporal Logic Specifications Combined with Time Series Constraints, Journal of Universal Computer Science (JUCS), 9(11), 2003, pp. 1261-1276. (http://www.jucs.org/jucs_9_11/monitoring_temporal_logic_specification)
• G. Brat, D. Drusinsky, D. Giannakopoulou, A. Goldberg, K. Havelund. M. Lowry, C. Pasareanu, A. Venet, W. Wisser, R. Washington, Experimental Evaluation of Verification and Validation Tools on Martian Rover Software, Formal Methods in System Design journal, vol. 25, issues 2-3 (2004), pp. 167-198, 2004.
• D. Drusinsky, On-line Monitoring of Metric Temporal Logic with Time-Series Constraints Using Alternating Finite Automata, Journal of Universal Computer Science, Vol. 12, No. 5 (2006), pp. 482-498.
• K. Demir, D. Drusinsky and M. Shing, Creating and Validating Embedded Assertion Statecharts, IEEE Distributed Systems Online, 8(5), 2007, art. no. 0705-o5003. http://dsonline.computer.org/portal/pages/dsonline/2007/05/o5003.html
• D. Drusinsky, J.B. Michael and M. Shing, A Framework for Computer-Aided Validation, Innovations in Systems and Software Engineering, 4(2), June 2008, pp. 161-168.
• Drusinsky, D. Michael, J. B., and Shing, M.-T. , A Visual Tradeoff Space for Formal Verification and Validation Techniques, IEEE Systems Journal, Vol. 2, No. 4, Dec 2008, pp. 513-519. ISSN: 1932-8184
• Doron Drusinsky, James Bret Michael, Thomas Otani, Man-Tak Shing. Verification and Validation for Trustworthy Software Systems. IEEE Software, November 2011, pp. 86-92.