Detail publikace
On the Implementation of State-space Exploration Procedure in a Relational Database Management System
Originální název
On the Implementation of State-space Exploration Procedure in a Relational Database Management System
Anglický název
On the Implementation of State-space Exploration Procedure in a Relational Database Management System
Jazyk
en
Originální 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.
Anglický 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.
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",
annote="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.",
address="IEEE Computer Society",
booktitle="30th IFAC Workshop on Real-Time Programming and 4th International Workshop on Real-Time Software",
chapter="30231",
edition="NEUVEDEN",
howpublished="print",
institution="IEEE Computer Society",
year="2009",
month="october",
pages="151--156",
publisher="IEEE Computer Society",
type="conference paper"
}