Details of Grant 

EPSRC Reference:	EP/D50595X/1
Title:	Efficient Specification Pattern Library for Model Validation
Principal Investigator:	Huth, Professor MR
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	Computing
Organisation:	Imperial College London
Scheme:	Standard Research (Pre-FEC)
Starts:	01 October 2005	Ends:	30 September 2008	Value (£):	87,942
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	Communications Information Technologies
Related Grants:
Panel History:
Summary on Grant Application Form
Todays and tomorrows software and hardware are too complex to guarantee their reliable functioning by merely inspecting their components through established quality assurance techniques, e.g. manual code inspection. Such computational systems are increasingly embedded in devices unbeknownst to users who nonetheless rely on the correct behaviour of these systems. Electronic control units in cars, implanted sensors for monitoring medical conditions, and electronic purses are such examples of small devices with complex interaction of hardware and software.Recently, researchers and developers have recognized that testing and validation of such systems benefits greatly from the creation of models for such systems and the exposure of these models to formal simulation and analysis. Typical questions one has about such models are: Is it possible to reach an unsafe state from a safe state in the model (e.g. get an electronic purse to exceed its credit limit)? If the model has reached an unsafe state, is there always a model evolution from that state onwards back to a safe state? Is the model capable of generating a certain scenario, expected from the actual system it models (i.e. is the model consistent with a certain simulation run, e.g., the seizure of a bank card after a multiply repeated input of a flawed PIN number)? Etc.Any answers to the questions above will be answers about models, so models need to capture well the systems they mean to represent. Equally, not all aspects of systems may be known prior to their completion but pre-production validations can safe huge costs (e.g. it is very expensive to fix a flawed chip for a new PC generation once it has been burned ).Both concerns are addressed by abstracting state and behaviour of systems and models into three values: true (present in the system or model), false (absent in the system or model), and unknown (may or may not be present in the system or model). Answers to questions then also have these three possible values.The lack of complete knowledge about systems or models, represented by unknown, means that answering questions such as the above consumes too many computational resources to be viable in practice. Alternative and sound ways of answering are available that interpret logical connectives such as and and or in a compositional manner. This often results in answers unknown although to real answer for the more expensive analysis is true or false. For example, p or not p ' is always true but returns unknown for the cheaper analysis if p is unknown. This research will establish for which patterns of questions the cheaper analysis is optimal and precise in that its findings equal those of the much more expensive analysis. These findings will marry the efficiency of the analysis with the reasoning power of the more expensive one.
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.imperial.ac.uk