Mustafa Al-Lail
PhD Candidate
Department of Computer Science
Colorado State University
Office: CSB 325
Phone: (425) 524-7803

I am a PhD candidate in the department of Computer Science at Colorado State University, Fort Collins, CO, USA. I have just completed a one-year full time lecturer position at the Department of Computer Science & Software Engineering, Seattle University. I had been co-supervised by Dr. Robert B. France, the renowned professor of Software Engineering, and Dr. Indrakshi Ray, a distinguished professor in cybersecurity.   Before enrolling in graduate school, I had spent a number of years working as a senior network engineer.


My research focuses on developing new techniques for specification, validation, and verifications of software and access control systems. Specifically, I am interested in the following areas of software and system development: 


1- Model-Driven Software Engineering

My main research area is in model-driven development that aims to reduce the significant effort associated with developing and analyzing complex software systems through the creation and manipulation of software models. My current research focuses on developing techniques and tools to (1) formally specify and analyze temporal properties of software properties using models, (2) domain-specific modeling languages, and (3) scaling the analysis to large models using model slicing techniques.


2- Access Control Models

Access control models are used to mitigate the risks of unauthorized access to data, resources, and systems. My research focuses on developing new models that address the new emerging access control problems for the spatiotemporal requirement, workflow systems, and access control domain specific languages.


3- Formal Specification, Verification, and Validation of Software Systems

Formal methods research aims to improve the reliability and robustness of design through employing mathematical techniques for specification, validation, and verification of hardware and software systems. My current research focus on integrating different formal techniques (such as model checking, automated theorem proving, etc..) with software modeling technologies. Additionally, I investigate the development of new specification languages, verification techniques and tools.



         Mustafa Al-Lail, Wuliang Sun, Robert B. France, "Analyzing Behavioral Aspects of UML Design Class Models Against Temporal Properties", in Proceedings of The 14th International Conference on Quality Software (QSIC 2014), Dallas, Texas, USA October 2014, 196-201

         Ramadan Abdulnabi, Mustafa Al-Lail, Indrakshi Ray, Robert B. France, "Specication, Validation, and Enforcement of a Generalized Spatio-Temporal Role-Based Access Control Model" IEEE Systems Journal 7(3), 501-515 (2013)

         Mustafa Al-Lail, Ramadan Abdunabi, Robert B. France, Indrakshi Ray : An Approach to Analyzing Temporal Properties in UML Class Models, in Proceedings of ModelMoDeVVa@MoDELS 2013: 77-86

          Mustafa Al-Lail," A Framework for Specifying and Analyzing Temporal Properties of UML Class Models". Demos/Posters/StudentResearch@MoDELS 2013: 112-117

         Mustafa Al-Lail, Ramadan Abdunabi, Robert B France, Indrakshi Ray, 2013,"Rigorous Analysis of Temporal Access Control Properties in Mobile Systems", in Proceedings of 18th IEEE International Conference on the Engineering of Complex Computer Systems, Singapore July 2013, 246-25

 My ResearchGate