An experience in proving regular networks of processes by modular model checking

DOI10.1007/BF01185559zbMath0790.68071MaRDI QIDQ1323369

Christophe Ratel, Nicolas Halbwachs, Fabienne Lagnier

Publication date: 2 June 1994

Published in: Acta Informatica (Search for Journal in Brave)

zbMATH Keywords

verificationreal-time systemsmodel checkingspecificationsynchronous systemscircuit behaviorregular network of hardware devicessynchronous declarative language

Mathematics Subject Classification ID

Network design and communication in computer systems (68M10) Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Model checking and abstraction to the aid of parameterized systems (a survey), Causality problem in real-time calculus, Networks of Processes with Parameterized State Space, Symbolic model checking with rich assertional languages, Automatic verification of parameterized networks of processes, Automatically testing interactive applications using extended task trees, A novel approach to verifying context free properties of programs

Uses Software

• CESAR
• LUSTRE

Cites Work

• Proving properties of a ring of finite-state machines
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• Unnamed Item
• Unnamed Item
• Unnamed Item