Revision as of 06:19, 28 June 2014

4th Halmstad Summer School on Testing, HSST 2014

June 9-12, 2014 - Halmstad University, Sweden

HSST 2014 Group Photo.

HSST 2015

Introduction

Testing and debugging account for a major part of software development cost and effort, yet the current practice of software testing is often insufficiently structured and disciplined. There have been various attempts in the past decades to bring more rigour and structure into this field, resulting in several industrial-strength processes, techniques and tools for different levels of testing. The 4th Halmstad Summer School on Testing provides an overview of the state of the art in testing, including theory, industrial cases, tools and hands-on tutorials by internationally-renowned researchers.

Abstracts, Slides and Recorded Videos

Automated Test Generation via Satisfiability Modulo Theory Solvers

Thomas Ball, Microsoft Research

Satisfiability Modulo Theory (SMT) solvers power a new generation of modeling, verification, and testing tools. I will focus attention on the use of SMT solvers in automated test generation tools (specifically the SAGE and Pex tools from Microsoft) and how interpolating solvers can be used to bridge the gap between testing and verification. No previous knowledge of SMT solvers is assumed.

Power Point Slides

Recorded Video Part I

Recorded Video Part II

Model-Based Testing, the Difference between Theory and Practice

Machiel van der Bijl, Axini BV

Model-based testing has been around for at least 20 years, at least in academia. It solves a problem that is recognized by the industry: thorough testing of (complex) software/hardware systems. When one explains model-based testing to an engineer from another engineering discipline, say construction, the question is always asked why the technique is not used in practice.

This lecture will focus on applying model-based tested to industry grade systems. It will be a combination of theory combined with the practical application of MBT.

Slide Set (pdf)

Improved Testing of Multithreaded Programs with Dynamic Symbolic Execution

Keijo Heljanko, Aalto University

Testing of multithreaded programs using dynamic symbolic execution is a technique that automatically tests the source code of a multithreaded program with the help of symbolic execution employing SMT solvers. This tutorial focuses on how the path explosion problem that is due to the high number of interleavings can be alleviated using both traditional partial order reduction techniques, as well as by the novel combination of testing with the unfolding technique.

Slide Set 1 (pdf)

Slide Set 2 (pptx)

Slide Set 3 (pdf)

Recorded Video Part I

Recorded Video Part II

Property-based testing with QuickCheck

John Hughes, Quvic and Chalmers

QuickCheck is a random testing tool that uses properties as test oracles, and generates minimized counterexamples to make debugging failures as easy as possible. QuickCheck is embedded in a functional language, which is used to build specification frameworks for particular kinds of problems on top of the underlying property-based tests. I’ll present the basic techniques and extensions for testing state machines, separate components, and race conditions, and I’ll describe our experiences in applying these techniques to hard industrial testing problems for Ericsson, Volvo Cars, and other Quviq customers.

Slide Set (pdf)

Testing and Verifying Software Properties with ACL2 and ProofPad

Rex Page, The University of Oklahoma

Designing tests for software requires developers to think carefully about what they expect their software to do and to state those expectations in detail. This by itself helps connect specifications with implementations, especially when the tests are expressed as Boolean properties. Automated testing of expected properties against random data has proven to be an effective method for rooting out subtle bugs. When applications justify investing the additional effort required for verification by mathematical proof, mechanized tools are required to avoid mistakes in the details of complex logic. ACL2 provides the required, mechanized support and has been used productively in VLSI design and in software development for safety-critical and security-critical applications. This presentation employs the ProofPad interactive development environment to illustrate property-based testing and verification of ACL2 software.

Handouts Set 1

Handouts Set 2

Lisp Exercises

Solutions and Demos

Practical Model-Based Testing With Papyrus and RT-Tester

Jan Peleska, Verified International GMBH and Bremen University

In Model-Based Testing (MBT), test models specify the expected behaviour of the system under test (SUT), so that relevant test cases, concrete test data and expected results can be automatically derived from the model, and transformed into executable test procedures. The objective of this tutorial is to get a "hands-on" experience of the MBT work flow, as it is performed today in leading-edge industrial test campaigns. The application domain is embedded concurrent real-time systems.

In the first part of this session, the practical development of test models in the widely used SysML formalism is illustrated, using the Papyrus tool which is freely available for academic use. In the second part, the MBT tool RT-Tester is used to derive test cases, test data and test oracles from the test models written with Papyrus and exercise automatically generated test procedures on an SUT. RT-Tester is also made available free of charge for academic applications (also after the summer school for students interested in working with this tool in the context of their bachelor, master or doctoral theses).

Slides (pdf)

