Synchronous Closing and Flow Analysis for Model Checking Timed Systems

Abstract. 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, ation of decomposition and abstraction techniques is needed. To model check components of a system, a standard approach is to close the t 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, 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 r...

• Type: Conference
• Year: 2003
• Where: FMCO
• Authors: Natalia Ioustinova, Natalia Sidorova, Martin Steffen
• Keywords: FMCO 2003, Model Checking, Particular Model Checking, Standard Model Checkers