Synchronous closing and flow analysis for model checking timed systems

N. Ioustinova, N. Sidorova, M. Steffen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)


Formal methods, in particular model checking, are increasingly accepted as integral part of system development. With large software systems beyond the range of fully automatic verification, however, a combination of decomposition and abstraction techniques is needed. To model check components of a system, a standard approach is to close the component with an abstraction of its environment, as standard model checkers often do not handle open reactive systems directly. To make it useful in practice, the closing of the component should be automatic, both for data and for control abstraction. Specifically for model checking asynchronous open systems, external input queues should be removed, as they are a potential source of a combinatorial state explosion. In this paper we investigate a class of environmental processes for which the asynchronous communication scheme can safely be replaced by a synchronous one. Such a replacement is possible only if the environment is constructed under rather a severe restriction on the behavior, which can be partially softened via the use of a discrete-time semantics. We employ data-flow analysis to detect instances of variables and timers influenced by the data passing between the system and the environment.
Original languageEnglish
Title of host publicationFormal Methods for Components and Objects (Revised Lectures, FMCO 2003, Leiden, The Netherlands, November 4-7, 2003)
EditorsF.S. Boer, M.M. Bonsangue, S. Graf, W.P. Roever, de
Place of PublicationBerlin
ISBN (Print)3-540-22942-6
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Synchronous closing and flow analysis for model checking timed systems'. Together they form a unique fingerprint.

Cite this