Tuesday, June 11, 2013

ScalaCheck Book

The ScalaCheck Book that was mentioned during the summer school has now been pre-leased by  Artima!

Friday, May 31, 2013

Instructions for the Third Summer School on Testing


Arrival and Directions:



  • The school will be held in the lecture room D 215 (D building, first floor, which is considered 2nd floor in Swedish!, room 15); you can find a campus map at:  http://www.hh.se/download/18.149d6d3d13e19db3d27af9/1366793973580/map-HH_2013.pdf .
  • Lunchs will be served at the Spiro kantine located at the ground floor of the G building; please join the crowd when moving to the lunch, as there are no separate tickets available.  
  • Please note that June 6 (the day after the summer school) is a national holiday in Sweden and the university as well as many shops in the town are closed.


Software and Tools:

  • For the first day you will need the client for the RT-Tester tool. It will be provided on memory sticks during the lecture.
  • For the second day, you need to install the following pieces of software: 
  • For the third day you will need the following pieces of software:

Monday, April 8, 2013

The Third Halmstad Summer School on Testing

The Third Halmstad Summer School on Testing

Halmstad University, June 3 - June 5, 2013



Software testing accounts 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 rigor and structure into this field, resulting in several industrial-strength processes, techniques and tools for different levels of testing. The 3rd 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 


  • Test-Driven Software Development in Java Including Concurrency (Robert "Corky" Cartwright, Rice)
  • Industrial-Strength Model-Based Testing and its Methodology with RT-Tester and its Methodology (Wen-Ling Huang and Jan Peleska, Verified Systems and University of Bremen)
  • Property-based testing with QuickCheck (John Hughes, QuviQ and Chalmers)
  • Closing the V - by going from V to DEL (Tony Larsson, Halmstad)
  • Testing and Verifying Software Properties with ACL2 and ProofPad, and Dracula (Rex Page, Oklahoma) 
  • Introduction to Model-Based Testing (Mohammad Mousavi, Halmstad) 
  • Hands on ScalaCheck (Rickard Nilsson, Lund)
  • Accurate Programming Using ScalaCheck (Walid Taha, Halmstad).




Program




June 3  (9:00-17:00)



09:00-09:15 Arrival and Registration


09:15-09:30 Welcome, opening remarks (Walid Taha, Halmstad)


09:30-10:30  Introduction to Model-Based Testing  (Mohammad Mousavi, Halmstad)


10:30-11:00 Coffee Break


11:00-12:30 Industrial-Strength Model-Based Testing with RT-Tester and its Methodology, Part I  (Jan Peleska, Verified and University of Bremen)


12:30-14:00 Lunch Break


14:00-15:30 Industrial-Strength Model-Based Testing with RT-Tester and its Methodology, Part II (Wen-Ling Huang, University of Bremen)


15:30-16:00 Coffee Break



16:00-17:00 Closing the V - by going from V to DEL (Tony Larsson, Halmstad)





June 4 (9:00-17:30)




09:00-10:30 Testing Concurrent Java Programs, Part I (Corky Cartwright, Rice)


10:30-11:00 Coffee Break


11:00-12:30 Testing Concurrent Java Programs, Part II (Corky Cartwright, Rice)


12:30-14:00 Lunch Break


14:00-15:30 Testing and Verifying Software Properties with ACL2 and ProofPad, Part I (Rex Page, Oklahoma)


15:30-16:00 Coffee Break


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


June 5 (9:00-17:30)


09:00-10:30 Accurate Programming Using ScalaCheck (Walid Taha, Halmstad)

10:30-11:00 Coffee Break

11:00-12:30 Hands-on ScalaCheck (Rickard Nilsson, Lund)

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:30 Property-based testing with QuickCheck, Part II  
(John Hughes, QuviQ and Chalmers)





Registration




The registration deadline is  May 1, 2013.


The registration fee is 1000 SEK (approx. 120 EUR) and covers lunches and coffee breaks.


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 your registration is confirmed, please use the following form to pay the registration fee:

Registration fee HSST2013




Venue


The summer school will be held on the campus of Halmstad University  in Halmstad, Sweden.  Halmstad is a popular summer 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.  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.



Directions for getting to campus can be found here:




The campus map, with a link to a printable pdf version can be found here:




If you are flying in 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 here:




and allow one hour from touchdown to getting to the train station (just outside customs).  
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.


Accommodation



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




Organizers



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)


