0103387 - UIVT-O 20040128 RIV US eng C - Konferenční příspěvek (zahraniční konf.)
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]
Grant CEP: GA ČR GA102/03/0672
Výzkumný záměr: CEZ:AV0Z1030915
Klíčová slova: formal verification * software components * state explosion * behavior protocols * parse trees
Kód oboru RIV: JD - Využití počítačů, robotika a její aplikace

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.
Trvalý link: http://hdl.handle.net/11104/0010695