My research interests are in the areas of:

• The design and verification of distributed multiprocessor systems.
• Design Methodologies including formal methods.
  
• Defining and Describing Distributed Services.
• AI in Games of Strategy.

Modern society has become reliant on software systems for many mission-critical and life-critical functions. One approach to verifying these software systems is to use formal mathematical logics, theorem provers and model checkers. My work has used a variety of formalisms such as Mixed Intuitionistic Linear Logic (MILL) and variants of the pi-calculus for the specification and verification of mission critical distributed systems as typified by communications and security protocols. As part of the Enterprise Ireland funded research project IMPROVE, I am working on the specification and verification of the family of protocols that can be found in modern Public Key Infrastructures.

In isolation, these formalisms will be of little practical value unless they are integrated into a design methodology that covers the complete development cycle from analysis, design, development and verification. These design methodologies have to be "designer-friendly". I have been involved in several national and international projects that address this and related issues. The goal of these projects is to develop object-oriented methodologies to aid a designer in bringing a design from initial requirements specification to a formal model.

In the area of web services, the Client-Server Matching project is investigating ways to provide a web-based framework to allow users to have universal access to web services from various access devices possibly via a series of intermediate services. This framework is dynamic and requires minimal configuration, but is still flexible enough to offer universal access as new applications/services and access devices are developed.

I am also interested in applications of Artificial Intelligence (AI) in Strategic Games. Although significant advances have been made in computer Chess, there is still a long way to go in the development of "intelligent" search algorithms for computer games, particularly games of strategy. My research analyses existing "expert" games to find recurrent partial patterns and their outcomes. When these partial positions re-occur, their associated outcomes are used to forward prune the search tree.

Publications:

Journals

• Bai L, Lao S, Smeaton A.F, O'Connor N, Sadlier D and Sinclair D. 2009. Semantic Analysis of Field Sports Video Using a Petri-Net of Audio-Visual Concepts. Computer Journal
• Clarke S., Fitzgerald B Nixon P., Pohl K., Ryan K., Sinclair D. and Thiel S.. 2009. The Role of Software Engineering in Future Automotive Systems Development. Sae International Journal Of Passenger Cars Electronic And Electrical Systems, 1, 1, pp544-552.
• Sinclair D. and Power J. 2005. Specifying and Verifying Communications Protocols using Mixed Intuitionistic Linear Logic. Electronic Notes in Theoretical Computer Science. Volume 133, Edited by J. Bicarregui; A. Butterfield; A. Arenas., , pp255-273.
• J.F. Power and D. Sinclair. 2004. A Formal Model of Forth Control Words in the Pi-Calculus. Journal Of Universal Computer Science, vol 10, issue 9, , pp1272-1293.
• Sinclair D. 1998. The GST load balancing algorithm for parallel and distributed systems. International Journal Of Approximate Reasoning, 19,, pp39-56.

Refereed Conference Proceedings

