Technical Reports
A List by Author: Petr Slovák
- e-mail:
- slovak(a)ics.muni.cz
Decidable Race Condition for HMSC
by
Vojtěch Řehák,
Petr Slovák,
Jan Strejček,
Loic Hélouet,
December 2009, 30 pages.
FIMU-RS-2009-10.
Available as Postscript,
PDF.
Abstract:
Races in Message Sequence Charts may lead to a bad interpretation of
described behaviours, and are often considered as a design error. While
there is a quadratic-time algorithm detecting races in Basic Message
Sequence Charts (BMSCs), the problem is undecidable for High-level
Message Sequence Charts (HMSCs). To improve this negative situation for
HMSCs, we introduce two new notions: a new concept of race called
trace-race and an extension of the HMSC formalism with open coregions,
i.e. coregions that can extend over more than one BMSC. We present three
arguments showing benefits of our notions over the standard notions of
race and HMSC. First, every trace-race-free HMSC is also race-free.
Second, every race-free HMSC can be equivalently expressed as a
trace-race-free HMSC with open coregions. Last, the trace-race detection
problem for HMSC with open coregions is decidable and PSPACE-complete
(the problem is in P if the number of processes and gates is fixed).
Formalisms and Tools for Design and Specification of Network Protocols
by
Jindřich Babica,
Vojtěch Řehák,
Petr Slovák,
Pavel Troubil,
Martin Zavadil,
May 2007, 33 pages.
FIMU-RS-2007-02.
Available as Postscript,
PDF.
Abstract:
Message Sequence Charts (MSC) are a useful formalism for formalization of
network protocols early in their design phase. In this paper, we introduce
the basics of MSC language and describe some of the possibilities for
automatic location of "problematic" parts in the design. Focus is then given
to different modifications of MSC design (FIFO behavior, bounded channels,
etc. ) as well as formal checking of more complex design properties (MSC
membership, realizability). Next, an introduction of Specification and
Description Language (SDL) is presented. Possibilities of automatic
synthesis of system design in MSC to an SDL model and it`s correctness
verification are mentioned.
