|
|
Automated Validation of Business Critical Systems with Component Based Designs COCONUT: A Correct-by-Construction Workbench for Design and Verification of Embedded Systems High-Integrity Component-Based Engineering for Enterprise Systems Methodologies and Technologies for Industrial Strength Systems Engineering Modelling and analysis of long running transactions NOTOS: New algOrithm for LTL mOdel checking with Satisfiability Paradigm Unifying System Specification Environments for proven Electronic design Rigorous Open Development Environment for Complex Systems (RODIN) Trusted Software Agents and Services Verifying Shared Memory Communication for Low-Power Multi-core SoCs VERTIGO - Verification and Validation of Embedded System Design Workbench Automated Validation of Business Critical Systems with Component Based Designs Customization and Adaptation of Automatically Generated Code High-Integrity Component-Based Engineering for Enterprise Systems Methodologies and Technologies for Industrial Strength Systems Engineering RICES Reasoning about Information Consistency across Enterprise Solutions Automated Validation of Business Critical Systems with Component Based Designs NOTOS: New algOrithm for LTL mOdel checking with Satisfiability Open Middleware Infrastructure Institute RICES Reasoning about Information Consistency across Enterprise Solutions Towards a Modular Approach to Model-Based Verification: logical, semantical and algorithmic support |
|
Infinite State Model Checking using Partial Evaluation |
Motivation: The past years have seen dramatic growth in the application of model checking techniques to the validation and verification of hardware systems. However, despite the success of model checking, most systems must be substantially simplified (i.e., abstracted) and considerable human ingenuity is still required. Furthermore, most software systems cannot be modelled directly by a finite state system: as soon as some kind of recursion, dynamic or unbounded data structures come into play, an infinite number of states must be verified. Description The main objective of the project is to study the potential of automatically deriving abstractions for infinite model checking through a combination of existing technology for the automatic control of partial evaluation and abstract interpretation. First successful experiments of this idea have been conducted using the ECCE and LOGEN tools. The project consists of a theoretical study coupled with the implementation of a combined partial evaluation and abstract interpretation system (based upon ECCE). The practicality of the approach will be gauged on realistic examples, some of them coming from the EPSRC funded ABCD projet for the validation of business-critical systems. Homepage: http://www.ecs.soton.ac.uk/~mal/ISM.htmlType: Normal Research Project Research Group: Dependable Systems & Software Engineering Themes: Formal Methods, Software Engineering, E-Business Technologies Dates: 1st August 2000 to 30th May 2002 Funding
Principal Investigators
Other Investigators
|
