Faculty
NPS - Faculty Profiles - Heading
Faculty Profile Directory
FacultyCV
Back
Overview
1988: Ph.D. Computer Science, Weizmann Inst. of Science, Rehovot, Israel. Gad Reshef Award.
1988-1993: Sony Semiconductor Division (Atsugi, Japan, and San-Jose, CA) -researcher.
1993-1997: R-Active Concepts, Inc, where I was owner and CEO. R-Active’s BetterState tool had thousands of seats and received two EDN awards.
1997-2000: ISI Inc. Acquired BetterState. I joined ISI as software architect. ISI’s BetterState was used by GM, Honda, Nissan, Mazda, NASA, and other automotive, semiconductor and aerospace companies.
2000-2018: owner and CEO of Time Rover, Inc., and Maya Software Inc.
These companies developed two tools:
1. The TemporalRover: the first run-time formal verification tool based on Metric Temporal Logic (MTL).
2. The StateRover: a UML-based design, code generation, and formal runtime formal verification tool, implemented as a set of plugins for the Eclipse IDE. The StateRover was in active use by NASA and the Missile Defense National Team until 2018.
2002-Present: Professor of computer science at NPS.
2010: Participated in NASA’s investigation of the Toyota Runway Acceleration.
2018-Present: Chief Science Officer at Aerendir, Inc., Mountain View, Calif.
2021-Present: Algorithms Column Editor, IEEE Computer Society’s Computer Magazine (https://www.computer.org/csdl/magazine/co)
1988-1993: Sony Semiconductor Division (Atsugi, Japan, and San-Jose, CA) -researcher.
1993-1997: R-Active Concepts, Inc, where I was owner and CEO. R-Active’s BetterState tool had thousands of seats and received two EDN awards.
1997-2000: ISI Inc. Acquired BetterState. I joined ISI as software architect. ISI’s BetterState was used by GM, Honda, Nissan, Mazda, NASA, and other automotive, semiconductor and aerospace companies.
2000-2018: owner and CEO of Time Rover, Inc., and Maya Software Inc.
These companies developed two tools:
1. The TemporalRover: the first run-time formal verification tool based on Metric Temporal Logic (MTL).
2. The StateRover: a UML-based design, code generation, and formal runtime formal verification tool, implemented as a set of plugins for the Eclipse IDE. The StateRover was in active use by NASA and the Missile Defense National Team until 2018.
2002-Present: Professor of computer science at NPS.
2010: Participated in NASA’s investigation of the Toyota Runway Acceleration.
2018-Present: Chief Science Officer at Aerendir, Inc., Mountain View, Calif.
2021-Present: Algorithms Column Editor, IEEE Computer Society’s Computer Magazine (https://www.computer.org/csdl/magazine/co)
NPS Experience
- Unknown - current: Professor
Other Experience
- 2021 Editor, IEEE
- 2000 - 2002 Consultant, Xerox Palo Alto Research Center, DHL
- 1999 President, Time Rover, Inc.
- 1997 - 1999 Software architect, BetterState product, Integrated Systems Inc. (ISI)
- 1992 - 1997 President, R-Active Concepts, Inc.
Research Interests
Formal Methods and Formal Verification
Run-time Verification
Verification of cyber-physical systems
Real Time Model Checking
Machine-learning for biometric authentication
Biometric authentication integrated with cryptographic protocols
Cyber Security techniques
Applications of signature schemes such as blind signatures
Theoretical computer science
Run-time Verification
Verification of cyber-physical systems
Real Time Model Checking
Machine-learning for biometric authentication
Biometric authentication integrated with cryptographic protocols
Cyber Security techniques
Applications of signature schemes such as blind signatures
Theoretical computer science
Teaching Interests
Algorithms
Automata Theory and Formal Languages
Model Checking and Run-Time Verification of Safety Critical Systems Principles of Software Design
Principles of Programming Languages
Introduction to Software Engineering
Automata Theory and Formal Languages
Model Checking and Run-Time Verification of Safety Critical Systems Principles of Software Design
Principles of Programming Languages
Introduction to Software Engineering
Awards
- 1988 - Gad Reshef Award, Weizmann Institute of Science, Statecharts
Scholarly Work
Publications
- Journal Articles
- Drusinsky, D, Runtime Feature Blocking and Risk Reduction using Runtime Bayesian-Logic Reasoning. Innovations in Systems and Software Engineering.
- Drusinsky, D, Run-Time Monitoring using Bounded Constraint Instance Discovery within Big Data Stream. Innovations in Systems and Software Engineering, 2(12), 141–151.
- Michael, J. B., Dinolt, G. W., & Drusinsky, D, (2020). Open questions in formal methods. Computer, 05(53), 81-84.
- Drusinsky, D., & Michael, J. B, (2020). Obtaining Trust in Executable Derivatives Using Crowdsourced Critiques With Blind Signatures. Computer, 04(53), 51-56.
- Drusinsky, D, (2017). Reverse engineering concurrent UML state machines using black box testing and genetic programming. Innovations Syst Softw Eng, 2-3(13), 117–128.
- Drusinsky, D, (2017). Library-based Visual Formal Specification Monitoring System for Monitoring Log-Files with Visible and Hidden Data. Innovations in Systems and Software Engineering, 1(13), 67–79.
- Drusinsky, D, (2015). Run-time monitoring using bounded constraint instance discovery within big data streams. Innovations in Systems and Software Engineering, 1-11.
- Technical Reports
- Drusinsky, D, (2018). Dynamic Feature Monitoring and Blocking: Phase 1.