Details of Grant 

EPSRC Reference:	GR/S86211/01
Title:	New-Generation Symbolic Model Checkers for Verifying Asynchronous Systems
Principal Investigator:	Luettgen, Professor G
Other Investigators:
Researcher Co-Investigators:
Project Partners:	College of William and Mary
Department:	Computer Science
Organisation:	University of York
Scheme:	Standard Research (Pre-FEC)
Starts:	01 September 2004	Ends:	31 August 2007	Value (£):	184,746
EPSRC Research Topic Classifications:	Software Engineering
EPSRC Industrial Sector Classifications:	Information Technologies
Related Grants:
Panel History:
Summary on Grant Application Form
This proposal is devoted to the development, implementation, and assessment of new-generation symbolic model checkers for verifying event-based asynchronous systems, such as distributed embedded software. It involves a research collaboration of the PI with the US co-author, for whose activities the US National Science Foundation has recently awarded funding. The project's principal aim is to overcome the severe time- and memorydeficiencies of current BDD-based model-checking techniques when verifying asynchronous systems. This will be achieved by employing MDDs and Kronecker-based data structures for storing state spaces and system transitions, respectively, which will permit one to systematically exploit the event locality that is inherent in asynchronous systems in such a way that model checking only requires local manipulations of these data structures. Key project goals include the devising of parallelisations of model-checking algorithms based on these ideas, their formal proof of correctness, and their implementation in the form of C++ packages that will also be made web-accessible for remote execution. The performance of the developed model checkers will be assessed by extensive benchmarking and by comparison to existing state-of-the-art model checkers, and our algorithms' practicality will be tested by applying them to a realistic case study involving the formal analysis of human-computer-interaction aspects in aircraft cockpits.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.york.ac.uk