Complete formal verification of multi core embedded systems using bounded model checking

Ulrich Kühne; Daniel Große; Rolf Drechsler

doi:10.1109/DCAS.2006.321055

Complete formal verification of multi core embedded systems using bounded model checking

Ulrich Kühne
, Daniel Große
, Rolf Drechsler

University of Bremen

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Embedded systems are today frequently used in many applications. Modern designs show a rising complexity, partially including multiple CPU cores. The verification of such systems has to deal with parallel execution of programs and resource conflicts. In this paper we introduce an approach for the formal verification of multi core embedded systems. Bounded model checking is used as the underlying technique. It is shown how it can be applied to the verification of multi core systems ranging from the hardware up to the interaction of multiple cores on the software layer. The approach is demonstrated by the complete verification of a dual core RISC CPU.

Original language	English
Title of host publication	2006 IEEE Dallas ICAS Workshop on Design, Applications, Integration and Software, DCAS-06
Pages	147-150
Number of pages	4
DOIs	https://doi.org/10.1109/DCAS.2006.321055
Publication status	Published - 1 Dec 2006
Externally published	Yes
Event	2006 IEEE Dallas ICAS Workshop on Design, Applications, Integration and Software, DCAS-06 - Richardson, TX, United States Duration: 29 Oct 2006 → 30 Oct 2006

Publication series

Name	2006 IEEE Dallas/CAS Workshop onDesign, Applications, Integration and Software, DCAS-06

Conference

Conference	2006 IEEE Dallas ICAS Workshop on Design, Applications, Integration and Software, DCAS-06
Country/Territory	United States
City	Richardson, TX
Period	29/10/06 → 30/10/06

Access to Document

10.1109/DCAS.2006.321055

Cite this

Kühne, U., Große, D., & Drechsler, R. (2006). Complete formal verification of multi core embedded systems using bounded model checking. In 2006 IEEE Dallas ICAS Workshop on Design, Applications, Integration and Software, DCAS-06 (pp. 147-150). Article 4115134 (2006 IEEE Dallas/CAS Workshop onDesign, Applications, Integration and Software, DCAS-06). https://doi.org/10.1109/DCAS.2006.321055

@inproceedings{6f783e0c70f74c9eb806be94a79c53a4,

title = "Complete formal verification of multi core embedded systems using bounded model checking",

abstract = "Embedded systems are today frequently used in many applications. Modern designs show a rising complexity, partially including multiple CPU cores. The verification of such systems has to deal with parallel execution of programs and resource conflicts. In this paper we introduce an approach for the formal verification of multi core embedded systems. Bounded model checking is used as the underlying technique. It is shown how it can be applied to the verification of multi core systems ranging from the hardware up to the interaction of multiple cores on the software layer. The approach is demonstrated by the complete verification of a dual core RISC CPU.",

author = "Ulrich K{\"u}hne and Daniel Gro{\ss}e and Rolf Drechsler",

year = "2006",

month = dec,

day = "1",

doi = "10.1109/DCAS.2006.321055",

language = "English",

isbn = "1424406692",

series = "2006 IEEE Dallas/CAS Workshop onDesign, Applications, Integration and Software, DCAS-06",

pages = "147--150",

booktitle = "2006 IEEE Dallas ICAS Workshop on Design, Applications, Integration and Software, DCAS-06",

note = "2006 IEEE Dallas ICAS Workshop on Design, Applications, Integration and Software, DCAS-06 ; Conference date: 29-10-2006 Through 30-10-2006",

}

Kühne, U, Große, D & Drechsler, R 2006, Complete formal verification of multi core embedded systems using bounded model checking. in 2006 IEEE Dallas ICAS Workshop on Design, Applications, Integration and Software, DCAS-06., 4115134, 2006 IEEE Dallas/CAS Workshop onDesign, Applications, Integration and Software, DCAS-06, pp. 147-150, 2006 IEEE Dallas ICAS Workshop on Design, Applications, Integration and Software, DCAS-06, Richardson, TX, United States, 29/10/06. https://doi.org/10.1109/DCAS.2006.321055

Complete formal verification of multi core embedded systems using bounded model checking. / Kühne, Ulrich; Große, Daniel; Drechsler, Rolf.
2006 IEEE Dallas ICAS Workshop on Design, Applications, Integration and Software, DCAS-06. 2006. p. 147-150 4115134 (2006 IEEE Dallas/CAS Workshop onDesign, Applications, Integration and Software, DCAS-06).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Complete formal verification of multi core embedded systems using bounded model checking

AU - Kühne, Ulrich

AU - Große, Daniel

AU - Drechsler, Rolf

PY - 2006/12/1

Y1 - 2006/12/1

N2 - Embedded systems are today frequently used in many applications. Modern designs show a rising complexity, partially including multiple CPU cores. The verification of such systems has to deal with parallel execution of programs and resource conflicts. In this paper we introduce an approach for the formal verification of multi core embedded systems. Bounded model checking is used as the underlying technique. It is shown how it can be applied to the verification of multi core systems ranging from the hardware up to the interaction of multiple cores on the software layer. The approach is demonstrated by the complete verification of a dual core RISC CPU.

AB - Embedded systems are today frequently used in many applications. Modern designs show a rising complexity, partially including multiple CPU cores. The verification of such systems has to deal with parallel execution of programs and resource conflicts. In this paper we introduce an approach for the formal verification of multi core embedded systems. Bounded model checking is used as the underlying technique. It is shown how it can be applied to the verification of multi core systems ranging from the hardware up to the interaction of multiple cores on the software layer. The approach is demonstrated by the complete verification of a dual core RISC CPU.

UR - https://www.scopus.com/pages/publications/46249132345

U2 - 10.1109/DCAS.2006.321055

DO - 10.1109/DCAS.2006.321055

M3 - Conference contribution

AN - SCOPUS:46249132345

SN - 1424406692

SN - 9781424406692

T3 - 2006 IEEE Dallas/CAS Workshop onDesign, Applications, Integration and Software, DCAS-06

SP - 147

EP - 150

BT - 2006 IEEE Dallas ICAS Workshop on Design, Applications, Integration and Software, DCAS-06

T2 - 2006 IEEE Dallas ICAS Workshop on Design, Applications, Integration and Software, DCAS-06

Y2 - 29 October 2006 through 30 October 2006

ER -

Complete formal verification of multi core embedded systems using bounded model checking

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this