Model-Based Testing - There is Nothing More Practical than a Good Theory

Jan Tretmans, Radboud University Nijmegen and TNO - ESI

Systematic testing of software plays an important role in the quest for improved software quality. Model-based testing is one of the promising technologies to meet the challenges imposed on software testing. In model-based testing a system under test (SUT) is tested for compliance with a formal description, or model, of the SUT's required behaviour. Such a model serves as a precise and complete specification of what the SUT shall do, and, consequently, is a good basis for the automatic and reproducible generation of large volumes of high-quality test cases. This enables effective test automation beyond the mere automatic execution of manually crafted test scripts, which is the current state of practice. And if the model is valid, i.e., expresses precisely what the system shall do, then all these tests are provably valid, too.

The lecture will discuss the model-based testing theory for non-deterministic state-based systems, where models are expressed as labelled transition systems, and compliance between the SUT and the model is defined with the `ioco' implementation relation. The ioco-testing theory, on the one hand, provides a sound and well-defined foundation for labelled transition system testing, having its roots in the theoretical area of testing equivalences and refusal testing. On the other hand, it has proved to be a practical basis for several model based test generation tools and applications. Definitions, underlying assumptions, properties, and several examples of the ioco-testing theory will be presented, involving specifications, implementations, test cases, the ioco-implementation relation and some of its variants, a test generation algorithm, and the soundness and exhaustiveness of this algorithm. A tool, a discussion of industrial applicability, a demo, and a practical exercise with a downloadable ioco-test generation tool will conclude the lecture.

Slide Set 1 (pdf)

Slide Set 2 (pdf)

Speakers

Thomas Ball

Biography Thomas Ball (Tom) is a Principal Researcher and Research Manager at Microsoft Research. From 1993-1999, he was at Bell Laboratories, where he made contributions in program visualization and profiling. His 1997 PLDI paper on path profiling with colleagues Ammons and Larus received the PLDI 2007 Most Influential Paper Award. In 1999, Tom moved to Microsoft Research, where he started the SLAM software model checking project with Sriram Rajamani, leading to the Static Driver Verifier (SDV) tool for finding defects in device driver code. A 2001 PLDI paper on SLAM’s predicate abstraction procedure for C programs received the PLDI 2011 Most Influential Paper Award. Tom and Sriram received the 2011 CAV Award for SLAM/SDV. Tom is a 2011 ACM Fellow for "contributions to software analysis and defect detection". At Microsoft, he has nurtured research areas such as automated theorem proving, program testing and verification, and empirical software engineering.

Machiel van der Bijl

Biography Machiel van der Bijl is co-founder of Axini BV, The Netherlands, a company specializing in modeling and model-based testing. Machiel has a broad experience in both theoretical and practical computer science. He has worked for several companies in the financial and embedded/high tech sector. Machiel has a Master of Science and a PhD degree in computer science from the University of Twente. The last six years he has been working with his colleagues at Axini on applying model-based testing to hardware/software systems in the industry. Axini is the maker of Axini TestManager, a modelling environment to model and test industry grade hardware/software systems. It is used in the financial and embedded/high tech sector.

Keijo Heljanko

Biography Keijo Heljanko is an Associate Professor at Department of Computer Science and Engineering, Aalto University, Finland. He obtained his doctoral degree in 2002 from Helsinki University of Technology, spent a year as a postdoc at University of Stuttgart, and has since worked in various research positions at Aalto University, with the latest Associate Professor appointment in Aug 2013. His research interests include distributed systems, distributed computing, formal methods, model checking, and automated testing.

John Hughes

Biography John Hughes has been a functional programming enthusiast for more than thirty years, at the Universities of Oxford, Glasgow, and since 1992 Chalmers University in Gothenburg, Sweden. He served on the Haskell design committee, co-chairing the committee for Haskell 98, and is the author of more than 75 papers, including "Why Functional Programming Matters", one of the classics of the area. With Koen Claessen, he created QuickCheck, the most popular testing tool among Haskell programmers, and in 2006 he founded Quviq to commercialise the technology using Erlang.

Rex Page

Biography Rex Page has maintained an active interest in equation-based programming for over four decades, starting with applications in massively parallel computation and progressing to high-assurance software. He has moved between academic and industrial positions, both large companies and start-ups, on a regular basis. His longest gig is his current position as Professor of Computer Science at The University of Oklahoma, which he has held since 1994.

Jan Peleska

Biography Since 1995, Dr. Peleska is professor for computer science (operating systems and distributed systems) at Bremen University in Germany. At the University of Hamburg, he studied mathematics and wrote his doctoral thesis on a topic in the field of differential geometry. From 1984 to 1990 he worked with Philips as Senior Software Designer and later on as department manager in the field of fault-tolerant systems, distributed systems and database systems. From 1990 to 1994 he was manager of a department at Deutsche System-Technik responsible for the development of safety-critical embedded systems. Since 1994 he has worked as a consultant, specialising on development methods, verification, validation and test of safety-critical systems. His habilitation thesis focusing on Formal Methods for the development of dependable systems was finished in 1995. Together with his wife Cornelia Zahlten, he has founded the company Verified Systems International GmbH in 1998, providing tools and services in the field of safety-critical system development, verification, validation and test. His research interests include formal methods for the development of dependable systems, test automation based on formal methods with applications to embedded real-time systems, verification, and formal methods in combination with CASE methods. Current industrial applications of his research work focus on the development and verification of avionic software, space mission systems and railway and automotive control systems. Together with his colleague Rolf Drechsler he manages the Post Graduate Programme Embedded Systems GESy which has been founded in 2006.

Jan Tretmans

Biography Jan Tretmans is associate professor in the Model-Based System Development group, Radboud University, Nijmegen, and Research Fellow at TNO - Embedded Systems Innovation, Eindhoven. He is working in the areas of software testing, and the use of formal methods, models, and verification techniques in software engineering. In particular, he likes to combine these two topics: testing using formal methods, also referred to as model-based testing. In these fields he has several publications, such as the ioco-theory for model-based testing of non-deterministic state-based systems, and he has given numerous presentations at scientific conferences as well as for industrial audiences. Among others, Jan applied formal modelling to the software control system of the Maeslant Kering, a safety-critical storm surge barrier near Rotterdam, and he performed model-based testing of the European electronic biometric passport. Currently, Jan Tretmans is involved in the joint TNO-ESI project THEMIS with the company ASML on improving testing processes with model-based testing, and in the Dutch Technical Research Organisation STW project ITALIA on combing model-based testing and automata learning.

Registration

The registration deadline is April 15, 2014.

To apply to the summer school, please send an email to Veronica.Gaspes@hh.se with "Halmstad Summer School on Testing" in the title. If you have any dietary requirements, or would like to attend only certain days of the summer school, please specify in your email text.

The registration fee is 2000 SEK (approx. 225 EUR, ) and covers lunches, coffee breaks, the social event, and the study material but does not include the social dinner. The ticket to the social dinner costs 500 SEK and can be requested upon registration (please indicate in your email). The deadline for registration is April 15, 2014. After sending the registration email, you will receive a confirmation. Please proceed to payment after you receive the confirmation email.

On-site or late registration is possible but will cost 2500 SEK (excluding the social dinner).

If your registration is confirmed, please use the following web page to pay the registration fee: PayPal Payment Page.

Program

June 9 (9:00-17:00)

09:00-09:15 Arrival and Registration

09:15-09:30 Welcome, opening remarks (Mohammad Mousavi, Halmstad)

09:30-10:30 Automated Test Generation via Satisfiability Modulo Theory Solvers, Part I (Thomas Ball, Microsoft)

10:30-11:00 Coffee Break

11:00-12:30 Automated Test Generation via Satisfiability Modulo Theory Solvers, Part II (Thomas Ball, Microsoft)

12:30-14:00 Lunch Break

14:00-15:30 Improved Testing of Multithreaded Programs with Dynamic Symbolic Execution, Part I (Keijo Heljanko, Aalto)

15:30-16:00 Coffee Break

16:00-17:00 Improved Testing of Multithreaded Programs with Dynamic Symbolic Execution, Part II (Keijo Heljanko, Aalto)

June 10 (9:30-17:00)

09:30-10:30 Model-Based Testing - There is Nothing More Practical than a Good Theory, Part I (Jan Tretmans, TNO-ESI and Nijmegen)

10:30-11:00 Coffee Break

11:00-12:30 Model-Based Testing - There is Nothing More Practical than a Good Theory, Part II (Jan Tretmans, TNO-ESI and Nijmegen)

12:30-14:00 Lunch Break

14:00-15:30 Model-Based Testing, the Difference between Theory and Practice, Part I (Machiel van der Bijl, Axini)

15:30-16:00 Coffee Break

16:00-17:00 Model-Based Testing, the Difference between Theory and Practice, Part II (Machiel van der Bijl, Axini)

June 11 (9:30-12:30)

09:30-10:30 Practical Model-Based Testing With Papyrus and RT-Tester, Part I (Jan Peleska, Verified and Bremen)

10:30-11:00 Coffee Break

11:00-12:30 Practical Model-Based Testing With Papyrus and RT-Tester, Part II (Jan Peleska, Verified and Bremen)

12:30-14:00 Lunch Break

14:00-17:00 Social Event

18:30-22:00 Social Dinner

June 12 (9:30-17:00)

09:30-10:30 Testing and Verifying Software Properties with ACL2 and ProofPad, Part I (Rex Page, Oklahoma)

10:30-11:00 Coffee Break

11:00-12:30 Testing and Verifying Software Properties with ACL2 and ProofPad, Part II (Rex Page, Oklahoma)

12:30-14:00 Lunch Break

14:00-15:30 Property-Based Testing with QuickCheck, Part I (John Hughes, Quviq and Chalmers)

15:30-16:00 Coffee Break

16:00-17:00 Property-Based Testing with QuickCheck, Part II (John Hughes, Quviq and Chalmers)

Venue

The workshop will be held on the campus of Halmstad University in Halmstad, Sweden. Halmstad is a popular holiday destination located on the Swedish west coast. Just a few minutes by bicycle or bus takes you from campus to city centre, sandy beaches or forested Galgberget Hill.

Directions to/in Campus

Directions for getting to campus can be found at http://www.hh.se/english/abouttheuniversity/visitus.307_en.html

The campus map can be found here: http://www.hh.se/download/18.4cc60a491424e61ad931b4d/1385107637179/Campuskarta+A5+ENG-20+NOV+2013.pdf. The workshop will be located at the Baertling lecture hall, which is located at the ground floor (1st floor in Swedish terms!) of the J building (house Visionen). Coffee breaks will be held at the ground floor of the same building.

Directions to Halmstad

Trains take you directly to Göteborg in 75 minutes, to the Malmö-Copenhagen area in about 2 hours and to Stockholm in 4.5 hours. There are also daily flights from Halmstad Airport to Stockholm.

If you are flying internationally it is generally easiest to fly into Copenhagen (CPH) airport (also known as Kastrup). The best thing about flying into CPH is that you just buy a train ticket when you arrive at the airport and simply take a train from the airport directly to Halmstad. The train leaves from the airport itself approximately once an hour on weekdays. We recommend that you check the time-table at the Swedish Railways site and allow one hour from touchdown to getting to the train station (just outside customs). (It seems that you can take an earlier or a later train on the same day regardless of the exact train you booked, but obviously you will lose your seat reservation if you have made one.) To get to your hotel, you can combine a taxi booking with your train ticket at the Swedish Railways site and a driver will wait for you with your name mentioned on a board once you arrive in Halmstad.

In Halmstad, everything is either in walking distance or a short taxi ride away. Usually there are taxis at the station. If there are none there is a phone that connects directly to the local taxi company. For the eventuality that the phone is not working, it is good to have a cell phone handy. The number for the taxi company is written on the phone.

Note that CPH is in Denmark (and not in Sweden). So, if you need visas for European countries, make sure you get one that works for both.

If for some reason you cannot or do not want to use CPH, the next best international airport is in Gothenburg (GOT), locally known as Landvetter. The tricky thing about using that airport is that you would first have to take a 45 minute shuttle from the airport to the Gothenburg train station, and then take the train to Halmstad. That is one transfer and one wait. You can buy a combined shuttle and train ticket from the the Swedish Railways site.

Accommodation

We have made a pre-booking for a group of rooms at Hotel Continental. The negotiated rate is 752 SEK per night (including breakfast) for a single room. If you would like to use this offer, please send an email to the hotel reservation and mention the booking code "HSST2014".

Here are some other suggestions for the accommodation, with an indication of their price range, (obtained from booking.com) and their distance to the summer school venue:

• Scandic Hallandia (~160-200 EUR / night, 2km)
• Hotel Amadeus (~100-120 EUR / night, 2.5km)
• First Hotel Martenson (~130-150 EUR / night, 2km)
• Quality Hotel Halmstad (~80-100 EUR / night, 3 km)
• STF Halmstads Hostel Kaptenshamn (~80-100 EUR / night, 2km)

An annotated Google Map with suggestion for restaurants can be found here.

History

This is the fourth edition of the summer school. Information about the previous editions is provided below.

• HSST 2013 (June 3- June 5, 2013),
• Second Summer School on Accurate Programming (May 30 - June 1, 2012)

Organizers

Please do not hesitate to contact us if you have any questions or enquiries:

• Veronica Gaspes (Organization Chair, veronica.gaspes@hh.se)
• Mohammad Mousavi (Program Co-Chair, m.r.mousavi@hh.se)
• Eva Nestius (Local Organization)
• Walid Taha (Program Co-Chair, walid.taha@hh.se)

HSST 2014 Second Group Photo.