Abstraction and flow analysis for model checking open asynchronous systems
Formal methods, especially model checking, are an indispensable part of the software engineering process. With large software systems currently 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. 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 close a component synchronously by embedding the external environment directly into the system to avoid the external queues, while for the data, we use a two-valued abstraction, namely data influenced from the outside or not. This gives a more precise analysis than the one investigated in . To further combat the state explosion problem, we combine this data abstraction with a static analysis to remove superfluous code fragments. The static analysis we use is reminiscent to the one presented in , but we use a combination of a may and a must-analysis instead of a may-analysis.
|Design Tools and Techniques (acm D.2.2), Software/Program Verification (acm D.2.4), Languages (acm D.2.1.1), Model Validation and Analysis (acm I.6.4)|
|Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (msc 68N30), Semantics (msc 68Q55), Specification and verification (program logics, model checking, etc.) (msc 68Q60), Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (msc 68Q85)|
|Software Engineering [SEN]|
|Organisation||Specification and Analysis of Embedded Systems|
Ioustinova, N, Sidorova, N, & Steffen, M. (2002). Abstraction and flow analysis for model checking open asynchronous systems. Software Engineering [SEN]. CWI.