• Clarke S., Fitzgerald B., Nixon P., Pohl K., Ryan K., Sinclair D. and Thiel S. , The Role of Software Engineering in Future Automotive Systems Development, SAE World Congress & Exhibition, 14-APR-08 - 17-APR-08, Detroit, MI, USA
• Jiao D., Sinclair D., Weakest Preconditions for Applied pi-Calculus, International Multi-Conference on Computing in the Global Information Technology (ICCGI'07), 04-MAR-07 - 09-MAR-07, Guadeloupe, French Caribbean
• Lyttleton O., Sinclair D. and Tracey D., Mediating between Heterogeneous Ontologies using Schema Matching Techniques, IEEE Information Reuse and Integration 2005 (IRI05), 15-AUG-05 - 17-AUG-05, Los Vegas
• David Sinclair, David Gray and Geoff Hamilton, Synthesising Attacks on Cryptographic Protocols, 2nd International Conference on Automated Technology for Verification and Analysis (ATVA 2004), 31-OCT-04 - 03-NOV-04, Taipei, Taiwan
• David Sinclair and James Power, Specifying and Verifying Communications Protocols using Mixed Intuitionistic Linear Logic, 9th International Workshop of Formal Methods in Industrial Critical Systems (FMICS 2004), 20-SEP-04 - 21-SEP-04, Linz, Austria
• Frédéric Oehl, David Sinclair, Olga Kouchnarenko and Gérard Cece, Automatic Approximation for the Verification of Cryptographic Protocols, Formal Aspects of Security, 18-DEC-03 - 20-DEC-03, London
• Frédéric Oehl and David Sinclair, Combining ISABELLE and Timbruk for Cryptographic Protocol Verification, Workshop on Internet Security Communication (SECI) 2002, 19-SEP-02 - 21-SEP-02, Tunis, Tunisia
• Frédéric Oehl and David Sinclair, Combining Theorem Prover and Model Checker to verify Cryptographic Protocols, Modelling and Verification of Parallel Processes, 17-JUN-02 - 21-JUN-02, Nantes, France
• Frederic Oehl and David Sinclair, Combining two approaches for the verification of cryptographic protocols, Specification and Verification of Emerging Systems, 01-DEC-01 - 01-DEC-01, Paphos, Cryprus
• Benyamin Aziz, David Gray, Geoff Hamilton, Frederic Oehl and David Sinclair, Implementing Protocol Verification for E-Commerce, Advances in Infrastructure for Electronic Business, Science, and Education on the Internet, 06-AUG-01 - 12-AUG-01, L'Aquila, Italy
• James Power and David Sinclair, A Formal Model of Forth Control Words in the Pi-Calculus, 6th International Workshop on Formal Methods for Industrial Critical Systems, 16-JUL-01 - 17-JUL-01, Paris, France
• David Gray, Geoff Hamilton, James Power, David Sinclair, A Specification of TCP/IP using Mixed Intuitionistic Linear Logic, IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems, 18-APR-01 - 20-APR-01, Washington DC
• David Sinclair, James Power, Paul Gibson, David Gray, Geoff Hamilton, Specifying and Verifying IP with Linear Logic, IEEE International Workshop on Distributed Systems Validation and Verification, 10-APR-00 - 10-APR-00, Taipei , Taiwan
• David Sinclair, James Power, Paul Gibson, David Gray, Geoff Hamilton, Four Logics and a Protocol, 3rd. Irish Workshop in Formal Methods, 01-JUL-99 - 02-JUL-99, Galway, Ireland
• David Sinclair, Using Example-Based Reasoning for Selective Move Generation in Two-Player Adversarial Games, 4th European Workshop on Case-Based Reasoning; Lecture Notes in Artificial Intelligence 1448, 23-SEP-98 - 26-SEP-98, Dublin, Ireland
• David Sinclair, Using an Object-Oriented Methodology to bring a Hybrid System from Initial Concept to Formal Definition, Hybrid and Real-Time Systems, 26-MAR-97 - 28-MAR-97, Grenoble, France
• David Sinclair, The GST Load Balancing Algorithm for Parallel and Distributed Systems, 1st International Workshop on Approximate Reasoning in Scheduling, 11-FEB-97 - 11-FEB-97, Zurich, Switzerland
• D.Sinclair, L. Cuypers, K. Verschaeve, E. Holz, A. Birbas, V. Mariatos, N. Kyrloglou, J-L Roux , A formal approach to HW/SW co-design: the INSYDE project, IEEE Symposium and Workshop on Engineering of Computer-Based Systems, 11-MAR-96 - 15-MAR-96, Friedrichshafen, GERMANY
• D.Sinclair, B. Stone and G. Clynch, An Object Oriented Methodology from Requirements to Validation, 2nd Object Oriented Information Systems Conference, 18-DEC-95 - 20-DEC-95, Dublin, Ireland
• D.Sinclair, E. Holz, D. Witaszek, M.Wasowski, Validation of hybrid systems by co-simulation, Hybrid Systems III, 22-OCT-95 - 25-OCT-95, New Jersey, USA
• David Sinclair, Synthesis of 2-Dimensional Grey Scale Filters by 3x3 Cellular Autamata, 3rd International Workshop on Parallel Image Analysis, 07-JUN-94 - 09-JUN-94, Maryland, USA