Abstracts


Test-Driven Software Development in Java Including Concurrency (Robert “Corky” Cartwright, Rice)


In my experience, test-driven development--where unit tests are written in the process of designing and coding an application--is an extremely effective approach to developing single-threaded applications in high-level object-oriented languages like Java.  In contrast, testing concurrent applications is much more difficult; there are many traps--including deep design flaws in the mainstream testing frameworks like JUnit and TestNG--that can ensnare developers who apply test-driven development to the task of writing concurrent applications. In this tutorial, I will briefly review test-driven development for simple single-threaded applications, observe how it breaks down when it is naively applied to concurrent applications, and show how it can be salvaged with appropriate care in writing test code.  In the process, I will present ConcJUnit, a unit testing framework compatible with JUnit developed by my student, Dr. Mathias Ricken, that addresses flaws in the design of JUnit.



Industrial-Strength Model-Based Testing and its Methodology (Jan Peleska and Wen-ling Huang, Bremen)



In this tutorial fundamental concepts and latest advancements in testing are discussed.
The focus lies on model-based testing of (potentially safety-critical) distributed
embedded systems. We discuss the fundamental questions


  - Have we tested enough ?
  - Has our test suite sufficient strength ?
  - How can we automate test generation, execution and evaluation ?


from both practical and theoretical angles and provide tool demonstrations
illustrating the present state-of-the-art.


The session is divided into 2 lectures.


Lecture 1 focuses on modelling, automated  generation of test cases, test data and procedures, and on automated requirements tracing.
It is demonstrated that model-based testing is sufficiently mature to be applied in practice, because existing tool can handle test models of considerable complexity, support work flows complying to the usual process models, and produce artefacts conforming to the requirements of today's standards. This lecture is targeted at practitioners from industry and at researchers interested in comparing their own research in the field to what is currently feasible in practice.


Lecture 2 focuses on theoretical foundations. It is demonstrated how various test strategies are justified through their capability to produce exhaustive tests, that is, tests proving some conformance relation between specification model and implementation. We consider "best practice" strategies like equivalence class partition testing and boundary value testing, as well as novel strategies suitable for testing large distributed systems.


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.

Talk title: Closing the V - by going from V to DEL (Tony Larsson, Halmstad)



Tracing back to the cause a failure found in field operation and then correcting it is very very costly. Many have realized that one therefore needs to find more faults already in early phases, especially when working with complex distributed systems. Several techniques have been suggested but few seems to significantly reduce the number of faults discovered in later phases such as during system integration or acceptance test. A method seems to be needed for early testing of distributed systems that if possible also helps to give a structure to the overall testing process from specification to certified product.


Introduction to Model-Based Testing (Mohammad Mousavi, Halmstad)



Computer systems are tested too late, too little and in an ad-hoc manner. Model-Based Testing (MBT) offers a structured and mechanized solution to testing by using behavioral models to automatically generate and execute effective test-suites. In this tutorial, we present the theoretical background for MBT and introduce some of the existing tools for different flavors of MBT.


Hands on ScalaCheck (Rickard Nilsson, Lund)



ScalaCheck does not only port the functionality of QuickCheck to Scala, it also ports a set of functional concepts and ways of thinking. When delving deeper into ScalaCheck, defining custom data generators and complex properties, it can be worthwhile to have a bit of an understanding for ScalaCheck’s implementation and a host of practical examples to go along.


Testing and Verifying Software Properties with ACL2 and ProofPad (Rex Page, Oklahoma)



Designing properties for software testing requires developers to think carefully about what they expect their software to do and to express those expectations in detail. This by itself helps connect specifications with implementations, and running tests against those properties using 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 must be used to avoid mistakes in the details of complex logic. ACL2 provides this kind of support in industrial applications, especially in VLSI design and safety-critical and security-critical software. The ProofPad IDE adds property-based testing to ACL2’s capabilities.



Accurate Programming Using ScalaCheck (Walid Taha, Halmstad)



Accurate programming is a practical approach to producing high quality programs. It combines ideas from test-automation, test-driven development, agile programming, and other state of the art software development methods. In addition to building on approaches that have proven effective in practice, it emphasizes concepts that help programmers sharpen their understanding of both the problems they are solving and the solutions they come up with. This is achieved by encouraging programmers to think about programs in terms of properties.



Speakers



Robert “Corky” Cartwright (Rice)


