|
2nd RIDINGS
Workshop on the RIgorous DesIgN
of GALS Systems |
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 |
|