|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
INRIA Grenoble / CONVECS team
|
|---|---|
| Functionality: |
Hardware Design.
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Period: |
2023-2024
|
| Description: |
SoC (System-on-Chip) architectures, which are widely used in
smartphones and IoT devices, integrate a complete computing system
on a single chip. The complexity of SoCs, together with their potential
use in critical applications, call for thorough verification; however,
the current industrial practice is still mainly based on hardware
simulators using directed tests and/or execution-time assertions.
A major challenge in SoC verification is to devise meaningful
system-level tests involving many components of the SoC.
PSS (Portable test and Stimulus Standard), defined by the Accellera consortium of hardware design tool vendors and users, provides a language to specify both a verification intent (e.g., a sequence of actions) and an implicit description of the SoC's behavior (as a collection of ordering constraints on the actions). PSS also defines a methodology to derive from a verification intent, by automatic inference of (intermediate) actions, complete tests to be executed on the actual SoC. However, since PSS emphasizes the verification intent and limits the modeling of the SoC's behavior to a set of constraints, the actually modeled behavior becomes difficult to grasp. Also, PSS promotes the derivation of complete tests using a backward exploration of the verification intent that favors shortest-path solutions, possibly missing interesting and more complex tests. To improve the PSS testing methodology, this work suggests to formally express the behavior of a PSS model as a composition of communicating LTSs, obtained by an automated translation from PSS to the LNT and EXP languages of CADP, implemented in the PSS2LNT prototype tool. This makes it possible to analyze the corresponding LTS (Labelled Transition System) using the CADP model checker and thus increase the confidence in both the original PSS model and the generated tests. Also, applying conformance testing techniques with coverage guarantees on the LTS enables to improve the coverage of the generated tests. |
| Conclusions: |
The translation from PSS to LNT enables the formal analysis of the
PSS behavior by model checking, therefore helping the early discovery
of modeling errors, increasing confidence in the generated tests, and
avoiding false positives. The translation also opens the way to
conformance testing, making it possible to generate a set of test cases
with coverage guarantees, thus helping to find more bugs in the system
under test. Last but not least, formalizing the natural language
specification of PSS also pinpoints semantic options and ambiguities.
|
| Publications: |
[Ledent-Mateescu-Serwe-24]
Philippe Ledent, Radu Mateescu, and Wendelin Serwe.
"Improving PSS Test Generation Using Model Checking and Conformance
Testing". Proc. of the 2024 Forum on Specification & Design
Languages (FDL'2024), Stockholm, Sweden, September 4-6, 2024.
Available on-line at: https://inria.hal.science/hal-04719995/en |
| Contact: | Wendelin Serwe INRIA Center of University Grenoble Alpes 655, avenue de l'Europe F-38330 Montbonnot Saint Martin FRANCE Email: wendelin.serwe@inria.fr |
| Further remarks: | This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software |
Back to the CADP research tools page