Synchronous closing and flow analysis for model checking timed systems

N. Ioustinova, N. Sidorova, M. Steffen

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

2 Citaten (Scopus)

Samenvatting

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.
Originele taal-2Engels
TitelFormal Methods for Components and Objects (Revised Lectures, FMCO 2003, Leiden, The Netherlands, November 4-7, 2003)
RedacteurenF.S. Boer, M.M. Bonsangue, S. Graf, W.P. Roever, de
Plaats van productieBerlin
UitgeverijSpringer
Pagina's292-313
ISBN van geprinte versie3-540-22942-6
DOI's
StatusGepubliceerd - 2004

Publicatie series

NaamLecture Notes in Computer Science
Volume3188
ISSN van geprinte versie0302-9743

Vingerafdruk

Duik in de onderzoeksthema's van 'Synchronous closing and flow analysis for model checking timed systems'. Samen vormen ze een unieke vingerafdruk.

Citeer dit