An experience in proving regular networks of processes by modular model checking
type: Item
instance of: scholarly article
title: An experience in proving regular networks of processes by modular model checking
zbMATH Open document ID: 0790.68071
DOI: 10.1007/BF01185559
author: Nicolas Halbwachs
author: Fabienne Lagnier
author: Christophe Ratel
published in: Acta Informatica
publication date: 1994-06-02T00:00:00Z
review text: This paper presents a complete example of the use of the synchronous declarative language LUSTRE for the specification, description and verification of a resource arbiter, which is a regular network of hardware devices. The fact that both programs and properties may be expressed in LUSTRE is used to perform an inductive verification. An invariant property of the network is found, and merged with the description program. Verification is performed by model checking.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68M10
Mathematics Subject Classification ID: 94C10
Mathematics Subject Classification ID: 68N15
zbMATH DE Number: 567326
zbMATH Keywords: synchronous systems
zbMATH Keywords: real-time systems
zbMATH Keywords: circuit behavior
zbMATH Keywords: verification
zbMATH Keywords: synchronous declarative language
zbMATH Keywords: specification
zbMATH Keywords: regular network of hardware devices
zbMATH Keywords: model checking
describes a project that uses: LUSTRE
describes a project that uses: CESAR
MaRDI profile type: Publication
cites work: Graph-Based Algorithms for Boolean Function Manipulation
cites work: Automatic verification of finite-state concurrent systems using temporal logic specifications
cites work: Q4037091
cites work: Q3711745
cites work: Q3940830
cites work: Proving properties of a ring of finite-state machines
Recommended article: A model and temporal proof system for networks of processes
Recommended article: Formal Techniques for Networked and Distributed Systems - FORTE 2005
Recommended article: Automatic verification of parameterized networks of processes
Recommended article: Q3347278
Recommended article: Regular model checking revisited
Recommended article: CONCUR 2004 - Concurrency Theory
Recommended article: Model checking for process rewrite systems and a class of action-based regular properties
Recommended article: Verification, Model Checking, and Abstract Interpretation
Recommended article: Applications and Theory of Petri Nets 2004
description: scientific article; zbMATH DE number 567326