Quality of Service: Modelling, Design and Analysis (Model Checking)

 

The specification and implementation of QoS in distributed systems is increasingly important, due to the need to address questions of performance. Designing a distributed system often involves breaking the system into smaller entities such as objects, components and services. In [1,2,3] we present a method of design and modelling of QoS using ODP. However, models of QoS-enabled systems are complex and must be analyzed to ensure their correctness. . In collaboration with Osaka University, we have developed a method of verification of Timeliness properties, such as throughput, latency and jitter [4,5]. Recently, we have furthered this approach to create intelligent autonomic QoS managers for wireless systems, which extends existing industrial architectures such as ITSUMO [6,7,8].

This research is in collaboration with Kozo Okano's team at Osaka University and, among other things, has resulted in tool for static analysis if Timed Automata via Rational Presburger Arithmetic. We have implemented the approach in a tool called Time Action Lock Checker (TALC). I also collaborate on this topic with Rachid Anane, Coventry University, UK.

 

Selected publications

  1. A UML approach to the design of open distributed systems. B. Bordbar, J. Derrick, and G. Waters. In Chris George and Huaikou Miao, editors, Formal Methods and Software Engineering, volume 2495 of Lecture Notes in Computer Science, pages 561-572. Springer, November 2002.

  2. Using UML to specify QoS constraints in ODP. B. Bordbar, J. Derrick, and A. G. Waters. Computer Network and ISDN systems, 40, pages 279-304, 2002

  3. Design Support for Distributed Systems: DSE4DS. D.H. Ake hurst, B.Bordbar, J.Derrick, and A.G.Waters. In J.Finney, M.Haahr, and A.Montressor, editors, Proceedings of the 7th Cabernet Radicals Workshop, October 2002.

  4. Verification of Timeliness QoS Properties in Multimedia Systems . B. Bordbar and K. Okano, Proceeding of 5th International Conference on Formal Engineering Methods, LNCS Vol. 2885, pp 523-540, 2003

  5. Testing Deadlock-freeness in Real-time Systems; A Formal Approach. B. Bordbar and K. Okano. 4th International Workshop on Formal Approaches to Testing of Software, FATES 2004, LNCS 3395, pp.95-109 (Sep. 2004).

  6. An Architecture for Automated QoS Resolution in Wireless Systems, B. Bordbar and R. Anane, Proceeding of the IEEE AINA 2005, International Workshop on Web and Mobile Information Systems (WAMIS), March 2005, Taipei, Taiwan, 774-779

  7. An Evaluation Mechanism for QoS Management in Wireless Systems, B. Bordbar, R. Anane and K.Okano, International Workshop on Performance Modelling in Wired, Wireless, Mobile Networking and Computing 2005, In Proc. of ICPADS 2005 Vol.II pp.150-154 (Jul. 2005)

  8. A Timed Automata Approach to QoS Resolution, B. Bordbar, R. Anane and K. Okano, International Journal of Simulation, Systems, Science and Technology, Vol. 7, No 1, pages 46-54, 2006 An extended version of this

  9. A Model Driven Approach to the Analysis of Timeliness Properties, M. A. Ameedeen, B. Bordbar and R. Anane, European Conference on Model Driven Architecture Foundations and Applications (ECMDA-FA 09), LNCS, Vol. 5562, pages 221-236, 2009