1st RIDINGS Workshop

on the RIgorous DesIgN of GALS Systems
Inria Montbonnot, May 17, 2017

 

logo convecs            logo tugraz

Scientific programme

09:15

Welcome and coffee

09:30 – 10:00

Josip Bozic (IST / TU Graz)

Security Testing Based on Attack Patterns and Planning 

 

Testing for security related issues is an important task of growing interest due to the vast amount of applications and services available over the internet. Cryptographic protocols like SSL/TLS are implemented to ensure the safety of transferred data between two peers. The biggest challenge for security testing is to specify and implement ways in order to detect potential vulnerabilities in a never-ending quest against new security threats but also to cover already known ones. Therefore, many different approaches have been suggested including fuzz testing and model-based testing approaches. In our work, we suggest to formalize attack patterns from which test cases can be generated and executed automatically. Additionally, we represent attacks as sequences of actions that have to be carried out in order to be successful. Hence, testing is formalized in this context as a problem where the goal is to break the application under test. Both approaches can be extended further so new testing possibilities can be generated.

10:00 – 10:30

Hermann Felbinger (IST / TU Graz)

Test-Suite Reduction Does Not Necessarily Require Executing The Program Under Test

 

Removing redundancies from test-suites is an important task of software testing in order to keep test- suites as small as possible, but not to harm the test-suites fault detection capabilities. A straightforward algorithm for test-suite reduction would select elements of the test-suite randomly and remove them if and only if the reduced test- suite fulfills the same or similar coverage or mutation score. Such algorithms rely on the execution of the program and the repeated computation of coverage or mutation score. Here we present an alternative approach that purely relies on a model learned from the original test-suite without requiring the execution of the program under test. The idea is to remove those tests that do not change the learned model.

Coffee break

11:00 – 11:30

Birgit Hofer (IST / TU Graz)

Fault Localization in Software and Spreadsheets

 

Software debugging, i.e., the process of locating and fixing faults in a program's source code, is rarely automated. Most programmers debug their programs manually or semi-automatically stepping through the code using break points. Therefore, software debugging is a very time-consuming and consequently expensive task.  Spreadsheets are a hot topic because there are 10 times more spreadsheet users than professional programmers and important decisions are often based on spreadsheets. Numerous studies have shown that spreadsheets contain errors at an alarmingly high rate and that the correction of the errors is often time consuming and frustrating. This talk focuses on the fault localization part of the debugging process, i.e., the identification of the statements of the program's source code (or the formulas) that are responsible for an observed error. In particular, two techniques will be presented, namely Model-based Software Debugging (MBSD) and Spectrum-based Fault Localization (SFL).

11:30 – 12:00

Franz Wotawa (IST / TU Graz)

Research activities at the Institute for Software Technology / TU Graz

 

In my talk, I will give an overview of the most recent research activities and projects of the Institute for Software Technology. In addition, I will further give details about the application of model-based techniques to carry out various tasks, including testing and diagnosis.

Lunch

14:00 – 14:30

Frédéric Lang (joint work with CONVECS)

The LNT language and the LNT2LOTOS compiler

 

In this talk, I will present the language LNT developed in our team for describing asynchronous concurrent systems. I will then present the compiler LNT2LOTOS, which translates an LNT specification into a LOTOS one, thus enabling a connection to the CADP verification tools through the Open/Caesar programming interface.

14:30 – 15:00

Hubert Garavel (joint work with Wendelin Serwe)

The Unheralded Value of the Multiway Rendezvous: Illustration with the Production Cell Benchmark

 

The multiway rendezvous introduced in Theoretical CSP is a powerful paradigm to achieve synchronization and communication among a group of (possibly more than two) processes. We illustrate the advantages of this paradigm on the production cell benchmark, a model of a real metal processing plant, for which we propose a compositional software controller, which is written in LNT and LOTOS, and makes intensive use of the multiway rendezvous.

15:00 – 15h30

Lina Marsso (joint work with Hubert Garavel)

A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm

 

We present a term rewrite system that formally models the Message Authenticator Algorithm (MAA), which was one of the first cryptographic functions for computing a Message Authentication Code and was adopted, between 1987 and 2001, in international standards (ISO 8730 and ISO 8731-2) to ensure the authenticity and integrity of banking transactions. Our term rewrite system is large (13 sorts, 18 constructors, 644 non-constructors, and 684 rewrite rules), confluent, and terminating. Implementations in thirteen different languages have been automatically derived from this model and used to validate 200 official test vectors for the MAA.

 

Coffee break

16:00 – 16:30

Gianluca Barbon (joint work with Vincent Leroy and Gwen Salaün)

Debugging of Concurrent Systems using Counterexample Analysis

 

Model checking is an established technique for automatically verifying that a model satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task for several reasons: (i) the counterexample can contain hundreds of actions, (ii) the debugging task is mostly achieved manually, and (iii) the counterexample does not give any clue on the state of the system (e.g., parallelism or data expressions) when the error occurs. This paper presents a new approach that improves the usability of model checking by simplifying the comprehension of counterexamples. Our solution aims at keeping only actions in counterexamples that are relevant for debugging purposes. To do so, we first extract in the model all the counterexamples.  Second, we define an analysis algorithm that identifies actions that make the behaviour skip from incorrect to correct behaviours, making these actions relevant from a debugging perspective. Our approach is fully automated by a tool that we implemented and applied on real-world case studies from various application areas for evaluation purposes..

Closing