|
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 Infinite State Model Checking using Partial Evaluation 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 |
DSSE:Research Projects |
VERTIGO - Verification and Validation of Embedded System Design Workbench |
VERTIGO addresses a new generation of technologies and tools for modelling and testing embedded platforms, that will be the foundation for a viable and cost-efficient mapping of HW/SW systems embedded in intelligent devices. The contributions of the VERTIGO project include: (1) Definition of an HW/SW co-simulation strategy which allows to check the correctness of the interaction between HW and SW through simulation and assertion checking. (2) A verification framework that combines simulation with model checking to reduce verification time and increase coverage. (3) The development of techniques to separate the verification of IPs interaction from the verification of the IP-cores to facilitate efficient design-reuse. (4) Integration of formal and dynamic techniques in a seamless manner and federated around an assertion-based methodology and new coverage metrics. (5) Integrating several state-of-the-art static verification techniques (SAT, High-Level Decision Diagrams, Hierarchical Petri Nets, EFSMs) to the same platform. (6) Bounded and unbounded model checking capability based on SAT, by selecting and extending the most promising existing solutions. (7) The utilization of hybrid solvers in RTL unbounded model checking, by extending previous work on SAT technology and on SAT extensions. Homepage: http://www.vertigo-project.eu/Type: Normal Research Project Research Group: Dependable Systems & Software Engineering Themes: Formal Methods, Design, Automation, Simulation and Optimisation Dates: 1st June 2006 to 30th November 2008 Partners
Funding
Principal Investigators
Other Investigators
|