Verification of Large State/Event Systems using Compositionality and Dependency Analysis

Jørn Lind-Nielsen; Henrik Reif Andersen; Henrik Hulgaard; Gerd Behrmann; Kaare Kristoffersen; Kim G. Larsen

doi:10.1023/a:1008736219484

Verification of Large State/Event Systems using Compositionality and Dependency Analysis

Authors:

Lind-Nielsen, Jørn ;
Close
Department of Information Technology, Technical University of Denmark
Andersen, Henrik Reif ;
Close
Department of Information Technology, Technical University of Denmark
Hulgaard, Henrik ;
Close
unknown
Behrmann, Gerd ;
Close
Aalborg University
Kristoffersen, Kaare ;
Close
Aalborg University
Larsen, Kim G.
Close
Aalborg University

DOI:

10.1023/a:1008736219484

Abstract:

A state/event model is a concurrent version of Mealy machines used for describing embedded reactive systems. This paper introduces a technique that uses compositionality and dependency analysis to significantly improve the efficiency of symbolic model checking of state/event models. It makes possible automated verification of large industrial designs with the use of only modest resources (less than 5 minutes on a standard PC for a model with 1421 concurrent machines). The results of the paper are being implemented in the next version of the commercial tool visualSTATETM.

Type:

Journal article

Language:

English

Published in:

Formal Methods in System Design, 2001, Vol 18, Issue 1, p. 5-23

Keywords:

Formal verification; Symbolic model checking; Backwards reachability; Embedded software

Main Research Area:

Science/technology

Publication Status:

Published

Review type:

Peer Review

Submission year:

2001

Scientific Level:

Scientific

ID:

5659643

Verification of Large State/Event Systems using Compositionality and Dependency Analysis

Full text access

On-site access

At institutions

Example	Finds records
water{}	containing the word "water".
water supplies"{}"	containing the phrase "water supplies".
author:"Doe, John"author:"{}"	containing the phrase "Doe, John" in the author field.
title:IEEEtitle:{}	containing the word "IEEE" in the title field.
bech{}	containing the word "bech".
marie bech"{}"	containing the phrase "marie bech".
orcid:0000-0002-5429-5292orcid:{}	Having a particular ORCID
Need more help?	Advanced search tutorial