**2013**

- Needham security protocol and Lowe attack
- References:
- Needham and Schroeder, Using encryption for authentication in large networks of computers, Comm ACM, Vol 21, no 12, pp 993-999, 1978.
- Gavin Lowe, An attack on the Needham-Schroeder public key authentication protocol, Inform. Processing Letters, V 56, No 3, pp 131-133, 1995.
- Bully algorithm
- Bully algorithm assumes that nodes are fully connected
- Reference Bully alg: Garcia-Molina, Elections in a distributed computing system, IEEE Transactions on Computers, CC-31, no 1, pp 4, 1982. – Also: Modified bully election algorithm in distributed systems, WSEAS Tr. on Inf. Science and Appl, Vol 2, no 8, 2005.
- Find center of tree (using Spin)
- Algorithm described in book: N. Santoro, Design and Analysis of Distributed Algorithms, 2007
- Termination check for Khaled’s algorithm
- Modeling and analyzing the Yo-Yo Protocol for leader selection using Spin
- Yo-Yo works on a mesh network, nodes have identities
- Algorithm described in book: N. Santoro, Design and Analysis of Distributed Algorithms, 2007

**2012**

- Verification of a network broadcast algorithm using SPIN
- Electronic Warfare System: UPPAAL Modeling
- Modeling a memory access protocol for multi-CPU computers

**2011**

- Modelling and Validation of Distributed Bitonic Mergesort Algorithm using SPIN
- Modelling the focused addressing and bidding algorithm using the Telelogic TAU tool for SDL
- Reference: Ramamritham, Stankovic, Distributed scheduling of tasks with deadlines and resource requirements, IEEE Tr. On Computers, Vol 38, No 8, 1989
- Modelling and Validation of Distributed Algorithm for Finding Shortest Path using Spin
- Reference: K.M. Chandy and J. Misra, Distributed computation of graph: Shortest path algorithms
- Modelling and Validation of Distributed Algorithm for Deadlock Detection using Spin
- References:
- Bracha, Toueg, Distributed deadlock detection, Distr. Computing, 2, pp 127-138, 1987
- Kshemkalyani, Singhal, Distributed detection of generalized deadlocks, in Proc. 17th Int. Conf. on Distributed Computing Systems (ICDCS), May 1997.
*plus two other projects*

**2010**

- Modelling and Analyzing Distributed Algorithm for Minimum-Weight Spanning Trees (MSTs) [1] using the SPIN Tool
- Alg. described in: Gallager, Humblet, Spira, A distributed algorithm for mini um-weight spanning trees, ACM Transactions on Programming languages and Systems, Vol 5, No 1, pp 66-77, 1983
- Model checking the SIP protocol using SPIN
- SIP described in : Rosenberg, Schulzrinne, Camarillo, SIP: Session Initiation Protocol, RFC 3261, 2002
- Modeling of a Simple in-flight safety system Using Alloy
- Modeling B-tree structures for peer-to-peer systems in Allow

**2009**

- Satisfying Concurrency Control Requirements in Design of Databases (step-wise development of distributed algorithm) using a tool for Colored Petri-nets
- Modeling the Selectively Reliable Multicast Protocol using the SPIN tool
- Analysis of “Component Design Derived from Global Specification” (one of the last course chapters) modeling some examples of distributed component designs using Telelogic SDL tool.
- Modeling and analyzing the Yo-Yo Protocol for leader selection using the Alloy tool
- Modeling and analyzing the Bully algorithm for leader selection using the Telelogic Tau tool

**2008**

- Deriving the behavior of a controller for controlling the temperature of a chemical plant (using the IOA tool of Drissi)
- Modeling the SIP call waiting feature (using the Telelogic SDL tool)
- Modeling a protocol (developed within this project) for making reservation of resources in a distributed environment (using the SPIN tool)

**2007**

- Modeling the SIP protocol (IP telephony) using the SPIN tool
- Modeling a cruise control system using the LTSA tool (verification of safety and progress properties)
- Modeling in SDL of a distributed database system providing the so-called Practical Byzantine Fault Tolerant Service (using the Telelogic SDL tool)
- Modeling a version of CSMA/CD in SDL for checking functional properties and certain performance parameters (using the Telelogic SDL tool)
- Modeling the Small Aircraft Landing Protocol (defined for the Small Aircraft Transportation System) using the Alloy tool
- Modeling the SIP three-way conference call feature (using the Telelogic SDL tool)