Name
Abstract | ||
|---|---|---|
Formal methods, especially model checking, are an indispensablepart of the software engineering process. Withlarge software systems currently beyond the range of fullyautomatic verification, however, a combination of decompositionand abstraction techniques is needed. To modelcheck components of a system, a standard approach is toclose the component with an abstraction of its environment.To make it useful in practice, the closing of the componentshould be automatic, both for data and for control abstraction.Specifically for model checking asynchronous opensystems, external input queues should be removed, as theyare a potential source of a combinatorial state explosion.In this paper, we close a component synchronously byembedding the external environment directly into the systemto avoid the external queues, while for the data, we usea two-valued abstraction, namely data influenced from theoutside or not. This gives a more precise analysis than theone investigated in [8]. To further combat the state explosionproblem, we combine this data abstraction with a staticanalysis to remove superfluous code fragments. The staticanalysis we use is reminiscent to the one presented in [8],but we use a combination of a may and a must-analysis insteadof a may-analysis. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1109/APSEC.2002.1182992 | APSEC |
Keywords | Field | DocType |
software model checking,control abstraction,withlarge software system,data abstraction,open components,model checking open asynchronous,program transformation.,external input queue,asynchronous communication,flow analysis,external queue,combinatorial state explosion,formal methods,two-valued abstraction,abstraction,component synchronously,external environment,decompositionand abstraction technique,data analysis,automatic control,open system,model checking,data flow analysis,formal method,software systems,mathematical model,mathematics,computer science,static analysis,open systems,software engineering,formal verification,asynchronous system | Asynchronous communication,Abstraction model checking,Programming language,Model checking,Computer science,Static analysis,Software system,Real-time computing,Abstraction inversion,Formal methods,Formal verification,Distributed computing | Conference |
ISBN | Citations | PageRank |
0-7695-1850-8 | 6 | 0.49 |
References | Authors | |
7 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Natalia Ioustinova | 1 | 62 | 6.99 |
| Natalia Sidorova | 2 | 657 | 54.08 |
| Martin Steffen | 3 | 122 | 10.32 |