Modeling for verification

Sanjit A. Seshia*, Natasha Sharygina, Stavros Tripakis

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapterScientificpeer-review

7 Citations (Scopus)

Abstract

System modeling is the initial, and often crucial, step in verification. The right choice of model and modeling language is important for both designers and users of verification tools. This chapter aims to provide a guide to system modeling in four stages. First, it provides an overview of the main issues one must consider in modeling systems for verification. These issues involve both the selection or design of a modeling language and the steps of model creation. Next, it introduces a simple modeling language, SML, for illustrating the issues involved in selecting or designing a modeling language. SML uses an abstract state machine formalism that captures key features of widely-used languages based on transition system representations. We introduce the simple modeling language to simplify the connection between languages used by practitioners (such as Verilog, Simulink, or C) and various underlying formalisms (e.g., automata or Kripke structures) used in model checking. Third, the chapter demonstrates key steps in model creation using SML with illustrative examples. Finally, the presented modeling language SML is mapped to standard formalisms such as Kripke structures.

Original languageEnglish
Title of host publicationHandbook of Model Checking
Pages75-105
Number of pages31
ISBN (Electronic)9783319105758
DOIs
Publication statusPublished - 18 May 2018
MoE publication typeA3 Part of a book or another research book

Fingerprint Dive into the research topics of 'Modeling for verification'. Together they form a unique fingerprint.

Cite this