Modeling for verification

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

Researchers

Research units

  • University of California at Berkeley
  • Università della Svizzera italiana

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.

Details

Original languageEnglish
Title of host publicationHandbook of Model Checking
Publication statusPublished - 18 May 2018
MoE publication typeA3 Part of a book or another research book

ID: 29254616