2nd RIDINGS Workshop

on the RIgorous DesIgN of GALS Systems
IST Graz, November 15, 2017

 

logo convecs            logo tugraz


Scientific programme


11:30 – 12:00

Wendelin Serwe (Inria CONVECS)

Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip 

 

We report about a case study on the functional verification of a System-on-Chip (SoC) with a formal system-level model. Our approach improves industrial simulation-based verification techniques in two aspects. First, we suggest to use the formal model to assess the sanity of an interface verification unit. Second, we present a two-step approach to generate clever semi-directed test cases from temporal logic properties: model-based testing tools of the CADP toolbox generate system-level abstract test cases, which are then refined with a commercial Coverage-Directed Test Generation tool into interface-level concrete test cases that can be executed at RTL level. Applied to an AMBA 4 ACE-based cache-coherent SoC, we found that our approach helps in the transition from interface-level to system-level verification, facilitates the validation of system-level properties, and enables early detection of bugs in both the SoC and the commercial test-bench.

12:00 – 12:30

Lina Marsso (Inria CONVECS)

TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation

 

We present TESTOR, a tool for on-the-fly conformance test case generation, guided by test purposes. Concretely, given a formal specification of a system and a test purpose, TESTOR automatically generates test cases, which assess using black box testing techniques the conformance to the specification of a system under test. In this context, a test purpose describes the goal states to be reached by the test and enables one to indicate parts of the specification that should be ignored during the testing process. Compared to the existing tool TGV, TESTOR has a more modular architecture, based on generic graph transformation components, is capable of extracting a test case completely on the fly, and enables a more flexible expression of test purposes, taking advantage of the multiway rendezvous. TESTOR has been implemented on top of the CADP verification toolbox, evaluated on three published case-studies and more than 10000 examples taken from the non-regression test suites of CADP.

12:30 – 13:30

Bernhard Aichernig (IST / TU Graz)

Smart Black-box Testing - Combining Model Learning and Model-based Testing

 

Testing has always been a challenge due to (1) its incompleteness by nature, (2) the lack of good specifications and (3) by its high demand for resources. With the growing complexity of the systems-under-test the situation is not likely to improve. The combination of model-learning with model-based testing offers an opportunity to master this complexity. In my talk I will introduce this line of research and report about our recent results including applications in the Internet of Things. Our goal is a natural evolution of testing: with the trend of our environment becoming "smarter", e.g. smart homes, smart cars, smart production, smart energy, our testing process needs to become smart as well. We are seeing the advent of smart testing.

13:30 – 15:00

Lunch and technical discussion