Rapid Verification of Embedded Systems Using Patterns

W. T. Tsai, L. Yu, F. Zhu, R. Paul

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Citations (Scopus)

Abstract

Verification pattern (VP) is a new technique to test embedded systems rapidly, and it has been used to test industrial safety-critical embedded systems successfully. The key concept of this approach is to classify system scenarios into patterns, and use the same code template to test all the scenarios of the same pattern. In this way, testing effort can be greatly reduced. This paper extends VPs so that they can fully interoperate with a formalized scenario model ACDATE. In this way, various static and dynamic analyses can be performed on system scenarios as well as on system patterns. Furthermore, this paper provides a mapping from system scenarios into temporal logic expressions. In this way, a practitioner can specify system constraints in scenarios, and follow the mapping to obtain the temporal logic expressions easily to perform formal model checking. This paper also provides an OO framework to support automated test script development from VPs. In this way, VPs can be used in an integrated process where both semi-formal analyses and formal techniques can be used together to develop mission-critical embedded applications.

Original languageEnglish (US)
Title of host publicationProceedings - IEEE Computer Society's International Computer Software and Applications Conference
Pages466-471
Number of pages6
StatePublished - 2003
EventProceedings: 27th Annual International Computer Software and Applications Conference, COMPSAC 2003 - Dallas, TX, United States
Duration: Nov 3 2003Nov 6 2003

Other

OtherProceedings: 27th Annual International Computer Software and Applications Conference, COMPSAC 2003
CountryUnited States
CityDallas, TX
Period11/3/0311/6/03

Fingerprint

Temporal logic
Embedded systems
Model checking
Testing

Keywords

  • Embedded systems
  • Model checking
  • Testing
  • Verification
  • Verification patterns

ASJC Scopus subject areas

  • Software

Cite this

Tsai, W. T., Yu, L., Zhu, F., & Paul, R. (2003). Rapid Verification of Embedded Systems Using Patterns. In Proceedings - IEEE Computer Society's International Computer Software and Applications Conference (pp. 466-471)

Rapid Verification of Embedded Systems Using Patterns. / Tsai, W. T.; Yu, L.; Zhu, F.; Paul, R.

Proceedings - IEEE Computer Society's International Computer Software and Applications Conference. 2003. p. 466-471.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Tsai, WT, Yu, L, Zhu, F & Paul, R 2003, Rapid Verification of Embedded Systems Using Patterns. in Proceedings - IEEE Computer Society's International Computer Software and Applications Conference. pp. 466-471, Proceedings: 27th Annual International Computer Software and Applications Conference, COMPSAC 2003, Dallas, TX, United States, 11/3/03.
Tsai WT, Yu L, Zhu F, Paul R. Rapid Verification of Embedded Systems Using Patterns. In Proceedings - IEEE Computer Society's International Computer Software and Applications Conference. 2003. p. 466-471
Tsai, W. T. ; Yu, L. ; Zhu, F. ; Paul, R. / Rapid Verification of Embedded Systems Using Patterns. Proceedings - IEEE Computer Society's International Computer Software and Applications Conference. 2003. pp. 466-471
@inproceedings{8360d1f77f114b7b8f76c3479abaf42a,
title = "Rapid Verification of Embedded Systems Using Patterns",
abstract = "Verification pattern (VP) is a new technique to test embedded systems rapidly, and it has been used to test industrial safety-critical embedded systems successfully. The key concept of this approach is to classify system scenarios into patterns, and use the same code template to test all the scenarios of the same pattern. In this way, testing effort can be greatly reduced. This paper extends VPs so that they can fully interoperate with a formalized scenario model ACDATE. In this way, various static and dynamic analyses can be performed on system scenarios as well as on system patterns. Furthermore, this paper provides a mapping from system scenarios into temporal logic expressions. In this way, a practitioner can specify system constraints in scenarios, and follow the mapping to obtain the temporal logic expressions easily to perform formal model checking. This paper also provides an OO framework to support automated test script development from VPs. In this way, VPs can be used in an integrated process where both semi-formal analyses and formal techniques can be used together to develop mission-critical embedded applications.",
keywords = "Embedded systems, Model checking, Testing, Verification, Verification patterns",
author = "Tsai, {W. T.} and L. Yu and F. Zhu and R. Paul",
year = "2003",
language = "English (US)",
pages = "466--471",
booktitle = "Proceedings - IEEE Computer Society's International Computer Software and Applications Conference",

}

TY - GEN

T1 - Rapid Verification of Embedded Systems Using Patterns

AU - Tsai, W. T.

AU - Yu, L.

AU - Zhu, F.

AU - Paul, R.

PY - 2003

Y1 - 2003

N2 - Verification pattern (VP) is a new technique to test embedded systems rapidly, and it has been used to test industrial safety-critical embedded systems successfully. The key concept of this approach is to classify system scenarios into patterns, and use the same code template to test all the scenarios of the same pattern. In this way, testing effort can be greatly reduced. This paper extends VPs so that they can fully interoperate with a formalized scenario model ACDATE. In this way, various static and dynamic analyses can be performed on system scenarios as well as on system patterns. Furthermore, this paper provides a mapping from system scenarios into temporal logic expressions. In this way, a practitioner can specify system constraints in scenarios, and follow the mapping to obtain the temporal logic expressions easily to perform formal model checking. This paper also provides an OO framework to support automated test script development from VPs. In this way, VPs can be used in an integrated process where both semi-formal analyses and formal techniques can be used together to develop mission-critical embedded applications.

AB - Verification pattern (VP) is a new technique to test embedded systems rapidly, and it has been used to test industrial safety-critical embedded systems successfully. The key concept of this approach is to classify system scenarios into patterns, and use the same code template to test all the scenarios of the same pattern. In this way, testing effort can be greatly reduced. This paper extends VPs so that they can fully interoperate with a formalized scenario model ACDATE. In this way, various static and dynamic analyses can be performed on system scenarios as well as on system patterns. Furthermore, this paper provides a mapping from system scenarios into temporal logic expressions. In this way, a practitioner can specify system constraints in scenarios, and follow the mapping to obtain the temporal logic expressions easily to perform formal model checking. This paper also provides an OO framework to support automated test script development from VPs. In this way, VPs can be used in an integrated process where both semi-formal analyses and formal techniques can be used together to develop mission-critical embedded applications.

KW - Embedded systems

KW - Model checking

KW - Testing

KW - Verification

KW - Verification patterns

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

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

M3 - Conference contribution

AN - SCOPUS:0344235388

SP - 466

EP - 471

BT - Proceedings - IEEE Computer Society's International Computer Software and Applications Conference

ER -