Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation

Brian Campbell; Ian Stark

doi:10.1007/978-3-319-10702-8_13

Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation

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

Abstract

We validate a HOL4 model of the ARM Cortex-M0 microcontroller core by testing the model’s behaviour on randomly chosen instructions against a real chip.

The model and our intended application involve precise timing information about instruction execution, but the implementations are pipelined, so checking the behaviour of single instructions would not give us sufficient confidence in the model. Thus we test the model using sequences of randomly chosen instructions.

The main challenge is to meet the constraints on the initial and intermediate execution states: we must ensure that memory accesses are in range and that we respect restrictions on the instructions. By careful transformation of these constraints an off-the-shelf SMT solver can be used to find suitable states for executing test sequences.

Original language	English
Title of host publication	Formal Methods for Industrial Critical Systems
Subtitle of host publication	19th International Conference, FMICS 2014, Florence, Italy, September 11-12, 2014. Proceedings
Editors	Frédéric Lang, Francesco Flammini
Publisher	Springer
Pages	185-199
Number of pages	15
ISBN (Electronic)	978-3-319-10702-8
ISBN (Print)	978-3-319-10701-1
DOIs	https://doi.org/10.1007/978-3-319-10702-8_13
Publication status	Published - 2014

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	8718
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-319-10702-8_13

Campbell and Stark 2014 Randomised testing of a microprocessor modelAccepted author manuscript, 791 KB

http://link.springer.com/chapter/10.1007%2F978-3-319-10702-8_13

REMS: Rigorous Engineering for Mainstream Systems
Stark, I. (Principal Investigator)
Other
1/03/13 → 29/02/20
Project: Research

Cite this

Campbell, B., & Stark, I. (2014). Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation. In F. Lang, & F. Flammini (Eds.), Formal Methods for Industrial Critical Systems: 19th International Conference, FMICS 2014, Florence, Italy, September 11-12, 2014. Proceedings (pp. 185-199). (Lecture Notes in Computer Science; Vol. 8718). Springer. https://doi.org/10.1007/978-3-319-10702-8_13

@inproceedings{44cde562396042d297798e1308122d7f,

title = "Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation",

abstract = "We validate a HOL4 model of the ARM Cortex-M0 microcontroller core by testing the model{\textquoteright}s behaviour on randomly chosen instructions against a real chip.The model and our intended application involve precise timing information about instruction execution, but the implementations are pipelined, so checking the behaviour of single instructions would not give us sufficient confidence in the model. Thus we test the model using sequences of randomly chosen instructions.The main challenge is to meet the constraints on the initial and intermediate execution states: we must ensure that memory accesses are in range and that we respect restrictions on the instructions. By careful transformation of these constraints an off-the-shelf SMT solver can be used to find suitable states for executing test sequences.",

author = "Brian Campbell and Ian Stark",

year = "2014",

doi = "10.1007/978-3-319-10702-8_13",

language = "English",

isbn = "978-3-319-10701-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "185--199",

editor = "Fr{\'e}d{\'e}ric Lang and Francesco Flammini",

booktitle = "Formal Methods for Industrial Critical Systems",

address = "United Kingdom",

}

Campbell, B & Stark, I 2014, Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation. in F Lang & F Flammini (eds), Formal Methods for Industrial Critical Systems: 19th International Conference, FMICS 2014, Florence, Italy, September 11-12, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8718, Springer, pp. 185-199. https://doi.org/10.1007/978-3-319-10702-8_13

Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation. / Campbell, Brian ; Stark, Ian.
Formal Methods for Industrial Critical Systems: 19th International Conference, FMICS 2014, Florence, Italy, September 11-12, 2014. Proceedings. ed. / Frédéric Lang; Francesco Flammini. Springer, 2014. p. 185-199 (Lecture Notes in Computer Science; Vol. 8718).

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

TY - GEN

T1 - Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation

AU - Campbell, Brian

AU - Stark, Ian

PY - 2014

Y1 - 2014

N2 - We validate a HOL4 model of the ARM Cortex-M0 microcontroller core by testing the model’s behaviour on randomly chosen instructions against a real chip.The model and our intended application involve precise timing information about instruction execution, but the implementations are pipelined, so checking the behaviour of single instructions would not give us sufficient confidence in the model. Thus we test the model using sequences of randomly chosen instructions.The main challenge is to meet the constraints on the initial and intermediate execution states: we must ensure that memory accesses are in range and that we respect restrictions on the instructions. By careful transformation of these constraints an off-the-shelf SMT solver can be used to find suitable states for executing test sequences.

AB - We validate a HOL4 model of the ARM Cortex-M0 microcontroller core by testing the model’s behaviour on randomly chosen instructions against a real chip.The model and our intended application involve precise timing information about instruction execution, but the implementations are pipelined, so checking the behaviour of single instructions would not give us sufficient confidence in the model. Thus we test the model using sequences of randomly chosen instructions.The main challenge is to meet the constraints on the initial and intermediate execution states: we must ensure that memory accesses are in range and that we respect restrictions on the instructions. By careful transformation of these constraints an off-the-shelf SMT solver can be used to find suitable states for executing test sequences.

U2 - 10.1007/978-3-319-10702-8_13

DO - 10.1007/978-3-319-10702-8_13

M3 - Conference contribution

SN - 978-3-319-10701-1

T3 - Lecture Notes in Computer Science

SP - 185

EP - 199

BT - Formal Methods for Industrial Critical Systems

A2 - Lang, Frédéric

A2 - Flammini, Francesco

PB - Springer

ER -

Campbell B , Stark I. Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation. In Lang F, Flammini F, editors, Formal Methods for Industrial Critical Systems: 19th International Conference, FMICS 2014, Florence, Italy, September 11-12, 2014. Proceedings. Springer. 2014. p. 185-199. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-10702-8_13

Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation

Abstract

Publication series

Access to Document

Fingerprint

Projects

REMS: Rigorous Engineering for Mainstream Systems

Cite this