×

Synchronous closing and flow analysis for model checking timed systems. (English) Zbl 1104.68415

de Boer, Frank S. (ed.) et al., Formal methods for components and objects. Second international symposium, FMCO 2003, Leiden The Netherlands, November 4–7, 2003. Revised lectures. Berlin: Springer (ISBN 3-540-22942-6/pbk). Lecture Notes in Computer Science 3188, 292-313 (2004).
Summary: 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.
For the entire collection see [Zbl 1060.68006].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

MOCHA
PDFBibTeX XMLCite
Full Text: DOI