0103387 - UIVT-O 20040128 RIV US eng C - Conference Paper (international conference)
Mach, M. - Plášil, František
Addresing State Explosion in Behavior Protocol Verification.
[Řešení problému exponenciálního nárůstu stavového prostoru (state explosion) ve verifikaci protokolů chování (behavior protocols).]
Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing. Michigan: ACIS, 2004 - (Hu, G.; Huang, T.; Ni, X.; Zhou, A.), s. 327-333. ISBN 0-9700776-8-8.
[ACIS. International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing /5./. Beijing (CN), 30.06.2004-02.07.2004]
R&D Projects: GA ČR GA102/03/0672
Institutional research plan: CEZ:AV0Z1030915
Keywords : formal verification * software components * state explosion * behavior protocols * parse trees
Subject RIV: JD - Computer Applications, Robotics

A typical problem formal verification faces is the size of the model of a system being verified. Even for a small system, the state space of the model tends to grow exponentially (state explosion). In this paper, we present a new representation of state spaces suitable for implementing operations upon behavior protocols of software components [1]. The proposed representation is linear in length of the source behavior protocol. By trading space for time, it allows handling behavior protocols of .practical size.. As a proof of concept, a verification tool for behavior protocols is discussed.

Článek navrhuje reprezentaci automatů řešící problém exponenciálního nárůstu stavového prostoru (state explosion), při formální verifikaci protokolů. Tato reprezentace převádí paměťovou náročnost na časovou, ta je poté řešena dalšími optimalizacemi.
Permanent Link: http://hdl.handle.net/11104/0010695