HSST 2017
7th Halmstad Summer School on Testing, HSST 2017
Organized in cooperation with TOCSYC Network
June 12-15, 2017 - Halmstad University, Sweden
Contents
- 1 Introduction
- 2 Tutorials
- 2.1 Specification guided testing and verification for Cyber-Physical Systems, Georgios Fainekos, Arizona State University, USA
- 2.2 Testing from Formal Specifications: A Unifying Framework, Marie-Claude Gaudel, Université de Paris-Sud, France
- 2.3 TSTL: a Little (Integrated) Language for Testing, Alex Groce, Northern Arizona University, USA
- 2.4 Combinatorial Interaction Testing, Justyna Petke, University College London, UK
- 2.5 Automated debugging – the past, the now, and the future, Franz Wotawa, Graz University of Technology, Austria
- 2.6 Fuzzing with Inferred Grammars, Andreas Zeller, Saarland University, Germany
- 3 Program
- 4 Registration
- 5 Ph.D. Student Presentations
- 6 Venue
- 7 History
- 8 Organizers
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 7th 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.
Tutorials
Specification guided testing and verification for Cyber-Physical Systems, Georgios Fainekos, Arizona State University, USA
Every year the software which controls Cyber-Physical Systems (CPS) increases in complexity. Due to the increased complexity, numerous design and implementation errors are discovered while CPS are operational in the field. Such errors can have catastrophic effects to human life and to the economy. In this talk, we present how the error detection process in CPS can be accelerated using Model-Based Development (MBD) and formal specifications. Temporal logic is a formal specification language that can capture both state-space and real-time system requirements. For example, temporal logics can mathematically state requirements like "whenever the system switches to first gear, then it should not switch back to second gear within 2.5sec". Our approach in tackling this challenging problem is to convert the verification problem into an optimization problem through a notion of robustness for temporal logics. Through this transformation, any stochastic optimization algorithm can be used for automatic test case generation for CPS. In this tutorial, we will explain how to write formal requirements and how to setup a falsification problem for CPS models. In addition, we will show how the basic underlying theory can be extended to provide a solution to the conformance problem and to the on-line monitoring problem. The presentation will be accompanied by demonstrations using our testing and verification Matlab(TM) toolbox called S-TaLiRo (System's TemporAl LogIc Robustness). In particular, we will demonstrate the use of S-TaLiRo on challenge problems from the automotive and medical device industries.
Testing from Formal Specifications: A Unifying Framework, Marie-Claude Gaudel, Université de Paris-Sud, France
The links between testing and formal methods have been studied for quite a while: some pioneering papers come back to the seventies. Sound and effective testing methods have been established based on various types of formal specifications, leading to tools for supporting the testing process. This tutorial presents a framework for developing such testing methods. It has been instantiated for several formal approaches, such as FSM, ADT, VDM, IOTS, process algebras (LOTOS and CSP), and more recently Circus. Given a specification and a system under test (SUT), any testing activity relies, explicitly or not, on a satisfaction relation (often called conformance): does the SUT satisfy the specification? Tests, and test drivers can be derived from the specification on the bases of the satisfaction relation and some assumptions on the SUT and its operational environment (often called testability hypotheses). Verdicts of test executions are also based on the satisfaction relation, but, moreover, they depend on the observations that can be made on the SUT. After presentation and formalisation of these generic concepts, their specialisations for some of the formal approaches mentioned above will be introduced.
TSTL: a Little (Integrated) Language for Testing, Alex Groce, Northern Arizona University, USA
TSTL (the Template Scripting Testing Language) is a "little language" (domain-specific language) for describing valid tests and correctness properties for Python programs. While TSTL can be used like other testing tools, both academic and industrial, as an off-the-shelf test generator, the core idea of TSTL is to offer, in place of a monolithic tool, an interface to testing as a language extension. This approach makes testing not a separate activity to be performed using a tool, but as natural to users of the language of the system under test as is the use of domain-specific libraries such as ArcPy, NLTK, or QIIME, in their domains (GIS, natural language processing, bioinformatics). TSTL is a language and tool infrastructure, but is also a way to bring testing activities under the control of an existing programming language in a simple, natural way. In this talk, I will present the basic ideas of TSTL as well as a tutorial on using TSTL for rapid prototyping of new automated testing and debugging techniques.
Combinatorial Interaction Testing, Justyna Petke, University College London, UK
The tutorial's focus will be Combinatorial Interaction Testing (CIT), a relatively mature area of software testing that benefited from search-based software engineering techniques (SBSE). CIT is a black-box testing method that has been extensively used in testing highly configurable software. In practice it's usually infeasible to test all possible parameter combinations of such systems. Empirical studies have shown that CIT provides a way of reducing the test suite size whilst still maintaining high fault detection rates. SBSE techniques have been successfully applied to the CIT test suite generation problem which will be presented in detail during the tutorial.
Automated debugging – the past, the now, and the future, Franz Wotawa, Graz University of Technology, Austria
What happens after testing when the implementation passes some tests but fails on others? Someone has to fix the detected misbehavior, which is considered a laborious task. In order to support debugging activities researchers have provided ideas and methods since the eighties of the last century. In this tutorial we will have a look at past and recent methods supporting debugging and also automating debugging to a certain extent. In addition, we will discuss some reasons behind the lack of such methods in today’s integrated development environment and give an outlook on new ideas and challenges of automated debugging research and practice.
Fuzzing with Inferred Grammars, Andreas Zeller, Saarland University, Germany
Large-scale random testing, also known as “Fuzzing”, is a cheap and fully automated technique to check programs for robustness. Effective fuzzing, however, requires the ability to create mostly valid inputs, because syntactically invalid inputs would be rejected by the program, never reaching the features one would like to test. In our previous LANGFUZZ work, we have shown how a given grammar greatly improves fuzzing effectiveness; LANGFUZZ is now the standard testing tool for Mozilla Firefox and hans found more than 4,000 bugs. Recent advances in grammar inference allow these techniques to be automatically deployed for arbitrary programs. In this tutorial, I will give a hands-on tutorial on how to fuzz, how to fuzz with grammars, and teach how to infer grammars automatically.
Program
June 12 (9:00-17:00)
09:00-09:15 Arrival and Registration
09:15-09:30 Welcome, opening remarks (Mohammad Mousavi) Slides
09:30-10:30 Specification guided testing and verification for Cyber-Physical Systems, Part I (Georgios Fainekos) Slides
10:30-11:00 Coffee Break
11:00-12:30 Specification guided testing and verification for Cyber-Physical Systems, Part II (Georgios Fainekos) Slides
12:30-14:00 Lunch Break
14:00-15:30 TSTL: a Little (Integrated) Language for Testing, Part I (Alex Groce)
15:30-16:00 Coffee Break
16:00-17:00 TSTL: a Little (Integrated) Language for Testing, Part II (Alex Groce)
June 13 (9:30-18:00)
09:30-10:30 Combinatorial Interaction Testing, Part I (Justyna Petke) Slides
10:30-11:00 Coffee Break
11:00-12:30 Combinatorial Interaction Testing, Part II (Justyna Petke) Slides
12:30-14:00 Lunch Break
14:00-15:30 Ph.D Symposium, Session I
- Lars Luthmann, Modeling and Testing Product Lines with Unbounded Parametric Real-Time Constraints
- Johan Eddeland, TESTRON: Model-Based Testing of Mechatronic Systems
15:30-16:00 Coffee Break
16:00-18:00 Ph.D. Presentations, Session II
- Jesús Morán, Automatic Functional Testing of MapReduce Applications
- Asma Berriri, Testing and verification for Software Defined Networks
- Sebastian Kunze, Testing Software Product Lines Using Differential Symbolic Execution
June 14 (9:30-12:30)
09:30-10:30 Testing from Formal Specifications: A Unifying Framework, Part I (Marie-Claude Gaudel) Slides - Part I
10:30-11:00 Coffee Break
11:00-12:30 Testing from Formal Specifications: A Unifying Framework, Part II (Marie-Claude Gaudel) Slides - Part II
12:30-14:00 Lunch Break
14:00-17:00 Social Event
18:30-22:00 Social Dinner
June 15 (9:30-17:00)
09:30-10:30 Automated debugging – the past, the now, and the future, Part I (Franz Wotawa) Slides - Part I
10:30-11:00 Coffee Break
11:00-12:30 Automated debugging – the past, the now, and the future, Part II (Franz Wotawa) Slides - Part II
12:30-14:00 Lunch Break
14:00-15:30 Fuzzing with Inferred Grammars, Part I (Andreas Zeller) Slides Examples
15:30-16:00 Coffee Break
16:00-17:00 Fuzzing with Inferred Grammars, Part II (Andreas Zeller) Slides Examples
Registration
The registration deadline is ' April 15 May 1, 2017. (Extended)
Please register using this link and also pay your registration using the PayPal button provided in the same page.
If you have any dietary requirements, or would like to attend only certain days, please indicate it in the registration form.
After submitting the registration form, please use the PayPal page for payment.
Upon concluding the payment process, you will receive a confirmation.
The registration fee is 3100 SEK (approx. 325 EUR, ) and covers lunches, coffee breaks, and the study material but does not include the social event and dinner. The ticket to the social event and dinner (excl. drinks) costs 550 SEK and can be included upon registration. The registration fees include Value Added Tax and is hence, VAT deductible for governmental organizations.
Ph.D. Student Presentations
We have 8 time slots for Ph.D. presentations, where each student has 10 minutes to present her/his research project (and possibly results) and receive feedback from our experts. We solicit abstracts of 2 pages in the EasyChair Style in order to make a selection. The abstract should be solely authored by the Ph.D. student, but reviewed and approved by her/his supervisors. The abstracts can be submitted using our EasyChair web page.
The submission system is open now. The deadline for submissions is May 15, 2017.
Venue
The summer school 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. The summer school will be located at the Baertling lecture hall, which is located at the ground floor of the J building (Visionen). Coffee breaks will be held at the same building. Lunches will be served in the ground floor of the Spiro restaurant in the G building.
Directions to Halmstad
Trains take you directly to Göteborg in about 1 hour, 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 price is 850 SEK for a single room, 1050 SEK for a double room and 620 SEK for a shared double room. All prices include breakfast.
If you would like to use this offer, please send an email to the hotel reservation and mention the booking code "Summer School 2017".
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 seventh edition of the summer school. Information about the previous editions is provided below.
- HSST 2018
- HSST 2016 (June 13- June 16, 2015),
- HSST 2015 (June 8- June 11, 2015),
- HSST 2014 (June 9- June 12, 2014),
- 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:
- Stella Erlandsson (Local Organization, stella.erlandsson@hh.se)
- Veronica Gaspes (Organization Chair, veronica.gaspes@hh.se)
- Mohammad Mousavi (Program Co-Chair, m.r.mousavi@hh.se)
- Richard Torkar (Program Co-Chair, richard.torkar@cse.gu.se)