| My research interests are in the areas of:
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
|