Robert “Corky” Cartwright is Professor of Computer Science at Rice University. He earned a bachelor’s degree magna cum laude in Applied Mathematics from Harvard College in 1971 and a doctoral degree in Computer Science from Stanford University in 1977 under the supervision of David Luckham and John McCarthy. After serving as an Assistant Professor at Cornell University from 1976 to 1980, he joined the faculty of Rice University, where he helped found the Computer Science Department in 1984. He has been a tenured member of the Rice faculty since 1981.    For the past 40 years, Professor Cartwright has conducted fundamental research on the theory, design, and implementation of programming languages.
His early work focused on formalizing functional programs as definitions extending a first order theory of the program data, enabling proofs of correctness by simple structural induction. This line of research culminated in the construction a comprehensive framework (with M. Felleisen and P.L. Curien) for formalizing the semantics of arbitrary deterministic interactive computations. He suggested enriching type systems beyond the limits that can be enforced by a compiler and dubbed the resulting type systems “soft type systems”. More recently, Professor Cartwright’s research has focused on improving the languages and tools used in mainstream software engineering, notably Java. Together with Guy Steele, he designed an extension of Java called NextGen that supports first-class generics (classes and methods parameterized by type) while retaining compatibility with the Java Virtual Machine. He is currently collaborating with Walid Taha on developing better linguistic frameworks built on top of the Java Virtual Machine for specifying and simulating cyber-physical systems such as robots.
  Professor Cartwright has a passionate interest in improving introductory computer science curricula. To support the object-oriented programming curriculum at Rice, he supervised the development of an open-source pedagogic programming environment called DrJava which has been adopted by many other colleges and universities.
  Throughout his career, Professor Cartwright has been active in professional service including serving on the editorial boards; serving as general chair, program chair, or program committee member for major research conferences; serving on the ACM Turing Award Committee; and serving as a member of the Board of Directors of the Computing Research Association.  In 1998, he was elected as a Fellow of the ACM.


Wen-ling Huang (Bremen)


Dr. Wen-ling Huang is professor for mathematics, with a research focus on differential geometry and applications in physics. In cooperation with Jan Peleska, she applies mathematical theories for the purpose of model-based testing and the formal justification of test strategies. In this field, she investigates strategies for testing systems with large data types, hybrid systems and large concurrent systems, in particular, Systems of Systems.
John Hughes (Quvic and Chalmers)


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.



Tony Larsson (Halmstad)


Tony Larsson is professor of embedded systems at Halmstad University. After a Master in Mechanical Engineering 1974 from University of Linköping, Sweden, he worked for more than 28 years in different positions and at different parts of Ericsson AB with dependable network distributed real-time embedded systems; both with hardware and software. During this period he was appointed technical expert in system design methods and also received his PhD in Computer Science at Linköping University, Sweden 1989. After a short period working for the defense material administration in Sweden on system architecture for the network based defense he in 2003 became Professor of Embedded Systems at Halmstad University. His current interests are focused around software solutions supporting real-time network enabled cooperative embedded systems and especially for intelligent transport, vehicle and mobile sensor network applications relying on different forms of wireless communication.



Mohammad Mousavi (Halmstad)


Mohammad Mousavi is a professor of Computer Systems Engineering at Halmstad University (HH) in Sweden and specializes in model-based testing and verification. He received his Ph.D. in Computer Science in 2005 from from Eindhoven University of Technology (TU/e), under the supervision of Jan Friso Groote (TU/e) and Gordon Plotkin (Edinburgh). Since then, he has been assistant professor at the Department of Electrical Engineering at TU/e, postdoctoral researcher at Reykjavik University, Iceland, assistant and associate professor at the Department of Computer Science at TU/e. He is the co-author of 70 chapters and scientific papers in refereed books, journals and conference proceedings. He has been the guest editor of special issues for Science of Computer Programming (Elsevier) and Innovations in Systems and Software Engineering (Springer).




Rickard Nilsson (Lund)


Rickard Nilsson is a software developer and systems administrator working at Lunarc, a center for scientific and technical computing at Lund University. Rickard is a fan of functional programming, and likes to bring ideas of declarative specifications and accuracy into the messy world of server configuration management and network deployments. He ported Haskell QuickCheck to Scala in 2007, and has since then been part of the Scala community, maintaining and developing the ScalaCheck project.



Rex Page (Oklahoma)


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 (Bremen)


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.




Walid Taha (Halmstad)


