Formal verification and software product lines

Tomoji Kishi, Natsuko Noda

研究成果: Article

21 引用 (Scopus)

抄録

A systematic method to verify designs within a product line based on formal verification techniques is presented. Model checking techniques to design verification, which is a formal verification technique in which the target system is described as a finite state model and provide some logical properties, was applied. Test scenarios were utilize for the design verification because it is a typical method for defining verification items. The application of the design verification was examine in the context of product line development for the verification by reuse. The variation points in the verification model were defined, a technique using UML has been been proposed that denotes variation points and variants by attaching certain stereotypes, to reuse the model in product line development. This formal verification techniques is one of the promising techniques to develop reliable embedded software.

元の言語English
記事番号1183270
ジャーナルCommunications of the ACM
49
発行部数12
DOI
出版物ステータスPublished - 2006 12 1
外部発表Yes

Fingerprint

Embedded software
Model checking
Formal verification

ASJC Scopus subject areas

  • Hardware and Architecture
  • Computer Graphics and Computer-Aided Design
  • Software
  • Theoretical Computer Science
  • Computational Theory and Mathematics

これを引用

Formal verification and software product lines. / Kishi, Tomoji; Noda, Natsuko.

:: Communications of the ACM, 巻 49, 番号 12, 1183270, 01.12.2006.

研究成果: Article

@article{a12a2a77948c4820b737afd2ca9692f2,
title = "Formal verification and software product lines",
abstract = "A systematic method to verify designs within a product line based on formal verification techniques is presented. Model checking techniques to design verification, which is a formal verification technique in which the target system is described as a finite state model and provide some logical properties, was applied. Test scenarios were utilize for the design verification because it is a typical method for defining verification items. The application of the design verification was examine in the context of product line development for the verification by reuse. The variation points in the verification model were defined, a technique using UML has been been proposed that denotes variation points and variants by attaching certain stereotypes, to reuse the model in product line development. This formal verification techniques is one of the promising techniques to develop reliable embedded software.",
author = "Tomoji Kishi and Natsuko Noda",
year = "2006",
month = "12",
day = "1",
doi = "10.1145/1183236.1183270",
language = "English",
volume = "49",
journal = "Communications of the ACM",
issn = "0001-0782",
publisher = "Association for Computing Machinery (ACM)",
number = "12",

}

TY - JOUR

T1 - Formal verification and software product lines

AU - Kishi, Tomoji

AU - Noda, Natsuko

PY - 2006/12/1

Y1 - 2006/12/1

N2 - A systematic method to verify designs within a product line based on formal verification techniques is presented. Model checking techniques to design verification, which is a formal verification technique in which the target system is described as a finite state model and provide some logical properties, was applied. Test scenarios were utilize for the design verification because it is a typical method for defining verification items. The application of the design verification was examine in the context of product line development for the verification by reuse. The variation points in the verification model were defined, a technique using UML has been been proposed that denotes variation points and variants by attaching certain stereotypes, to reuse the model in product line development. This formal verification techniques is one of the promising techniques to develop reliable embedded software.

AB - A systematic method to verify designs within a product line based on formal verification techniques is presented. Model checking techniques to design verification, which is a formal verification technique in which the target system is described as a finite state model and provide some logical properties, was applied. Test scenarios were utilize for the design verification because it is a typical method for defining verification items. The application of the design verification was examine in the context of product line development for the verification by reuse. The variation points in the verification model were defined, a technique using UML has been been proposed that denotes variation points and variants by attaching certain stereotypes, to reuse the model in product line development. This formal verification techniques is one of the promising techniques to develop reliable embedded software.

UR - http://www.scopus.com/inward/record.url?scp=33751559204&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33751559204&partnerID=8YFLogxK

U2 - 10.1145/1183236.1183270

DO - 10.1145/1183236.1183270

M3 - Article

AN - SCOPUS:33751559204

VL - 49

JO - Communications of the ACM

JF - Communications of the ACM

SN - 0001-0782

IS - 12

M1 - 1183270

ER -