ALBCOM Seminar: Axiom-based testing
- https://computing.phd.upc.edu/en/events/albcom-seminar-axiom-based-testing
- ALBCOM Seminar: Axiom-based testing
- 2011-04-27T12:00:00+02:00
- 2011-04-27T13:00:00+02:00
When
Apr 27, 2011 from 12:00 PM to 01:00 PM (Europe/Madrid / UTC200)
Where
Room S208 (floor -2), Omega Building, UPC, Barcelona
Add event to calendar
Speaker: Magne Haveraaen, Bergen Language Design Laboratory, University of Bergen, Norway
Abstract: Axiomatic specifications are considered part of the formal methods community, while testing is considered as belonging to software practice. When using axioms as basis for testing, an idea that goes back to the 1980s, we get a very powerful mechanism for improving software quality.
This presentation will start with some real-life examples where we have used axioms for developing software. The examples are from two widely different problem domains, the numerical domain of PDEs, and a multi-threaded software component of a science centre exhibit.
We then discuss some of the underlying ideas. One aspect is using a programming language compatible semantics for the axioms, not the idealised set-theoretical one that is standard from formal methods. Another concerns the integration of axiom-based testing with unit testing tools. Here we demonstrate our tool JAxT, and how we have taken the (informal) specification of the Java standard libraries and converted this into testable axioms. We then see how limitations of programming languages, e.g., the lack of signature morphisms, make full reuse of axioms difficult.
Abstract: Axiomatic specifications are considered part of the formal methods community, while testing is considered as belonging to software practice. When using axioms as basis for testing, an idea that goes back to the 1980s, we get a very powerful mechanism for improving software quality.
This presentation will start with some real-life examples where we have used axioms for developing software. The examples are from two widely different problem domains, the numerical domain of PDEs, and a multi-threaded software component of a science centre exhibit.
We then discuss some of the underlying ideas. One aspect is using a programming language compatible semantics for the axioms, not the idealised set-theoretical one that is standard from formal methods. Another concerns the integration of axiom-based testing with unit testing tools. Here we demonstrate our tool JAxT, and how we have taken the (informal) specification of the Java standard libraries and converted this into testable axioms. We then see how limitations of programming languages, e.g., the lack of signature morphisms, make full reuse of axioms difficult.
Share: