Unifying Theories of Programming and Testing
- 11:30 13th May 2009 ( week 3, Trinity Term 2009 )Room 478, Oxford University Computing Laboratory
In this talk we present our recent results on integrating theories of testing into Hoare and He's Unifying Theories of Programming (UTP). We show how the notion of conformance in testing relates to notions of refinement in programming. As an example, we discuss "ioco", Tretmans' commonly used input-output conformance relation over reactive processes, and present it in the style of UTP's predicative semantics. The underlying assumptions of this conformance relation are formulated as additional healthiness conditions over the alphabet of traces and refusal sets. This enables formal proofs of ioco-properties, e.g. its relation to CSP's process refinements. After the theory discussion we will give some insights into applications for automated test case generation: We show how automated ioco-checking has been applied in protocol testing and discuss how the theory points to a new test-case generator that is based on SMT solving.
Speaker bio
Dr. Bernhard K. Aichernig is an Assistant Professor at the Institute for Software Technology (IST) of TU Graz. He holds a doctorate and a diploma engineer degree from TU Graz. From 2002-2006 he worked as a Research Fellow at UNU-IIST in Macao S.A.R, China, a research institute on software technology of the United Nations. As an Adjunct Research Fellow he still strongly collaborates with UNU-IIST, e.g. in the EU FP6 project CREDO. He is a board member of Formal Methods Europe (FME), an international organization that promotes well-founded techniques in software engineering and organizes the Formal Methods (FM) conferences. His research focuses on the foundations of software engineering in order to achieve more reliable computer-based systems. He is an expert in formal methods and testing and is the local senior scientist in the FP7 project MOGENTES on the model-based generation of tests for dependable embedded systems.Share this:
