Current Projects


Orc is a theory of orchestration of services. It was proposed by J. Misra to model Internet-like, wide-area computations. In this project, we investigate the real-time operational semantics of Orc within the K framework using the K-tool.

Sequence Diagram Extensions for Program Comprehension

We develop in this project novel extensions to sequence diagrams that reflect more accurately the control-flow structure of programs to improve program comprehension, and demonstrate the value of these extensions through case studies and experimental evaluation.


This project investigates the real-time operational semantics of Orc within the rewriting logic formalism, using Maude and its real-time extension in Real-Time Maude. The project aims at building an efficient formal analysis and verification environment for Orc programs. A propotypical implementaion for such an environment has been recently made available in the web-based tool MOrc, which is accessible online here.


An architecture-independent parallelization of the VeStA tool, in which statistical model checking of CSL/PCTL formulas and statistical quantitative analysis of formulas in QuaTEx is performed in parallel. The tool can utilize several parallel architecutres, from muti-core nodes to multi-node clusters, to significantly decrease the time required to complete these usually demanding verification tasks. The tool's web page is located here.

Formal Analysis of DoS Counter Measures

The formal specification and statistical model-checking and quantitative analysis of various forms of DoS attacks (such as amplification attacks) and their counter-measures, such as the Adaptive Selective Verification protocol, using Maude and PVeStA.

Previous Projects


The project studies the formal semantics of Prolog, a representative logic programming language, in rewriting logic. See the MProlog page for more details.

Identity-Based Message Key Distribution

The project investigates the feasibiltiy of applying identity-based encryption techniques to messaging to minimize the need for long-lived keys.

Get in touch!

Dr. Musab A. Alturki
King Fahd University of Petroleum and Minerals
P.O. Box 840, Dhahran 31261
Saudi Arabia

Office: +966 3860-7185
Fax: +966 3860-2174

Find me on ...