Detail výsledku

On the Implementation of State-space Exploration Procedure in a Relational Database Management System

RÁB, J.; RYŠAVÝ, O.; ŠVÉDA, M. On the Implementation of State-space Exploration Procedure in a Relational Database Management System. 30th IFAC Workshop on Real-Time Programming and 4th International Workshop on Real-Time Software. Mragowo: IEEE Computer Society, 2009. p. 151-156. ISBN: 978-83-60810-22-4.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Ráb Jaroslav, Ing., UIFS (FIT)
Ryšavý Ondřej, doc. Ing., Ph.D., UIFS (FIT)
Švéda Miroslav, prof. Ing., CSc., UIFS (FIT), UTKO (FEKT)
Abstrakt

An examination of discrete system's behavior can be done by exhaustive exploration of the state space that is generated
according to the assigned domain semantics. Model-checking is the matured discipline that allows to explore state space as large as several millions of states.  In this paper, we describe a novel approach to the implementation of state exploration procedure using PL/SQL, the language of Oracle relational
database system. The high efficiency of database systems when dealing with large amounts of data and relatively cheap hardware available nowadays advocates the use of relational database as an implementation platform for practical exhaustive state exploration algorithm with the hope that this platform may scale up the model checking method to hundreds of millions of explorable states.

Klíčová slova

Formal Specification, Temporal Logic of Actions, State exploration,
Relational database systems

URL
Rok
2009
Strany
151–156
Sborník
30th IFAC Workshop on Real-Time Programming and 4th International Workshop on Real-Time Software
Konference
30th IFAC Workshop on Real-Time Programming
ISBN
978-83-60810-22-4
Vydavatel
IEEE Computer Society
Místo
Mragowo
BibTeX 
@inproceedings{BUT30231,
  author="Jaroslav {Ráb} and Ondřej {Ryšavý} and Miroslav {Švéda}",
  title="On the Implementation of State-space Exploration Procedure in a Relational Database Management System",
  booktitle="30th IFAC Workshop on Real-Time Programming and 4th International Workshop on Real-Time Software",
  year="2009",
  pages="151--156",
  publisher="IEEE Computer Society",
  address="Mragowo",
  isbn="978-83-60810-22-4",
  url="https://www.fit.vut.cz/research/publication/9063/"
}
Soubory
Projekty
Bezpečnost a zabezpečení aplikací sítí vestavěných systémů, GAČR, Standardní projekty, GA102/08/1429, zahájení: 2008-01-01, ukončení: 2010-12-31, ukončen
Rámec pro deduktivní analýzu softwarových aplikací vestavěných systémů, GAČR, Postdoktorandské granty, GP201/07/P544, zahájení: 2007-01-01, ukončení: 2008-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Pracoviště
Ústav informačních systémů (UIFS)
Nahoru