DigiCosme Tutorial "Model-based Testing"

The course will take place at Supelec, Amphi F3-05, 23.4.13, 9:00 - 12:30. Many testing techniques vitally depend on symbolic computation and constraint-solving techniques. Their limits therefore represent limits for testing as a whole. The HOL-TestGen system is designed as plug-in into the state-of-the-art theorem proving environment Isabelle/HOL. Thus, powerful modeling languages as well as powerful automated and interactive proof methods for constraint resolution are available. HOL-TestGen has been applied in unit, sequence, and reactive sequence black-box test scenarios in substantial case studies. Conceptually, it offers a quite unique combined view on these areas traditionally considered separately. Moreover, it bridges the gap to traditional program verification by concepts such as 'explicit test hypothesis'. The tutorial is going to be a guided tour through theory, pragmatics, and case-studies.

Tutorial Material:



Downloads:


Downloads : Isabelle (Use Version 2011-1!) , HOL-TestGen
More from the HOL-TestGen Website.

Bibliography:


2013

2012

2011

2010

2009

2008

2007

2005

2004