NuSeen: A Tool Framework for the NuSMV Model Checker

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F17%3A10360077" target="_blank" >RIV/00216208:11320/17:10360077 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1109/ICST.2017.54" target="_blank" >http://dx.doi.org/10.1109/ICST.2017.54</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/ICST.2017.54" target="_blank" >10.1109/ICST.2017.54</a>

Jazyk výsledku

angličtina

Název v původním jazyce

NuSeen: A Tool Framework for the NuSMV Model Checker

Popis výsledku v původním jazyce

NuSMV is a well-known tool for system verification that permits to verify both CTL and LTL properties. Although the tool is very powerful, it offers a minimal support for the editing and validation (e.g., by simulation) of models and of requirements specified as temporal properties. In this paper, we propose NuSeen, a framework that assists a designer during the modeling and V&amp;V activities when using NuSMV. In addition to an editor furnished with syntax highlighting, autocompletion, and outline, NuSeen also provides some tools for visualizing the variable dependencies, and graphically visualizing the counterexamples. It helps the designer in validating the model by checking certain qualities like minimality and completeness. Moreover, the framework also provides facilities for model-based testing by means of a test suite generator that is able to generate tests achieving value and decision coverage for NuSMV models.

Název v anglickém jazyce

NuSeen: A Tool Framework for the NuSMV Model Checker

Popis výsledku anglicky

NuSMV is a well-known tool for system verification that permits to verify both CTL and LTL properties. Although the tool is very powerful, it offers a minimal support for the editing and validation (e.g., by simulation) of models and of requirements specified as temporal properties. In this paper, we propose NuSeen, a framework that assists a designer during the modeling and V&amp;V activities when using NuSMV. In addition to an editor furnished with syntax highlighting, autocompletion, and outline, NuSeen also provides some tools for visualizing the variable dependencies, and graphically visualizing the counterexamples. It helps the designer in validating the model by checking certain qualities like minimality and completeness. Moreover, the framework also provides facilities for model-based testing by means of a test suite generator that is able to generate tests achieving value and decision coverage for NuSMV models.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA17-12465S" target="_blank" >GA17-12465S: Verifikace a hledání chyb v pokročilém softwaru</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)

ISBN

978-1-5090-6031-3

ISSN

2381-2834

e-ISSN

neuvedeno

Počet stran výsledku

8

Strana od-do

476-483

Název nakladatele

Institute of Electrical and Electronics Engineers Inc.

Místo vydání

Neuveden

Místo konání akce

Tokyo, Japan

Datum konání akce

13. 3. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000403393600047