Walid Taha is a Professor of Computer Science at Halmstad University. He is interested in the design, semantics, and implementation of programming and hardware description languages. His current research focus is on modeling, simulation, and verification of cyber-physical systems, and in particular developing the Acumen modeling language.  Taha is credited with developing the idea of multi-stage programming (or “staging” for short), and is the designer of several systems based on it, including MetaOCaml, ConCoqtion, Java Mint, and the Verilog Preprocessor. He contributed to several other programming languages innovations, including statically typed macros, tag elimination, tagless staged interpreters, event-driven functional reactive programming (E-FRP), the notion of exact software design, and gradual typing.

Sunday, May 6, 2012

Second Summer School on Accurate Programming


Halmstad University, May 30 - June 1, 2012

Accurate programming is a practical approach to producing high quality programs. It combines ideas from test-automation, test-driven development, agile programming, and other state of the art software development methods. In addition to building on approaches that have proven effective in practice, it emphasizes concepts that help programmers sharpen their understanding of both the problems they are solving and the solutions they come up with. This is achieved by encouraging programmers to think about programs in terms of properties.
The 2nd Halmstad Summer School on Accurate Programming serves as an introduction to the topic including industrial cases, state-of-the-art tools for modern programming languages and hands-on tutorials.


Lecturers
John HughesQuviQ (CEO) and Chalmers University of Technology. 
Rex Page, Oklahoma University. 
Walid Taha, Halmstad University. 
Veronica Gaspes, Halmstad University.


Program
May 30st (9:00-16:00)
Introduction to automatic testing and test-driven development. Industrial case studies. Introduction to QuviQs QuickCheck for Erlang. Hands on tutorial including testing of parallel programs and testing of C programs from Erlang. 

May 31st (9:00-16:00)
Type-driven development. Use cases as simple properties.  Using ScalaCheck for developing Scala and Java programs. Properties for functions on integer numbers. Properties, functions, and libraries for tuples and collections.  Hands on tutorials with Java, Scala and ScalaCheck.
June 1st (9:00-16:00)
Test-driven development for user-defined types.  Properties and contracts for user-defined types and objects.  Hands on tutorials with Java, Scala and ScalaCheck.
Registration
Deadline is  May 15th. 
  
The registration fee is SEK 500 and covers lunches and coffee breaks. The school is free of charge for masters students, PhD students and for industrial partners associated with CERES and CAISR.
To apply to the summer school, please send an email to Veronica.Gaspes@hh.se with "Accurate Programming Summer School" in the title.

Venue
The summer school will be held on the campus of Halmstad University  in Halmstad, Sweden. 
Directions for getting to campus can be found online.  If you are flying in 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 sj.se, and allow one hour from touchdown to getting to the train station (just outside customs).  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, which is a different country.  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 also fly to ARN in Stockhlm, Sweden, and from ARN take a national flight to Halmstad airport.

Tuesday, May 31, 2011

Getting Started with QuickCheck

Here are a few concrete points to help you get started quickly.

Starting Erlang
If Erlang is correctly installed, then...
...under Windows, choose Erlang OTP R14B02 from the start menu, and in the submenu choose Erlang.
...under Unix, type erl in the shell.
In both cases, an Erlang shell will start.

Changing directory
Make sure the shell is running in the right current directory (especially under Windows). Useful commands:
pwd(). Display the current directory
cd("directory"). Set the current directory

Creating Erlang modules
Choose a lower case name for your module, such as foo. Create a file foo.erl. Please use Emacs as your editor, if at all possible! In the file, write
-module(foo). Specify the module name--must be the same as the file name
-compile(export_all). Export your functions so you can test them.
-include_lib("eqc/include/eqc.hrl"). The QuickCheck header file
Using Emacs, you can insert this code using the menu QuickCheck->Properties->Full module header.
Your function definitions come next. For example,
prop_trivial() -> true.

Compiling Erlang modules
In the Erlang shell, in the same directory as your source code, type
c(foo).

Running QuickCheck tests
In the Erlang shell, type
eqc:quickcheck(foo:prop_trivial()).
and enjoy! Once a module is loaded, hitting tab in the shell completes module and function names, which speeds up typing a lot.

Materials for Wednesday

The materials for the QuickCheck day can now be downloaded here. They include the slides of both lectures, an exercise sheet, and three Erlang source files provided for use in the exercises. Everything is in a zip archive: download it, unzip it, compile the three Erlang files, and away you go.